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, 29 insertions, 18 deletions

diff --git a/library/global.ml b/library/global.ml
index e228de23a..6d7942ec0 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -48,14 +48,6 @@ let push_named_def d =
   global_env := env;
   cst
 
-(*let add_thing add kn thing =
-  let _,dir,l = repr_kn kn in
-  let kn',newenv = add dir l thing !global_env in
-    if kn = kn' then
-      global_env := newenv
-    else
-      anomaly "Kernel names do not match."
-*)
 
 let add_thing add dir id thing =
   let kn, newenv = add dir (label_of_id id) thing !global_env in
@@ -65,14 +57,23 @@ let add_thing add dir id thing =
 let add_constant = add_thing add_constant
 let add_mind = add_thing add_mind
 let add_modtype = add_thing (fun _ -> add_modtype) ()
-let add_module = add_thing (fun _ -> add_module) ()
-let add_alias = add_thing (fun _ -> add_alias) ()
+
+
+let add_module id me =
+  let l = label_of_id id in
+  let mp,resolve,new_env = add_module l me !global_env in
+    global_env := new_env;
+    mp,resolve
+    
 
 let add_constraints c = global_env := add_constraints c !global_env
 
 let set_engagement c = global_env := set_engagement c !global_env
 
-let add_include me = global_env := add_include me !global_env
+let add_include me is_module =
+  let resolve,newenv = add_include me is_module !global_env in
+    global_env := newenv;
+    resolve
 
 let start_module id =
   let l = label_of_id id in
@@ -82,15 +83,16 @@ let start_module id =
 
 let end_module fs id mtyo =
   let l = label_of_id id in
-  let mp,newenv = end_module l mtyo !global_env in
+  let mp,resolve,newenv = end_module l mtyo !global_env in
     Summary.unfreeze_summaries fs;
     global_env := newenv;
-    mp
+    mp,resolve
 
 
 let add_module_parameter mbid mte =
-  let newenv = add_module_parameter mbid mte !global_env in
-    global_env := newenv
+  let resolve,newenv = add_module_parameter mbid mte !global_env in
+    global_env := newenv;
+    resolve
 
 
 let start_modtype id =
@@ -117,15 +119,22 @@ let lookup_mind kn = lookup_mind kn (env())
 let lookup_module mp = lookup_module mp (env())
 let lookup_modtype kn = lookup_modtype kn (env())
 
+let constant_of_delta con = 
+  let resolver,resolver_param = (delta_of_senv !global_env) in
+    Mod_subst.constant_of_delta resolver_param
+      (Mod_subst.constant_of_delta resolver con)
 
-
-
+let mind_of_delta mind = 
+  let resolver,resolver_param = (delta_of_senv !global_env) in
+    Mod_subst.mind_of_delta resolver_param
+      (Mod_subst.mind_of_delta resolver mind)
+	
 let start_library dir =
   let mp,newenv = start_library dir !global_env in
     global_env := newenv;
     mp
 
-let export s = snd (export !global_env s)
+let export s = export !global_env s
 
 let import cenv digest =
   let mp,newenv = import cenv digest !global_env in
@@ -161,3 +170,5 @@ let register field value by_clause =
   let entry = kind_of_term value in
   let senv = Safe_typing.register !global_env field entry by_clause in
   global_env := senv
+
+