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, 16 insertions, 23 deletions

diff --git a/checker/declarations.mli b/checker/declarations.mli
index 3d061b4c2c..bae7da9084 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -141,19 +141,18 @@ type mutual_inductive_body = {
   (* Universes constraints enforced by the inductive declaration *)
     mind_constraints : Univ.constraints;
 
-  (* Source of the inductive block when aliased in a module *)
-    mind_equiv : kernel_name option
   }
 
 (* Modules *)
 
 type substitution
+type delta_resolver
+val empty_delta_resolver : delta_resolver
 
 type structure_field_body =
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
-  | SFBalias of module_path * struct_expr_body option * Univ.constraints option
   | SFBmodtype of module_type_body
 
 and structure_body = (label * structure_field_body) list
@@ -161,32 +160,33 @@ and structure_body = (label * structure_field_body) list
 and struct_expr_body =
   | SEBident of module_path
   | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body
-  | SEBstruct of mod_self_id * structure_body
-  | SEBapply of struct_expr_body * struct_expr_body
-      * Univ.constraints
+  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
+  | SEBstruct of structure_body
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path *
-      struct_expr_body option * Univ.constraints
+    With_module_body of identifier list * module_path
   | With_definition_body of  identifier list * constant_body
 
 and module_body =
-    { mod_expr : struct_expr_body option;
-      mod_type : struct_expr_body option;
+    { mod_mp : module_path;
+      mod_expr : struct_expr_body option; 
+      mod_type : struct_expr_body;
+      mod_type_alg : struct_expr_body option;
       mod_constraints : Univ.constraints;
-      mod_alias : substitution;
+      mod_delta : delta_resolver;
       mod_retroknowledge : action list}
 
 and module_type_body =
-    { typ_expr : struct_expr_body;
-      typ_strength : module_path option;
-      typ_alias : substitution}
+    { typ_mp : module_path;
+      typ_expr : struct_expr_body;
+      typ_expr_alg : struct_expr_body option ;
+      typ_constraints : Univ.constraints;
+      typ_delta :delta_resolver}
 
 (* Substitutions *)
 
 val fold_subst :
-  (mod_self_id -> module_path -> 'a -> 'a) ->
   (mod_bound_id -> module_path -> 'a -> 'a) ->
   (module_path -> module_path -> 'a -> 'a) ->
   substitution -> 'a -> 'a
@@ -194,10 +194,8 @@ val fold_subst :
 type 'a subst_fun = substitution -> 'a -> 'a
 
 val empty_subst : substitution
-val add_msid : mod_self_id -> module_path -> substitution -> substitution
 val add_mbid : mod_bound_id -> module_path -> substitution -> substitution
 val add_mp   : module_path -> module_path -> substitution -> substitution
-val map_msid : mod_self_id -> module_path -> substitution
 val map_mbid : mod_bound_id -> module_path -> substitution
 val map_mp   : module_path -> module_path -> substitution
 
@@ -206,14 +204,9 @@ val subst_mind : mutual_inductive_body subst_fun
 val subst_modtype : substitution -> module_type_body -> module_type_body
 val subst_struct_expr :  substitution -> struct_expr_body -> struct_expr_body
 val subst_structure : substitution -> structure_body -> structure_body
-val subst_signature_msid :
-  mod_self_id -> module_path -> structure_body -> structure_body
+val subst_module : substitution -> module_body -> module_body
 
 val join : substitution -> substitution -> substitution
-val join_alias : substitution -> substitution -> substitution
-val update_subst_alias : substitution -> substitution -> substitution
-val update_subst : substitution -> substitution -> substitution
-val subst_key : substitution -> substitution -> substitution
 
 (* Validation *)
 val val_eng : Obj.t -> unit