This big commit addresses two problems:

  1- Management of the name-space in a modular development / sharing of non-logical objects.
  2- Performance of atomic module operations (adding a module to the environment, subtyping ...).

1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P

Module M := P.

Module M.
 Include P.
 ...
End M.

Declare Module K : S with Module M := P.

In this 3 cases we don't want to be bothered by the duplication of names. 
Of course, M.foo delta reduce to P.foo but many non-logical features of coq 
do not work modulo conversion (they use eq_constr or constr_pat object). 
To engender a transparent name-space (ie using P.foo or M.foo is the same thing) 
we quotient the name-space by the equivalence relation on names induced by the 
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of 
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo). 
So:
*************************************************************************************
*  Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values   *
*************************************************************************************

Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free 
(also for a posteriori declaration of them, ex: a notation on M.foo will be 
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.


2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based 
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate 
several functors then we have bigger vo.


Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 110 insertions, 27 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 0d61a29aa..06ca87b4d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -108,7 +108,7 @@ 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
@@ -119,7 +119,9 @@ 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 *)
@@ -172,6 +174,28 @@ let kn_ord kn1 kn2 =
 	  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
@@ -181,47 +205,89 @@ 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 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
@@ -229,13 +295,24 @@ module ConstructorOrdered = struct
     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
@@ -281,24 +358,24 @@ module Hmod = Hashcons.Make(
     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(
-  struct
-    type t = kernel_name
+
+module Hcn = Hashcons.Make(
+  struct 
+    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)
@@ -310,8 +387,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)
 
 
 (*******)
@@ -335,3 +413,8 @@ type inv_rel_key = int (* index in the [rel_context] part of environment
 
 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