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

diff --git a/dev/db b/dev/db
index 8187857014..a355f62a99 100644
--- a/dev/db
+++ b/dev/db
@@ -11,6 +11,7 @@ install_printer Top_printers.ppdir
 install_printer Top_printers.ppmp
 install_printer Top_printers.ppkn
 install_printer Top_printers.ppcon
+install_printer Top_printers.ppmind
 install_printer Top_printers.ppsp
 install_printer Top_printers.ppqualid
 install_printer Top_printers.ppclindex
@@ -39,5 +40,5 @@ install_printer Top_printers.pptac
 install_printer Top_printers.ppobj
 install_printer Top_printers.pploc
 install_printer Top_printers.prsubst
-                                                  
-
+install_printer Top_printers.prdelta
+install_printer  Top_printers.print_pure_constr
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 107b2904aa..b5a54a1899 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -54,9 +54,9 @@ Mod_typing
 Safe_typing
 
 Summary
-Global
 Nameops
 Libnames
+Global
 Nametab
 Libobject
 Lib
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index d5ebde7cb0..310fb1188f 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -28,6 +28,7 @@ open Cerrors
 open Evd
 open Goptions
 open Genarg
+open Mod_subst
 
 
 let _ = Constrextern.print_evar_arguments := true
@@ -44,8 +45,9 @@ let ppmsid msid = pp (str (debug_string_of_msid msid))
 let ppmbid mbid = pp (str (debug_string_of_mbid mbid))
 let ppdir dir = pp (pr_dirpath dir)
 let ppmp mp = pp(str (string_of_mp mp))
-let ppcon con = pp(pr_con con)
+let ppcon con = pp(debug_pr_con con)
 let ppkn kn = pp(pr_kn kn)
+let ppmind kn = pp(debug_pr_mind kn)
 let ppsp sp = pp(pr_path sp)
 let ppqualid qid = pp(pr_qualid qid)
 let ppclindex cl = pp(Classops.pr_cl_index cl)
@@ -72,10 +74,10 @@ let ppidset l = pp (prset pr_id (Idset.elements l))
 let pP s = pp (hov 0 s)
 
 let safe_pr_global = function
-  | ConstRef kn -> pp (str "CONSTREF(" ++ pr_con kn ++ str ")")
-  | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++
+  | ConstRef kn -> pp (str "CONSTREF(" ++ debug_pr_con kn ++ str ")")
+  | IndRef (kn,i) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
 			  int i ++ str ")")
-  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++
+  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
 				      int i ++ str "," ++ int j ++ str ")")
   | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")")
 
@@ -92,6 +94,7 @@ let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
 let ppj j = pp (genppj pr_ljudge j)
 
 let prsubst s = pp (Mod_subst.debug_pr_subst s)
+let prdelta s = pp (Mod_subst.debug_pr_delta s)
 
 let pp_idpred s = pp (pr_idpred s)
 let pp_cpred s = pp (pr_cpred s)
@@ -159,9 +162,9 @@ let constr_display csr =
   | Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
   | Const c -> "Const("^(string_of_con c)^")"
   | Ind (sp,i) ->
-      "MutInd("^(string_of_kn sp)^","^(string_of_int i)^")"
+      "MutInd("^(string_of_mind sp)^","^(string_of_int i)^")"
   | Construct ((sp,i),j) ->
-      "MutConstruct(("^(string_of_kn sp)^","^(string_of_int i)^"),"
+      "MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^"),"
       ^(string_of_int j)^")"
   | Case (ci,p,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
@@ -309,7 +312,7 @@ let print_pure_constr csr =
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (string_of_kn sp)
+      print_string (debug_string_of_mind sp)
   and sp_con_display sp =
 (*    let dir,l = decode_kn sp in
     let ls =
@@ -318,7 +321,7 @@ let print_pure_constr csr =
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (string_of_con sp)
+      print_string (debug_string_of_con sp)
 
   in
     try
@@ -442,11 +445,11 @@ let raw_string_of_ref loc = function
       let (mp,dir,id) = repr_con cst in
       encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id)
   | IndRef (kn,i) ->
-      let (mp,dir,id) = repr_kn kn in
+      let (mp,dir,id) = repr_mind kn in
       encode_path loc "IND" (Some (mp,dir)) [id_of_label id]
 	(id_of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
-      let (mp,dir,id) = repr_kn kn in
+      let (mp,dir,id) = repr_mind kn in
       encode_path loc "CSTR" (Some (mp,dir))
 	[id_of_label id;id_of_string ("_"^string_of_int i)]
 	(id_of_string ("_"^string_of_int j))
@@ -456,13 +459,13 @@ let raw_string_of_ref loc = function
 let short_string_of_ref loc = function
   | VarRef id -> Ident (loc,id)
   | ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst)))
-  | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_kn kn)))
+  | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_mind kn)))
   | IndRef (kn,i) ->
-      encode_path loc "IND" None [id_of_label (pi3 (repr_kn kn))]
+      encode_path loc "IND" None [id_of_label (pi3 (repr_mind kn))]
         (id_of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
       encode_path loc "CSTR" None
-        [id_of_label (pi3 (repr_kn kn));id_of_string ("_"^string_of_int i)]
+        [id_of_label (pi3 (repr_mind kn));id_of_string ("_"^string_of_int i)]
         (id_of_string ("_"^string_of_int j))
 
 let _ = Constrextern.set_debug_global_reference_printer
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 266bd1043c..59545d8aa4 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -10,7 +10,7 @@ let ppripos (ri,pos) =
   | Reloc_annot a ->
       let sp,i = a.ci.ci_ind in
       print_string
-	("annot : MutInd("^(string_of_kn sp)^","^(string_of_int i)^")\n")
+	("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n")
   | Reloc_const _ ->
       print_string "structured constant\n"
   | Reloc_getglobal kn ->
@@ -62,7 +62,7 @@ and ppatom a =
   | Aid idk -> print_idkey idk
   | Aiddef(idk,_) -> print_string "&";print_idkey idk
   | Aind(sp,i) ->  print_string "Ind(";
-      print_string (string_of_kn sp);
+      print_string (string_of_mind sp);
       print_string ","; print_int i;
       print_string ")"