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

4 files changed, 31 insertions, 15 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index b44cabe8b..90432a4a4 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -66,14 +66,20 @@ let gen_constant_in_modules locstr dirs s =
 let check_required_library d =
   let d' = List.map id_of_string d in
   let dir = make_dirpath (List.rev d') in
+  let mp = (fst(Lib.current_prefix())) in
+  let current_dir = match mp with
+    | MPfile dp -> (dir=dp)
+    | _ -> false
+  in
   if not (Library.library_is_loaded dir) then
+    if not current_dir then
 (* Loading silently ...
     let m, prefix = list_sep_last d' in
     read_library
      (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
 *)
 (* or failing ...*)
-    error ("Library "^(string_of_dirpath dir)^" has to be required first.")
+      error ("Library "^(string_of_dirpath dir)^" has to be required first.")
 
 (************************************************************************)
 (* Specific Coq objects *)
@@ -123,7 +129,7 @@ let jmeq_module_name = ["Coq";"Logic";"JMeq"]
 let jmeq_module = make_dir jmeq_module_name
 
 (* TODO: temporary hack *)
-let make_kn dir id = Libnames.encode_kn dir id
+let make_kn dir id = Libnames.encode_mind dir id
 let make_con dir id = Libnames.encode_con dir id
 
 (** Identity *)
diff --git a/interp/notation.ml b/interp/notation.ml
index 342cb6c9c..8f9f0959d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -109,7 +109,7 @@ let open_scope i (_,(local,op,sc)) =
 let cache_scope o =
   open_scope 1 o
 
-let subst_scope (_,subst,sc) = sc
+let subst_scope (subst,sc) = sc
 
 open Libobject
 
@@ -180,19 +180,29 @@ type key =
 let notations_key_table = ref Gmapl.empty
 let prim_token_key_table = Hashtbl.create 7
 
+
+let make_gr = function
+  | ConstRef con -> 
+      ConstRef(constant_of_kn(canonical_con con))
+  | IndRef (kn,i) ->
+      IndRef(mind_of_kn(canonical_mind kn),i)
+  | ConstructRef ((kn,i),j )->
+      ConstructRef((mind_of_kn(canonical_mind kn),i),j)
+  | VarRef id ->  VarRef id
+      
 let rawconstr_key = function
-  | RApp (_,RRef (_,ref),_) -> RefKey ref
-  | RRef (_,ref) -> RefKey ref
+  | RApp (_,RRef (_,ref),_) -> RefKey (make_gr ref)
+  | RRef (_,ref) -> RefKey (make_gr ref)
   | _ -> Oth
 
 let cases_pattern_key = function
-  | PatCstr (_,ref,_,_) -> RefKey (ConstructRef ref)
+  | PatCstr (_,ref,_,_) -> RefKey (make_gr (ConstructRef ref))
   | _ -> Oth
 
 let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
-  | AApp (ARef ref,args) -> RefKey ref, Some (List.length args)
-  | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey ref, Some (List.length args)
-  | ARef ref -> RefKey ref, None
+  | AApp (ARef ref,args) -> RefKey(make_gr ref), Some (List.length args)
+  | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey (make_gr ref), Some (List.length args)
+  | ARef ref -> RefKey(make_gr ref), None
   | _ -> Oth, None
 
 (**********************************************************************)
@@ -458,7 +468,7 @@ let load_arguments_scope _ (_,(_,r,scl)) =
 let cache_arguments_scope o =
   load_arguments_scope 1 o
 
-let subst_arguments_scope (_,subst,(req,r,scl)) =
+let subst_arguments_scope (subst,(req,r,scl)) =
   (ArgsScopeNoDischarge,fst (subst_global subst r),scl)
 
 let discharge_arguments_scope (_,(req,r,l)) =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 939fe01aa..1330a3689 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -51,7 +51,7 @@ let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
 let cache_syntax_constant d =
   load_syntax_constant 1 d
 
-let subst_syntax_constant ((sp,kn),subst,(local,pat,onlyparse)) =
+let subst_syntax_constant (subst,(local,pat,onlyparse)) =
   (local,subst_interpretation subst pat,onlyparse)
 
 let classify_syntax_constant (local,_,_ as o) =
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index bea0eae31..ec1b20a12 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -143,7 +143,7 @@ let has_ldots =
     (function RApp (_,RVar(_,v),_) when v = ldots_var -> true | _ -> false)
 
 let compare_rawconstr f t1 t2 = match t1,t2 with
-  | RRef (_,r1), RRef (_,r2) -> r1 = r2
+  | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2 
   | RVar (_,v1), RVar (_,v2) -> v1 = v2
   | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2
   | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
@@ -281,7 +281,7 @@ let rec subst_pat subst pat =
   match pat with
   | PatVar _ -> pat
   | PatCstr (loc,((kn,i),j),cpl,n) ->
-      let kn' = subst_kn subst kn
+      let kn' = subst_ind subst kn
       and cpl' = list_smartmap (subst_pat subst) cpl in
         if kn' == kn && cpl' == cpl then pat else
           PatCstr (loc,((kn',i),j),cpl',n)
@@ -331,7 +331,7 @@ let rec subst_aconstr subst bound raw =
         (fun (a,(n,signopt) as x) ->
 	  let a' = subst_aconstr subst bound a in
 	  let signopt' = Option.map (fun ((indkn,i),n,nal as z) ->
-	    let indkn' = subst_kn subst indkn in
+	    let indkn' = subst_ind subst indkn in
 	    if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in
 	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
         rl
@@ -485,7 +485,7 @@ let adjust_application_n n loc f l =
 let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
   | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
-  | RRef (_,r1), ARef r2 when r1 = r2 -> sigma
+  | RRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma 
   | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
   | RApp (loc,f1,l1), AApp (f2,l2) ->
       let n1 = List.length l1 and n2 = List.length l2 in