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

2 files changed, 17 insertions, 17 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 12a3bb572e..f96a94fb42 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -425,7 +425,7 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
       | (_,"CONSTANT") ->
 	  Some (print_constant with_values sep (constant_of_kn kn))
       | (_,"INDUCTIVE") ->
-	  Some (gallina_print_inductive kn)
+	  Some (gallina_print_inductive (mind_of_kn kn))
       | (_,"MODULE") ->
 	  let (mp,_,l) = repr_kn kn in
 	    Some (print_module with_values (MPdot (mp,l)))
@@ -540,7 +540,7 @@ let print_full_pure_context () =
   | ((_,kn),Lib.Leaf lobj)::rest ->
       let pp = match object_tag lobj with
       | "CONSTANT" ->
-	  let con = constant_of_kn kn in
+	  let con = Global.constant_of_delta (constant_of_kn kn) in
 	  let cb = Global.lookup_constant con in
 	  let val_0 = cb.const_body in
 	  let typ = ungeneralized_type_of_constant_type cb.const_type in
@@ -559,9 +559,10 @@ let print_full_pure_context () =
 		  str "  : " ++ pr_ltype typ ++ cut () ++ str " := " ++
 		  print_body val_0) ++ str "." ++ fnl () ++ fnl ()
       | "INDUCTIVE" ->
-	  let (mib,mip) = Global.lookup_inductive (kn,0) in
+	  let mind = Global.mind_of_delta (mind_of_kn kn) in
+	  let (mib,mip) = Global.lookup_inductive (mind,0) in
 	  let mipv = mib.mind_packets in
-	  let names = list_tabulate (fun x -> (kn,x)) (Array.length mipv) in
+	  let names = list_tabulate (fun x -> (mind,x)) (Array.length mipv) in
 	  pr_mutual_inductive mib.mind_finite names ++ str "." ++
 	  fnl () ++ fnl ()
       | "MODULE" ->
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index a5470a8924..80f05bf929 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -27,7 +27,7 @@ let rec print_local_modpath locals = function
   | MPbound mbid -> pr_id (List.assoc mbid locals)
   | MPdot(mp,l) ->
       print_local_modpath locals mp ++ str "." ++ pr_lab l
-  | MPself _ | MPfile _ -> raise Not_found
+  | MPfile _ -> raise Not_found
 
 let print_modpath locals mp =
   try (* must be with let because streams are lazy! *)
@@ -58,9 +58,10 @@ let rec print_module name locals with_body mb =
     | true, Some mexpr ->
 	spc () ++ str ":= " ++ print_modexpr locals mexpr
   in
-  let modtype = match mb.mod_type with
-      None -> str ""
-    | Some t -> spc () ++ str": " ++
+
+  let modtype = 
+    match mb.mod_type with
+    | t -> spc () ++ str": " ++ 
 	print_modtype locals t
   in
     hv 2 (str "Module " ++ name ++ modtype ++ body)
@@ -78,8 +79,8 @@ and print_modtype locals mty =
 		 pr_id (id_of_mbid mbid) ++ str " : " ++
 		 print_modtype locals mtb1.typ_expr ++
 		 str ")" ++ spc() ++ print_modtype locals' mtb2)
-  | SEBstruct (msid,sign) ->
-      hv 2 (str "Sig" ++ spc () ++ print_sig locals msid sign ++ brk (1,-2) ++ str "End")
+  | SEBstruct (sign) -> 
+      hv 2 (str "Sig" ++ spc () ++ print_sig locals  sign ++ brk (1,-2) ++ str "End")
   | SEBapply (mexpr,marg,_) ->
       let lapp = flatten_app mexpr [marg] in
       let fapp = List.hd lapp in
@@ -90,31 +91,29 @@ and print_modtype locals mty =
       let s = (String.concat "." (List.map string_of_id idl)) in
       hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++
 	       str "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
-  | SEBwith(seb,With_module_body(idl,mp,_,_))->
+  | SEBwith(seb,With_module_body(idl,mp))->
       let s =(String.concat "." (List.map string_of_id idl)) in
       hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++
 	       str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
 
-and print_sig locals msid sign =
+and print_sig locals sign = 
   let print_spec (l,spec) = (match spec with
     | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition "
     | SFBconst {const_body=None}
     | SFBconst {const_opaque=true} -> str "Parameter "
     | SFBmind _ -> str "Inductive "
     | SFBmodule _ -> str "Module "
-    | SFBalias (mp,_,_) -> str "Module "
     | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
   in
     prlist_with_sep spc print_spec sign
 
-and print_struct locals msid struc =
+and print_struct locals struc = 
   let print_body (l,body) = (match body with
     | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition "
     | SFBconst {const_body=Some _; const_opaque=true} -> str "Theorem "
     | SFBconst {const_body=None} -> str "Parameter "
     | SFBmind _ -> str "Inductive "
     | SFBmodule _ -> str "Module "
-    | SFBalias (mp,_,_) -> str "Module "
     | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
   in
     prlist_with_sep spc print_body struc
@@ -128,8 +127,8 @@ and print_modexpr locals mexpr = match mexpr with
       hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++
 	     str ":" ++ print_modtype locals mty.typ_expr ++
       str ")" ++ spc () ++ print_modexpr locals' mexpr)
-  | SEBstruct (msid, struc) ->
-      hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End")
+  | SEBstruct ( struc) -> 
+      hv 2 (str "Struct" ++ spc () ++ print_struct locals struc ++ brk (1,-2) ++ str "End")
   | SEBapply (mexpr,marg,_) ->
       let lapp = flatten_app mexpr [marg] in
 	hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr locals) lapp ++ str")")