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

diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index d30168a1b..a948d1647 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -13,26 +13,74 @@
 open Names
 open Term
 
-type resolver
+(* A delta_resolver maps name (constant, inductive, module_path) 
+   to canonical name  *)
+type delta_resolver
+
 type substitution
 
-val make_resolver :  (constant * constr option) list -> resolver
+val empty_delta_resolver : delta_resolver
+
+val add_inline_delta_resolver : constant -> delta_resolver -> delta_resolver
+
+val add_inline_constr_delta_resolver :  constant -> constr -> delta_resolver 
+  -> delta_resolver
+
+val add_constant_delta_resolver : constant -> delta_resolver -> delta_resolver
+
+val add_mind_delta_resolver : mutual_inductive -> delta_resolver -> delta_resolver
+
+val add_mp_delta_resolver : module_path -> module_path -> delta_resolver 
+  -> delta_resolver
+
+val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
+
+(* Apply the substitution on the domain of the resolver  *)
+val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver
+
+(* Apply the substitution on the codomain of the resolver  *)
+val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver
+
+val subst_dom_codom_delta_resolver : 
+  substitution -> delta_resolver -> delta_resolver
+
+(* *_of_delta return the associated name of arg2 in arg1   *)
+val constant_of_delta : delta_resolver -> constant -> constant
+
+val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
+
+val delta_of_mp : delta_resolver -> module_path -> module_path
+
+(* Extract the set of inlined constant in the resolver *)
+val inline_of_delta : delta_resolver -> kernel_name list
+
+(* remove_mp is used for the computation of a resolver induced by Include P *)
+val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver
+
+
+(* mem tests *)
+val mp_in_delta : module_path -> delta_resolver -> bool
+
+val con_in_delta : constant -> delta_resolver -> bool
+
+val mind_in_delta : mutual_inductive -> delta_resolver -> bool
+
+(*substitution*)
 
 val empty_subst : substitution
 
-val add_msid :
-  mod_self_id -> module_path -> substitution -> substitution
+(* add_* add [arg2/arg1]{arg3} to the substitution with no 
+   sequential composition  *)
 val add_mbid :
-  mod_bound_id -> module_path -> resolver option -> substitution -> substitution
+  mod_bound_id -> module_path -> delta_resolver  -> substitution -> substitution
 val add_mp :
-  module_path -> module_path -> substitution -> substitution
+  module_path -> module_path -> delta_resolver -> substitution -> substitution
 
-val map_msid :
-  mod_self_id -> module_path -> substitution
+(* map_* create a new substitution [arg2/arg1]{arg3} *)
 val map_mbid :
-  mod_bound_id -> module_path -> resolver option -> substitution
+  mod_bound_id -> module_path -> delta_resolver -> substitution
 val map_mp :
-  module_path -> module_path -> substitution
+  module_path -> module_path -> delta_resolver -> substitution
 
 (* sequential composition:
    [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
@@ -47,6 +95,8 @@ val subst_substituted : substitution -> 'a substituted -> 'a substituted
 (*i debugging *)
 val debug_string_of_subst : substitution -> string
 val debug_pr_subst : substitution -> Pp.std_ppcmds
+val debug_string_of_delta : delta_resolver -> string
+val debug_pr_delta : delta_resolver -> Pp.std_ppcmds
 (*i*)
 
 (* [subst_mp sub mp] guarantees that whenever the result of the
@@ -56,7 +106,10 @@ val debug_pr_subst : substitution -> Pp.std_ppcmds
 val subst_mp :
   substitution -> module_path -> module_path
 
-val subst_kn :
+val subst_ind :
+  substitution -> mutual_inductive -> mutual_inductive
+
+val subst_kn : 
   substitution -> kernel_name -> kernel_name
 
 val subst_con :
@@ -71,7 +124,7 @@ val subst_evaluable_reference :
   substitution -> evaluable_global_reference -> evaluable_global_reference
 
 (* [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *)
-val replace_mp_in_con : module_path -> module_path -> constant -> constant
+val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name
 
 (* [subst_mps sub c] performs the substitution [sub] on all kernel
    names appearing in [c] *)
@@ -80,15 +133,5 @@ val subst_mps : substitution -> constr -> constr
 (* [occur_*id id sub] returns true iff [id] occurs in [sub]
    on either side *)
 
-val occur_msid : mod_self_id -> substitution -> bool
 val occur_mbid : mod_bound_id -> substitution -> bool
 
-val update_subst_alias : substitution -> substitution -> substitution
-
-val update_subst : substitution -> substitution -> substitution
-
-val subst_key : substitution -> substitution -> substitution
-
-val join_alias : substitution -> substitution -> substitution
-
-val remove_alias : substitution -> substitution