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, 12 insertions, 12 deletions

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 93fc2c2dc..107b5368f 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -122,7 +122,7 @@ let find_projections = function Record l -> l | _ -> raise NoRecord
 
 let kn_sig =
   let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
-  make_kn specif empty_dirpath (mk_label "sig")
+  make_mind specif empty_dirpath (mk_label "sig")
 
 let rec pp_type par vl t =
   let rec pp_rec par = function
@@ -380,7 +380,7 @@ let pp_Dfix (rv,c,t) =
 let pp_equiv param_list name = function
   | NoEquiv, _ -> mt ()
   | Equiv kn, i ->
-      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (kn,i))
+      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (mind_of_kn kn,i))
   | RenEquiv ren, _  ->
       str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
 
@@ -408,7 +408,7 @@ let pp_logical_ind packet =
   fnl ()
 
 let pp_singleton kn packet =
-  let name = pp_global Type (IndRef (kn,0)) in
+  let name = pp_global Type (IndRef (mind_of_kn kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
   hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
@@ -416,7 +416,7 @@ let pp_singleton kn packet =
 		     pr_id packet.ip_consnames.(0)))
 
 let pp_record kn projs ip_equiv packet =
-  let name = pp_global Type (IndRef (kn,0)) in
+  let name = pp_global Type (IndRef (mind_of_kn kn,0)) in
   let projnames = List.map (pp_global Term) projs in
   let l = List.combine projnames packet.ip_types.(0) in
   let pl = rename_tvars keywords packet.ip_vars in
@@ -438,20 +438,20 @@ let pp_ind co kn ind =
   let init= ref (str "type ") in
   let names =
     Array.mapi (fun i p -> if p.ip_logical then mt () else
-		  pp_global Type (IndRef (kn,i)))
+		  pp_global Type (IndRef (mind_of_kn kn,i)))
       ind.ind_packets
   in
   let cnames =
     Array.mapi
       (fun i p -> if p.ip_logical then [||] else
-	 Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1)))
+	 Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((mind_of_kn kn,i),j+1)))
 	   p.ip_types)
       ind.ind_packets
   in
   let rec pp i =
     if i >= Array.length ind.ind_packets then mt ()
     else
-      let ip = (kn,i) in
+      let ip = (mind_of_kn kn,i) in
       let ip_equiv = ind.ind_equiv, i in
       let p = ind.ind_packets.(i) in
       if is_custom (IndRef ip) then pp (i+1)
@@ -601,12 +601,12 @@ and pp_module_type ol = function
       let name = pp_modname (MPbound mbid) in
       let def = pp_module_type None mt' in
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
-  | MTsig (msid, sign) ->
+  | MTsig (mp1, sign) ->
       let tvm = top_visible_mp () in
-      let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
+      let mp = match ol with None -> mp1 | Some l -> MPdot (tvm,l) in
       (* References in [sign] are in short form (relative to [msid]).
 	 In push_visible, [msid-->mp] is added to the current subst. *)
-      push_visible mp (Some msid);
+      push_visible mp (Some mp1);
       let l = map_succeed pp_specif sign in
       pop_visible ();
       str "sig " ++ fnl () ++
@@ -684,9 +684,9 @@ and pp_module_expr ol = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MEapply (me, me') ->
       pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")"
-  | MEstruct (msid, sel) ->
+  | MEstruct (mp, sel) ->
       let tvm = top_visible_mp () in
-      let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
+      let mp = match ol with None -> mp | Some l -> MPdot (tvm,l) in
       (* No need to update the subst with [Some msid] below : names are
 	 already in long form (see [subst_structure] in [Extract_env]). *)
       push_visible mp None;