From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- kernel/names.mli | 92 ++++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 66 insertions(+), 26 deletions(-) (limited to 'kernel/names.mli') diff --git a/kernel/names.mli b/kernel/names.mli index 49b10bfe..632f3733 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: names.mli 11582 2008-11-12 19:49:57Z notin $ i*) +(*i $Id$ i*) (*s Identifiers *) @@ -39,25 +39,13 @@ val empty_dirpath : dir_path (* 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 - signatures - invisible for users *) -type label -type mod_self_id - -(* 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 -val id_of_msid : mod_self_id -> identifier -val label_of_msid : mod_self_id -> label -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 +type label (*s Unique names for bound modules *) type mod_bound_id +(* The first argument is a file name - to prevent conflict between + different files *) val make_mbid : dir_path -> string -> mod_bound_id val repr_mbid : mod_bound_id -> int * string * dir_path val id_of_mbid : mod_bound_id -> identifier @@ -80,9 +68,9 @@ module Labmap : Map.S with type key = label type module_path = | MPfile of dir_path | MPbound of mod_bound_id - | MPself of mod_self_id + (* | MPapp of module_path * module_path very soon *) | MPdot of module_path * label -(*i | MPapply of module_path * module_path in the future (maybe) i*) + val check_bound_mp : module_path -> bool @@ -91,13 +79,12 @@ 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 *) -val initial_msid : mod_self_id -val initial_path : module_path (* [= MPself initial_msid] *) - (* Initial "seed" of the unique identifier generator *) val initial_dir : dir_path +(* Name of the toplevel structure *) +val initial_path : module_path (* [= MPfile initial_dir] *) + (*s The absolute names of objects seen by kernel *) type kernel_name @@ -122,25 +109,64 @@ module KNmap : Map.S with type key = kernel_name type variable = identifier type constant -type mutual_inductive = kernel_name +type mutual_inductive (* Beware: first inductive has index 0 *) type inductive = mutual_inductive * int (* Beware: first constructor has index 1 *) type constructor = inductive * int +(* *_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 module Cpred : Predicate.S with type elt = constant module Cset : Set.S with type elt = constant +module Cset_env : Set.S with type elt = constant +module Mindmap : Map.S with type key = mutual_inductive +module Mindmap_env : Map.S with type key = mutual_inductive +module Mindset : Set.S with type elt = mutual_inductive module Indmap : Map.S with type key = inductive module Constrmap : Map.S with type key = constructor +module Indmap_env : Map.S with type key = inductive +module Constrmap_env : Map.S with type key = constructor val constant_of_kn : kernel_name -> constant +val constant_of_kn_equiv : kernel_name -> kernel_name -> constant val make_con : module_path -> dir_path -> label -> constant +val make_con_equiv : module_path -> module_path -> dir_path + -> label -> constant +val user_con : constant -> kernel_name +val canonical_con : constant -> kernel_name val repr_con : constant -> module_path * dir_path * label +val eq_constant : constant -> constant -> bool + val string_of_con : constant -> string val con_label : constant -> label val con_modpath : constant -> module_path val pr_con : constant -> Pp.std_ppcmds +val debug_pr_con : constant -> Pp.std_ppcmds +val debug_string_of_con : constant -> string + + + +val mind_of_kn : kernel_name -> mutual_inductive +val mind_of_kn_equiv : kernel_name -> kernel_name -> mutual_inductive +val make_mind : module_path -> dir_path -> label -> mutual_inductive +val make_mind_equiv : module_path -> module_path -> dir_path + -> label -> mutual_inductive +val user_mind : mutual_inductive -> kernel_name +val canonical_mind : mutual_inductive -> kernel_name +val repr_mind : mutual_inductive -> module_path * dir_path * label +val eq_mind : mutual_inductive -> mutual_inductive -> bool + +val string_of_mind : mutual_inductive -> string +val mind_label : mutual_inductive -> label +val mind_modpath : mutual_inductive -> module_path +val pr_mind : mutual_inductive -> Pp.std_ppcmds +val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds +val debug_string_of_mind : mutual_inductive -> string + + val mind_modpath : mutual_inductive -> module_path val ind_modpath : inductive -> module_path @@ -150,16 +176,21 @@ val ith_mutual_inductive : inductive -> int -> inductive val ith_constructor_of_inductive : inductive -> int -> constructor val inductive_of_constructor : constructor -> inductive 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 *) type evaluable_global_reference = | EvalVarRef of identifier | EvalConstRef of constant +val eq_egr : evaluable_global_reference -> evaluable_global_reference + -> bool + (* Hash-consing *) val hcons_names : unit -> (constant -> constant) * - (kernel_name -> kernel_name) * (dir_path -> dir_path) * + (mutual_inductive -> mutual_inductive) * (dir_path -> dir_path) * (name -> name) * (identifier -> identifier) * (string -> string) @@ -168,7 +199,7 @@ val hcons_names : unit -> type 'a tableKey = | ConstKey of constant | VarKey of identifier - | RelKey of 'a + | RelKey of 'a type transparent_state = Idpred.t * Cpred.t @@ -178,7 +209,16 @@ 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} + starting by the end, {\em inverse} of de Bruijn indice *) type id_key = inv_rel_key tableKey + +val eq_id_key : id_key -> id_key -> bool + +(*equalities on constant and inductive + names for the checker*) + +val eq_con_chk : constant -> constant -> bool +val eq_ind_chk : inductive -> inductive -> bool + -- cgit v1.2.3