From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- kernel/names.ml | 277 +++++++++++++++++++++++++++++++++----------------------- 1 file changed, 166 insertions(+), 111 deletions(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index 642f5562..ae8ad093 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1,35 +1,34 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* string - let hash_sub hstr id = hstr id - let equal id1 id2 = id1 == id2 - let hash = Hashtbl.hash - end) +let id_ord = Pervasives.compare module IdOrdered = struct @@ -38,15 +37,27 @@ module IdOrdered = end module Idset = Set.Make(IdOrdered) -module Idmap = Map.Make(IdOrdered) +module Idmap = +struct + include Map.Make(IdOrdered) + exception Finded + let exists f m = + try iter (fun a b -> if f a b then raise Finded) m ; false + with |Finded -> true + let singleton k v = add k v empty +end module Idpred = Predicate.Make(IdOrdered) -(* Names *) +(** {6 Various types based on identifiers } *) type name = Name of identifier | Anonymous +type variable = identifier -(* Dirpaths are lists of module identifiers. The actual representation - is reversed to optimise sharing: Coq.A.B is ["B";"A";"Coq"] *) +(** {6 Directory paths = section names paths } *) + +(** Dirpaths are lists of module identifiers. + The actual representation is reversed to optimise sharing: + Coq.A.B is ["B";"A";"Coq"] *) type module_ident = identifier type dir_path = module_ident list @@ -58,14 +69,17 @@ let repr_dirpath x = x let empty_dirpath = [] +(** Printing of directory paths as ["coq_root.module.submodule"] *) + let string_of_dirpath = function | [] -> "<>" | sl -> String.concat "." (List.map string_of_id (List.rev sl)) +(** {6 Unique names for bound modules } *) let u_number = ref 0 -type uniq_ident = int * string * dir_path -let make_uid dir s = incr u_number;(!u_number,String.copy s,dir) +type uniq_ident = int * identifier * dir_path +let make_uid dir s = incr u_number;(!u_number,s,dir) let debug_string_of_uid (i,s,p) = "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" let string_of_uid (i,s,p) = @@ -76,30 +90,31 @@ module Umap = Map.Make(struct let compare = Pervasives.compare end) -type label = string - type mod_bound_id = uniq_ident let make_mbid = make_uid let repr_mbid (n, id, dp) = (n, id, dp) let debug_string_of_mbid = debug_string_of_uid let string_of_mbid = string_of_uid let id_of_mbid (_,s,_) = s -let label_of_mbid (_,s,_) = s +(** {6 Names of structure elements } *) -let mk_label l = l -let string_of_label = string_of_id +type label = identifier +let mk_label = id_of_string +let string_of_label = string_of_id +let pr_label l = str (string_of_label l) let id_of_label l = l let label_of_id id = id module Labset = Idset module Labmap = Idmap +(** {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 *) | MPdot of module_path * label let rec check_bound_mp = function @@ -110,12 +125,9 @@ let rec check_bound_mp = function let rec string_of_mp = function | MPfile sl -> string_of_dirpath sl | MPbound uid -> string_of_uid uid - (* | MPapp (mp1,mp2) -> - "("^string_of_mp mp ^ " " ^ - string_of_mp mp^")"*) | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l -(* we compare labels first if both are MPdots *) +(** we compare labels first if both are MPdots *) let rec mp_ord mp1 mp2 = match (mp1,mp2) with MPdot(mp1,l1), MPdot(mp2,l2) -> let c = Pervasives.compare l1 l2 in @@ -133,7 +145,12 @@ end module MPset = Set.Make(MPord) module MPmap = Map.Make(MPord) -(* Kernel names *) +let default_module_name = "If you see this, it's a bug" + +let initial_dir = make_dirpath [default_module_name] +let initial_path = MPfile initial_dir + +(** {6 Kernel names } *) type kernel_name = module_path * dir_path * label @@ -147,11 +164,12 @@ let label kn = let _,_,l = repr_kn kn in l let string_of_kn (mp,dir,l) = - string_of_mp mp ^ "#" ^ string_of_dirpath dir ^ "#" ^ string_of_label l + let str_dir = if dir = [] then "." else "#" ^ string_of_dirpath dir ^ "#" + in + string_of_mp mp ^ str_dir ^ string_of_label l let pr_kn kn = str (string_of_kn kn) - let kn_ord kn1 kn2 = let mp1,dir1,l1 = kn1 in let mp2,dir2,l2 = kn2 in @@ -165,87 +183,84 @@ let kn_ord kn1 kn2 = else MPord.compare mp1 mp2 -(* a constant name is a kernel name couple (kn1,kn2) +module KNord = struct + type t = kernel_name + let compare = kn_ord +end + +module KNmap = Map.Make(KNord) +module KNpred = Predicate.Make(KNord) +module KNset = Set.Make(KNord) + +(** {6 Constant names } *) + +(** a constant name is a kernel name couple (kn1,kn2) where kn1 corresponds to the name used at toplevel - (i.e. what the user see) - and kn2 corresponds to the canonical kernel name - i.e. in the environment we have + (i.e. what the user see) + and kn2 corresponds to the canonical kernel name + i.e. in the environment we have kn1 \rhd_{\delta}^* kn2 \rhd_{\delta} t *) type constant = kernel_name*kernel_name -(* For the environment we distinguish constants by their - user part*) +let constant_of_kn kn = (kn,kn) +let constant_of_kn_equiv kn1 kn2 = (kn1,kn2) +let make_con mp dir l = constant_of_kn (mp,dir,l) +let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) +let canonical_con con = snd con +let user_con con = fst con +let repr_con con = fst con + +let eq_constant (_,kn1) (_,kn2) = kn1=kn2 + +let con_label con = label (fst con) +let con_modpath con = modpath (fst con) + +let string_of_con con = string_of_kn (fst con) +let pr_con con = str (string_of_con con) +let debug_string_of_con con = + "(" ^ string_of_kn (fst con) ^ "," ^ string_of_kn (snd con) ^ ")" +let debug_pr_con con = str (debug_string_of_con con) + +let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl = + if lbl = l1 && lbl = l2 then con + else ((mp1,dp1,lbl),(mp2,dp2,lbl)) + +(** For the environment we distinguish constants by their user part*) module User_ord = struct type t = kernel_name*kernel_name let compare x y= kn_ord (fst x) (fst y) end -(* For other uses (ex: non-logical things) it is enough - to deal with the canonical part *) +(** For other uses (ex: non-logical things) it is enough + to deal with the canonical part *) module Canonical_ord = struct type t = kernel_name*kernel_name let compare x y= kn_ord (snd x) (snd y) end - -module KNord = struct - type t = kernel_name - let compare =kn_ord -end - -module KNmap = Map.Make(KNord) -module KNpred = Predicate.Make(KNord) -module KNset = Set.Make(KNord) - module Cmap = Map.Make(Canonical_ord) module Cmap_env = Map.Make(User_ord) module Cpred = Predicate.Make(Canonical_ord) module Cset = Set.Make(Canonical_ord) module Cset_env = Set.Make(User_ord) -module Mindmap = Map.Make(Canonical_ord) -module Mindset = Set.Make(Canonical_ord) -module Mindmap_env = Map.Make(User_ord) - -let default_module_name = "If you see this, it's a bug" -let initial_dir = make_dirpath [default_module_name] -let initial_path = MPfile initial_dir +(** {6 Names of mutual inductive types } *) -type variable = identifier +(** The same thing is done for mutual inductive names + it replaces also the old mind_equiv field of mutual + inductive types *) +(** Beware: first inductive has index 0 *) +(** Beware: first constructor has index 1 *) -(* The same thing is done for mutual inductive names - it replaces also the old mind_equiv field of mutual - inductive types*) type mutual_inductive = kernel_name*kernel_name type inductive = mutual_inductive * int type constructor = inductive * int -let constant_of_kn kn = (kn,kn) -let constant_of_kn_equiv kn1 kn2 = (kn1,kn2) -let make_con mp dir l = constant_of_kn (mp,dir,l) -let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) -let canonical_con con = snd con -let user_con con = fst con -let repr_con con = fst con -let string_of_con con = string_of_kn (fst con) -let con_label con = label (fst con) -let pr_con con = pr_kn (fst con) -let debug_pr_con con = str "("++ pr_kn (fst con) ++ str ","++ pr_kn (snd con)++ str ")" -let eq_constant (_,kn1) (_,kn2) = kn1=kn2 -let debug_string_of_con con = string_of_kn (fst con)^"'"^string_of_kn (snd con) - -let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl = - if lbl = l1 && lbl = l2 then con - else ((mp1,dp1,lbl),(mp2,dp2,lbl)) - -let con_modpath con = modpath (fst con) - let mind_modpath mind = modpath (fst mind) let ind_modpath ind = mind_modpath (fst ind) let constr_modpath c = ind_modpath (fst c) - let mind_of_kn kn = (kn,kn) let mind_of_kn_equiv kn1 kn2 = (kn1,kn2) let make_mind mp dir l = ((mp,dir,l),(mp,dir,l)) @@ -253,12 +268,15 @@ let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) let canonical_mind mind = snd mind let user_mind mind = fst mind let repr_mind mind = fst mind -let string_of_mind mind = string_of_kn (fst mind) let mind_label mind= label (fst mind) -let pr_mind mind = pr_kn (fst mind) -let debug_pr_mind mind = str "("++ pr_kn (fst mind) ++ str ","++ pr_kn (snd mind)++ str ")" + let eq_mind (_,kn1) (_,kn2) = kn1=kn2 -let debug_string_of_mind mind = string_of_kn (fst mind)^"'"^string_of_kn (snd mind) + +let string_of_mind mind = string_of_kn (fst mind) +let pr_mind mind = str (string_of_mind mind) +let debug_string_of_mind mind = + "(" ^ string_of_kn (fst mind) ^ "," ^ string_of_kn (snd mind) ^ ")" +let debug_pr_mind con = str (debug_string_of_mind con) let ith_mutual_inductive (kn,_) i = (kn,i) let ith_constructor_of_inductive ind i = (ind,i) @@ -267,6 +285,10 @@ let index_of_constructor (ind,i) = i let eq_ind (kn1,i1) (kn2,i2) = i1=i2&&eq_mind kn1 kn2 let eq_constructor (kn1,i1) (kn2,i2) = i1=i2&&eq_ind kn1 kn2 +module Mindmap = Map.Make(Canonical_ord) +module Mindset = Set.Make(Canonical_ord) +module Mindmap_env = Map.Make(User_ord) + module InductiveOrdered = struct type t = inductive let compare (spx,ix) (spy,iy) = @@ -306,7 +328,8 @@ let eq_egr e1 e2 = match e1,e2 with EvalConstRef con1, EvalConstRef con2 -> eq_constant con1 con2 | _,_ -> e1 = e2 -(* Hash-consing of name objects *) +(** {6 Hash-consing of name objects } *) + module Hname = Hashcons.Make( struct type t = name @@ -326,7 +349,7 @@ module Hdir = Hashcons.Make( struct type t = dir_path type u = identifier -> identifier - let hash_sub hident d = List.map hident d + let hash_sub hident d = list_smartmap hident d let rec equal d1 d2 = match (d1,d2) with | [],[] -> true | id1::d1,id2::d2 -> id1 == id2 & equal d1 d2 @@ -337,9 +360,9 @@ module Hdir = Hashcons.Make( module Huniqid = Hashcons.Make( struct type t = uniq_ident - type u = (string -> string) * (dir_path -> dir_path) - let hash_sub (hstr,hdir) (n,s,dir) = (n,hstr s,hdir dir) - let equal (n1,s1,dir1) (n2,s2,dir2) = n1 = n2 & s1 = s2 & dir1 == dir2 + type u = (identifier -> identifier) * (dir_path -> dir_path) + let hash_sub (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) + let equal (n1,s1,dir1) (n2,s2,dir2) = n1 = n2 && s1 == s2 && dir1 == dir2 let hash = Hashtbl.hash end) @@ -355,34 +378,66 @@ module Hmod = Hashcons.Make( let rec equal d1 d2 = match (d1,d2) with | MPfile dir1, MPfile dir2 -> dir1 == dir2 | MPbound m1, MPbound m2 -> m1 == m2 - | MPdot (mod1,l1), MPdot (mod2,l2) -> equal mod1 mod2 & l1 = l2 + | MPdot (mod1,l1), MPdot (mod2,l2) -> l1 == l2 && equal mod1 mod2 | _ -> false let hash = Hashtbl.hash end) - -module Hcn = Hashcons.Make( - struct - type t = kernel_name*kernel_name +module Hkn = Hashcons.Make( + struct + type t = kernel_name type u = (module_path -> module_path) * (dir_path -> dir_path) * (string -> string) - let hash_sub (hmod,hdir,hstr) ((md,dir,l),(mde,dire,le)) = - ((hmod md, hdir dir, hstr l),(hmod mde, hdir dire, hstr le)) - let equal ((mod1,dir1,l1),_) ((mod2,dir2,l2),_) = + let hash_sub (hmod,hdir,hstr) (md,dir,l) = + (hmod md, hdir dir, hstr l) + let equal (mod1,dir1,l1) (mod2,dir2,l2) = mod1 == mod2 && dir1 == dir2 && l1 == l2 let hash = Hashtbl.hash end) -let hcons_names () = - let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in - let hident = Hashcons.simple_hcons Hident.f hstring in - let hname = Hashcons.simple_hcons Hname.f hident in - let hdir = Hashcons.simple_hcons Hdir.f hident in - let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in - let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in - let hmind = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in - let hcn = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in - (hcn,hmind,hdir,hname,hident,hstring) +(** For [constant] and [mutual_inductive], we discriminate only on + the user part : having the same user part implies having the + same canonical part (invariant of the system). *) + +module Hcn = Hashcons.Make( + struct + type t = kernel_name*kernel_name + type u = kernel_name -> kernel_name + let hash_sub hkn (user,can) = (hkn user, hkn can) + let equal (user1,_) (user2,_) = user1 == user2 + let hash (user,_) = Hashtbl.hash user + end) + +module Hind = Hashcons.Make( + struct + type t = inductive + type u = mutual_inductive -> mutual_inductive + let hash_sub hmind (mind, i) = (hmind mind, i) + let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && i1 = i2 + let hash = Hashtbl.hash + end) + +module Hconstruct = Hashcons.Make( + struct + type t = constructor + type u = inductive -> inductive + let hash_sub hind (ind, j) = (hind ind, j) + let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && j1 = j2 + let hash = Hashtbl.hash + end) + +let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.f () +let hcons_ident = hcons_string +let hcons_name = Hashcons.simple_hcons Hname.f hcons_ident +let hcons_dirpath = Hashcons.simple_hcons Hdir.f hcons_ident +let hcons_uid = Hashcons.simple_hcons Huniqid.f (hcons_ident,hcons_dirpath) +let hcons_mp = + Hashcons.simple_hcons Hmod.f (hcons_dirpath,hcons_uid,hcons_string) +let hcons_kn = Hashcons.simple_hcons Hkn.f (hcons_mp,hcons_dirpath,hcons_string) +let hcons_con = Hashcons.simple_hcons Hcn.f hcons_kn +let hcons_mind = Hashcons.simple_hcons Hcn.f hcons_kn +let hcons_ind = Hashcons.simple_hcons Hind.f hcons_mind +let hcons_construct = Hashcons.simple_hcons Hconstruct.f hcons_ind (*******) -- cgit v1.2.3