From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- kernel/names.ml | 133 +++++++++++++++++++++----------------------------------- 1 file changed, 50 insertions(+), 83 deletions(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index df3a012f..4c8cf7bb 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: names.ml,v 1.53.2.1 2004/07/16 19:30:26 herbelin Exp $ *) +(* $Id: names.ml 7834 2006-01-11 00:15:01Z herbelin $ *) open Pp open Util @@ -19,13 +19,7 @@ let id_ord = Pervasives.compare let id_of_string s = String.copy s -let map_ident id = - if Options.do_translate() then - match id with - "fix" -> "Fix" - | _ -> id - else id -let string_of_id id = String.copy (map_ident id) +let string_of_id id = String.copy id (* Hash-consing of identifier *) module Hident = Hashcons.Make( @@ -138,74 +132,6 @@ end module MPset = Set.Make(MPord) module MPmap = Map.Make(MPord) - -(* this is correct under the condition that bound and struct - identifiers can never be identical (i.e. get the same stamp)! *) - -type substitution = module_path Umap.t - -let empty_subst = Umap.empty - -let add_msid = Umap.add -let add_mbid = Umap.add - -let map_msid msid mp = add_msid msid mp empty_subst -let map_mbid mbid mp = add_msid mbid mp empty_subst - -let list_contents sub = - let one_pair uid mp l = - (string_of_uid uid, string_of_mp mp)::l - in - Umap.fold one_pair sub [] - -let debug_string_of_subst sub = - let l = List.map (fun (s1,s2) -> s1^"|->"^s2) (list_contents sub) in - "{" ^ String.concat "; " l ^ "}" - -let debug_pr_subst sub = - let l = list_contents sub in - let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2) - in - str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" - -let rec subst_mp sub mp = (* 's like subst *) - match mp with - | MPself sid -> - (try Umap.find sid sub with Not_found -> mp) - | MPbound bid -> - (try Umap.find bid sub with Not_found -> mp) - | MPdot (mp1,l) -> - let mp1' = subst_mp sub mp1 in - if mp1==mp1' then - mp - else - MPdot (mp1',l) - | _ -> mp - -let join subst1 subst2 = - let subst = Umap.map (subst_mp subst2) subst1 in - Umap.fold Umap.add subst2 subst - -let rec occur_in_path uid = function - | MPself sid -> sid = uid - | MPbound bid -> bid = uid - | MPdot (mp1,_) -> occur_in_path uid mp1 - | _ -> false - -let occur_uid uid sub = - let check_one uid' mp = - if uid = uid' || occur_in_path uid mp then raise Exit - in - try - Umap.iter check_one sub; - false - with Exit -> true - -let occur_msid = occur_uid -let occur_mbid = occur_uid - - - (* Kernel names *) type kernel_name = module_path * dir_path * label @@ -225,11 +151,6 @@ let string_of_kn (mp,dir,l) = let pr_kn kn = str (string_of_kn kn) -let subst_kn sub (mp,dir,l as kn) = - let mp' = subst_mp sub mp in - if mp==mp' then kn else (mp',dir,l) - - let kn_ord kn1 kn2 = let mp1,dir1,l1 = kn1 in let mp2,dir2,l2 = kn2 in @@ -252,7 +173,9 @@ end module KNmap = Map.Make(KNord) module KNpred = Predicate.Make(KNord) module KNset = Set.Make(KNord) - +module Cmap = KNmap +module Cpred = KNpred +module Cset = KNset let default_module_name = id_of_string "If you see this, it's a bug" @@ -267,11 +190,35 @@ type mutual_inductive = kernel_name type inductive = mutual_inductive * int type constructor = inductive * int +let constant_of_kn kn = kn +let make_con mp dir l = (mp,dir,l) +let repr_con con = con +let string_of_con = string_of_kn +let con_label = label +let pr_con = pr_kn +let con_modpath = modpath + let ith_mutual_inductive (kn,_) i = (kn,i) let ith_constructor_of_inductive ind i = (ind,i) let inductive_of_constructor (ind,i) = ind let index_of_constructor (ind,i) = i +module InductiveOrdered = struct + type t = inductive + let compare (spx,ix) (spy,iy) = + let c = ix - iy in if c = 0 then KNord.compare spx spy else c +end + +module Indmap = Map.Make(InductiveOrdered) + +module ConstructorOrdered = struct + type t = constructor + let compare (indx,ix) (indy,iy) = + let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c +end + +module Constrmap = Map.Make(ConstructorOrdered) + (* Better to have it here that in closure, since used in grammar.cma *) type evaluable_global_reference = | EvalVarRef of identifier @@ -352,4 +299,24 @@ let hcons_names () = let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in let hkn = Hashcons.simple_hcons Hkn.f (hmod,hdir,hstring) in - (hkn,hdir,hname,hident,hstring) + (hkn,hkn,hdir,hname,hident,hstring) + + +(*******) + +type transparent_state = Idpred.t * Cpred.t + +type 'a tableKey = + | ConstKey of constant + | VarKey of identifier + | RelKey of 'a + + +type inv_rel_key = int (* index in the [rel_context] part of environment + starting by the end, {\em inverse} + of de Bruijn indice *) + +type id_key = inv_rel_key tableKey + + + -- cgit v1.2.3