diff options
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 68 |
1 files changed, 36 insertions, 32 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index e4d2c9322..f712c8d19 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -1,51 +1,53 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*s Identifiers *) +(** {6 Identifiers } *) type identifier type name = Name of identifier | Anonymous -(* Parsing and printing of identifiers *) + +(** Parsing and printing of identifiers *) val string_of_id : identifier -> string val id_of_string : string -> identifier val id_ord : identifier -> identifier -> int -(* Identifiers sets and maps *) +(** Identifiers sets and maps *) module Idset : Set.S with type elt = identifier module Idpred : Predicate.S with type elt = identifier module Idmap : Map.S with type key = identifier -(*s Directory paths = section names paths *) +(** {6 Directory paths = section names paths } *) type module_ident = identifier module ModIdmap : Map.S with type key = module_ident type dir_path -(* Inner modules idents on top of list (to improve sharing). +(** Inner modules idents on top of list (to improve sharing). For instance: A.B.C is ["C";"B";"A"] *) val make_dirpath : module_ident list -> dir_path val repr_dirpath : dir_path -> module_ident list val empty_dirpath : dir_path -(* Printing of directory paths as ["coq_root.module.submodule"] *) +(** Printing of directory paths as ["coq_root.module.submodule"] *) val string_of_dirpath : dir_path -> string -(*s Unique identifier to be used as "self" in structures and +(** {6 Sect } *) +(** Unique identifier to be used as "self" in structures and signatures - invisible for users *) type label type mod_self_id -(* The first argument is a file name - to prevent conflict between +(** The first argument is a file name - to prevent conflict between different files *) val make_msid : dir_path -> string -> mod_self_id val repr_msid : mod_self_id -> int * string * dir_path @@ -55,7 +57,7 @@ val refresh_msid : mod_self_id -> mod_self_id val debug_string_of_msid : mod_self_id -> string val string_of_msid : mod_self_id -> string -(*s Unique names for bound modules *) +(** {6 Unique names for bound modules } *) type mod_bound_id val make_mbid : dir_path -> string -> mod_bound_id @@ -65,7 +67,7 @@ val label_of_mbid : mod_bound_id -> label val debug_string_of_mbid : mod_bound_id -> string val string_of_mbid : mod_bound_id -> string -(*s Names of structure elements *) +(** {6 Names of structure elements } *) val mk_label : string -> label val string_of_label : label -> string @@ -76,11 +78,11 @@ val id_of_label : label -> identifier module Labset : Set.S with type elt = label module Labmap : Map.S with type key = label -(*s The module part of the kernel name *) +(** {6 The module part of the kernel name } *) type module_path = | MPfile of dir_path | MPbound of mod_bound_id - (* | MPapp of module_path * module_path very soon *) + (** | MPapp of module_path * module_path very soon *) | MPdot of module_path * label @@ -91,18 +93,18 @@ val string_of_mp : module_path -> string module MPset : Set.S with type elt = module_path module MPmap : Map.S with type key = module_path -(* Name of the toplevel structure *) +(** Name of the toplevel structure *) val initial_msid : mod_self_id -val initial_path : module_path (* [= MPself initial_msid] *) +val initial_path : module_path (** [= MPself initial_msid] *) -(* Initial "seed" of the unique identifier generator *) +(** Initial "seed" of the unique identifier generator *) val initial_dir : dir_path -(*s The absolute names of objects seen by kernel *) +(** {6 The absolute names of objects seen by kernel } *) type kernel_name -(* Constructor and destructor *) +(** Constructor and destructor *) val make_kn : module_path -> dir_path -> label -> kernel_name val repr_kn : kernel_name -> module_path * dir_path * label @@ -118,17 +120,19 @@ module KNpred : Predicate.S with type elt = kernel_name module KNmap : Map.S with type key = kernel_name -(*s Specific paths for declarations *) +(** {6 Specific paths for declarations } *) type variable = identifier type constant type mutual_inductive -(* Beware: first inductive has index 0 *) + +(** Beware: first inductive has index 0 *) type inductive = mutual_inductive * int -(* Beware: first constructor has index 1 *) + +(** Beware: first constructor has index 1 *) type constructor = inductive * int -(* *_env modules consider an order on user part of names +(** *_env modules consider an order on user part of names the others consider an order on canonical part of names*) module Cmap : Map.S with type key = constant module Cmap_env : Map.S with type key = constant @@ -191,7 +195,7 @@ val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool val eq_constructor : constructor -> constructor -> bool -(* Better to have it here that in Closure, since required in grammar.cma *) +(** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = | EvalVarRef of identifier | EvalConstRef of constant @@ -199,7 +203,7 @@ type evaluable_global_reference = val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool -(* Hash-consing *) +(** Hash-consing *) val hcons_names : unit -> (constant -> constant) * (mutual_inductive -> mutual_inductive) * (dir_path -> dir_path) * @@ -220,8 +224,8 @@ val full_transparent_state : transparent_state val var_full_transparent_state : transparent_state val cst_full_transparent_state : transparent_state -type inv_rel_key = int (* index in the [rel_context] part of environment - starting by the end, {\em inverse} +type inv_rel_key = int (** index in the [rel_context] part of environment + starting by the end, {e inverse} of de Bruijn indice *) type id_key = inv_rel_key tableKey |