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

3 files changed, 9 insertions, 8 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index f60abaf85..19473dfa6 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -21,7 +21,7 @@ open Bigint
 exception Non_closed_ascii
 
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let make_kn dir id = Libnames.encode_kn (make_dir dir) (id_of_string id)
+let make_kn dir id = Libnames.encode_mind (make_dir dir) (id_of_string id)
 let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
 
 let ascii_module = ["Coq";"Strings";"Ascii"]
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index e58618219..21b7115b6 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -24,7 +24,7 @@ let make_path dir id = Libnames.make_path (make_dir dir) (Names.id_of_string id)
 (* copied on g_zsyntax.ml, where it is said to be a temporary hack*)
 (* takes a path an identifier in the form of a string list and a string,
    returns a kernel_name *)
-let make_kn dir id = Libnames.encode_kn (make_dir dir) (Names.id_of_string id)
+let make_kn dir id = Libnames.encode_mind (make_dir dir) (Names.id_of_string id)
 
 
 (* int31 stuff *)
@@ -50,9 +50,10 @@ let zn2z_WW = ConstructRef ((zn2z_id "zn2z",0),2)
 let bigN_module = ["Coq"; "Numbers"; "Natural"; "BigN"; "BigN" ]
 let bigN_path = make_path (bigN_module@["BigN"]) "t"
 (* big ugly hack *)
-let bigN_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigN_module)),
-                             Names.mk_label "BigN")),
-              [], Names.id_of_string id) : Names.kernel_name)
+let bigN_id id = let kn =
+  ((Names.MPdot ((Names.MPfile (make_dir bigN_module)),
+                 Names.mk_label "BigN")),
+   [], Names.id_of_string id) in (Obj.magic (kn,kn) : Names.mutual_inductive)
 let bigN_scope = "bigN_scope"
 
 (* number of inlined level of bigN (actually the level 0 to n_inlined-1 are inlined) *)
@@ -81,9 +82,9 @@ let bigN_constructor =
 let bigZ_module = ["Coq"; "Numbers"; "Integer"; "BigZ"; "BigZ" ]
 let bigZ_path = make_path (bigZ_module@["BigZ"]) "t"
 (* big ugly hack bis *)
-let bigZ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)),
+let bigZ_id id =  let kn = ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)),
                              Names.mk_label "BigZ")),
-              [], Names.id_of_string id) : Names.kernel_name)
+              [], Names.id_of_string id) in (Obj.magic (kn,kn): Names.mutual_inductive)
 let bigZ_scope = "bigZ_scope"
 
 let bigZ_pos = ConstructRef ((bigZ_id "t_",0),1)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index a10c76013..f6afd080f 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -31,7 +31,7 @@ let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
 let positive_path = make_path positive_module "positive"
 
 (* TODO: temporary hack *)
-let make_kn dir id = Libnames.encode_kn dir id
+let make_kn dir id = Libnames.encode_mind dir id
 
 let positive_kn =
   make_kn (make_dir positive_module) (id_of_string "positive")