Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 137 insertions, 68 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index b4dcd7c8..4e444985 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: names.ml 11750 2009-01-05 20:47:34Z herbelin $ *)
+(* $Id$ *)
 
 open Pp
 open Util
@@ -23,7 +23,7 @@ let string_of_id id = String.copy id
 
 (* Hash-consing of identifier *)
 module Hident = Hashcons.Make(
-  struct 
+  struct
     type t = string
     type u = string -> string
     let hash_sub hstr id = hstr id
@@ -31,7 +31,7 @@ module Hident = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
-module IdOrdered = 
+module IdOrdered =
   struct
     type t = identifier
     let compare = id_ord
@@ -47,17 +47,11 @@ type name = Name of identifier | Anonymous
 
 (* 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
 
-module ModIdOrdered = 
-  struct
-    type t = identifier
-    let compare = Pervasives.compare
-  end
-
-module ModIdmap = Map.Make(ModIdOrdered)
+module ModIdmap = Idmap
 
 let make_dirpath x = x
 let repr_dirpath x = x
@@ -69,30 +63,21 @@ let string_of_dirpath = function
   | sl -> String.concat "." (List.map string_of_id (List.rev sl))
 
 
-let u_number = ref 0 
+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)
  let debug_string_of_uid (i,s,p) =
  "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
-let string_of_uid (i,s,p) = 
+let string_of_uid (i,s,p) =
   string_of_dirpath p ^"."^s
 
-module Umap = Map.Make(struct 
-			 type t = uniq_ident 
+module Umap = Map.Make(struct
+			 type t = uniq_ident
 			 let compare = Pervasives.compare
 		       end)
 
 type label = string
 
-type mod_self_id = uniq_ident
-let make_msid = make_uid
-let repr_msid (n, id, dp) = (n, id, dp)
-let debug_string_of_msid = debug_string_of_uid
-let refresh_msid (_,s,dir) = make_uid dir s
-let string_of_msid = string_of_uid
-let id_of_msid (_,s,_) = s
-let label_of_msid (_,s,_) = s
-
 type mod_bound_id = uniq_ident
 let make_mbid = make_uid
 let repr_mbid (n, id, dp) = (n, id, dp)
@@ -114,10 +99,9 @@ module Labmap = Idmap
 type module_path =
   | MPfile of dir_path
   | MPbound of mod_bound_id
-  | MPself of mod_self_id 
+ (* | MPapp of module_path * module_path *)
   | MPdot of module_path * label
 
-
 let rec check_bound_mp = function
   | MPbound _ -> true
   | MPdot(mp,_) ->check_bound_mp mp
@@ -126,12 +110,14 @@ let rec check_bound_mp = function
 let rec string_of_mp = function
   | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")"
   | MPbound uid -> string_of_uid uid
-  | MPself 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 *)
 let rec mp_ord mp1 mp2 = match (mp1,mp2) with
-    MPdot(mp1,l1), MPdot(mp2,l2) -> 
+    MPdot(mp1,l1), MPdot(mp2,l2) ->
       let c = Pervasives.compare l1 l2 in
 	if c<>0 then
 	  c
@@ -154,31 +140,53 @@ type kernel_name = module_path * dir_path * label
 let make_kn mp dir l = (mp,dir,l)
 let repr_kn kn = kn
 
-let modpath kn = 
+let modpath kn =
   let mp,_,_ = repr_kn kn in mp
 
-let label kn = 
+let label kn =
   let _,_,l = repr_kn kn in l
 
-let string_of_kn (mp,dir,l) = 
+let string_of_kn (mp,dir,l) =
   string_of_mp mp ^ "#" ^ string_of_dirpath dir ^ "#" ^ string_of_label l
 
 let pr_kn kn = str (string_of_kn kn)
 
 
-let kn_ord kn1 kn2 = 
+let kn_ord kn1 kn2 =
     let mp1,dir1,l1 = kn1 in
     let mp2,dir2,l2 = kn2 in
     let c = Pervasives.compare l1 l2 in
       if c <> 0 then
 	c
-      else 
+      else
 	let c = Pervasives.compare dir1 dir2 in
 	  if c<>0 then
-	    c 
+	    c
 	  else
 	    MPord.compare mp1 mp2
 
+(* 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 
+   kn1 \rhd_{\delta}^* kn2 \rhd_{\delta} t *)
+type constant = kernel_name*kernel_name
+
+(* 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 *)
+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
@@ -188,64 +196,115 @@ 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
+
+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_msid = (make_msid initial_dir "If you see this, it's a bug")
-let initial_path = MPself initial_msid
+let initial_path = MPfile initial_dir
 
 type variable = identifier
-type constant = kernel_name
-type mutual_inductive = kernel_name
+
+(* 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
-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 mind_modpath = modpath
+let constant_of_kn kn = (kn,kn)
+let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
+let make_con mp dir l = ((mp,dir,l),(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_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))
+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 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
+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 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
+  let compare (spx,ix) (spy,iy) =
+    let c = ix - iy in if c = 0 then Canonical_ord.compare spx spy else c
+end
+
+module InductiveOrdered_env = struct
+  type t = inductive
+  let compare (spx,ix) (spy,iy) =
+    let c = ix - iy in if c = 0 then User_ord.compare spx spy else c
 end
 
 module Indmap = Map.Make(InductiveOrdered)
+module Indmap_env = Map.Make(InductiveOrdered_env)
 
 module ConstructorOrdered = struct
   type t = constructor
-  let compare (indx,ix) (indy,iy) = 
+  let compare (indx,ix) (indy,iy) =
     let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c
 end
 
+module ConstructorOrdered_env = struct
+  type t = constructor
+  let compare (indx,ix) (indy,iy) =
+    let c = ix - iy in if c = 0 then InductiveOrdered_env.compare indx indy else c
+end
+
 module Constrmap = Map.Make(ConstructorOrdered)
+module Constrmap_env = Map.Make(ConstructorOrdered_env)
 
 (* Better to have it here that in closure, since used in grammar.cma *)
 type evaluable_global_reference =
   | EvalVarRef of identifier
   | EvalConstRef of constant
 
+let eq_egr e1 e2 = match e1,e2 with
+    EvalConstRef con1, EvalConstRef con2 -> eq_constant con1 con2
+  | _,_ -> e1 = e2
+
 (* Hash-consing of name objects *)
 module Hname = Hashcons.Make(
-  struct 
+  struct
     type t = name
     type u = identifier -> identifier
     let hash_sub hident = function
@@ -260,7 +319,7 @@ module Hname = Hashcons.Make(
   end)
 
 module Hdir = Hashcons.Make(
-  struct 
+  struct
     type t = dir_path
     type u = identifier -> identifier
     let hash_sub hident d = List.map hident d
@@ -272,7 +331,7 @@ module Hdir = Hashcons.Make(
   end)
 
 module Huniqid = Hashcons.Make(
-  struct 
+  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)
@@ -281,31 +340,31 @@ module Huniqid = Hashcons.Make(
   end)
 
 module Hmod = Hashcons.Make(
-  struct 
+  struct
     type t = module_path
     type u = (dir_path -> dir_path) * (uniq_ident -> uniq_ident) *
 	(string -> string)
     let rec hash_sub (hdir,huniqid,hstr as hfuns) = function
       | MPfile dir -> MPfile (hdir dir)
       | MPbound m -> MPbound (huniqid m)
-      | MPself m -> MPself (huniqid m)
       | MPdot (md,l) -> MPdot (hash_sub hfuns md, hstr l)
     let rec equal d1 d2 = match (d1,d2) with
       | MPfile dir1, MPfile dir2 -> dir1 == dir2
       | MPbound m1, MPbound m2 -> m1 == m2
-      | MPself m1, MPself m2 -> m1 == m2
       | MPdot (mod1,l1), MPdot (mod2,l2) -> equal mod1 mod2 & l1 = l2
       | _ -> false
     let hash = Hashtbl.hash
   end)
 
-module Hkn = Hashcons.Make(
+
+module Hcn = Hashcons.Make(
   struct 
-    type t = kernel_name
+    type t = kernel_name*kernel_name
     type u = (module_path -> module_path)
 	* (dir_path -> dir_path) * (string -> string)
-    let hash_sub (hmod,hdir,hstr) (md,dir,l) = (hmod md, hdir dir, hstr l)
-    let equal (mod1,dir1,l1) (mod2,dir2,l2) =
+    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),_) =
       mod1 == mod2 && dir1 == dir2 && l1 == l2
     let hash = Hashtbl.hash
   end)
@@ -317,8 +376,9 @@ let hcons_names () =
   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 hkn = Hashcons.simple_hcons Hkn.f (hmod,hdir,hstring) in
-  (hkn,hkn,hdir,hname,hident,hstring)
+  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)
 
 
 (*******)
@@ -333,12 +393,21 @@ let cst_full_transparent_state = (Idpred.empty, Cpred.full)
 type 'a tableKey =
   | ConstKey of constant
   | VarKey of identifier
-  | RelKey of 'a 
+  | RelKey of 'a
 
 
 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
 
+let eq_id_key ik1 ik2 =
+  match ik1,ik2 with
+    ConstKey (_,kn1),
+      ConstKey (_,kn2) -> kn1=kn2
+    | a,b -> a=b
+
+let eq_con_chk (kn1,_) (kn2,_) = kn1=kn2
+let eq_mind_chk (kn1,_) (kn2,_) = kn1=kn2
+let eq_ind_chk (kn1,i1) (kn2,i2) = i1=i2&&eq_mind_chk kn1 kn2