HUGE COMMIT

1. when applying a functor F(X) := B to a module M, the obtained module
   is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the
   body of t in M}. In principle it is now easy to fine tune the behaviour
   to choose whether b or M.t must be used. This change implies modifications
   both inside and outside the kernel.
2. for each object in the library it is now necessary to define the behaviour
   w.r.t. the substitution {X.t := b}. Notice that in many many cases the
   pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken
   (in the sense that it used to break several invariants). This commit
   fixes the behaviours for most of the objects, excluded
     a) coercions: a future commit should allow any term to be declared
        as a coercion; moreover the invariant that just a coercion path
        exists between two classes will be broken by the instantiation.
     b) global references when used as arguments of a few tactics/commands
   In all the other cases the behaviour implemented is the one that looks
   to me as the one expected by the user (if possible):
   [ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ]
     a) argument scopes: not expanded
     b) SYNTAXCONSTANT: expanded
     c) implicit arguments: not expanded
     d) coercions: expansion to be done (for now not expanded)
     e) concrete syntax tree for patterns: expanded
     f) concrete syntax tree for raw terms: expanded
     g) evaluable references (used by unfold, delta expansion, etc.): not
        expanded
     h) auto's hints: expanded when possible (i.e. when the expansion of the
        head of the pattern is rigid)
     i) realizers (for program extraction): nothing is done since the actual
        code does not look for the realizer of definitions with a body;
        however this solution is fragile.
     l) syntax and notation: expanded
     m) structures and canonical structures: an invariant says that no
        parameter can happear in them ==> the substitution always yelds the
        original term
     n) stuff related to V7 syntax: since this part of the code is doomed
        to disappear, I have made no effort to fix a reasonable semantics;
        not expanded is the default one applied
     o) RefArgTypes: to be understood. For now a warning is issued whether
        expanded != not expanded, and the not expanded solution is chosen.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 27 insertions, 11 deletions

diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index f4003c7f95..89491e2f91 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -8,22 +8,27 @@
 
 (*i $Id$ i*)
 
+(*s Mod_subst *)
+
 open Names
 open Term
 
-(*s Substitutions *)
-
+type resolver
 type substitution
 
+val make_resolver :  (constant * constr option) list -> resolver
+
 val empty_subst : substitution
 
 val add_msid : 
   mod_self_id -> module_path -> substitution -> substitution
 val add_mbid : 
-  mod_bound_id -> module_path -> substitution -> substitution
+  mod_bound_id -> module_path -> resolver option -> substitution -> substitution
 
-val map_msid : mod_self_id -> module_path -> substitution
-val map_mbid : mod_bound_id -> module_path -> substitution
+val map_msid :
+  mod_self_id -> module_path -> substitution
+val map_mbid :
+  mod_bound_id -> module_path -> resolver option -> substitution
 
 (* sequential composition: 
    [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
@@ -47,18 +52,29 @@ val debug_pr_subst : substitution -> Pp.std_ppcmds
 val subst_mp : 
   substitution -> module_path -> module_path
 
-(* [occur_*id id sub] returns true iff [id] occurs in [sub] 
-   on either side *)
+val subst_kn :
+  substitution -> kernel_name -> kernel_name
 
-val occur_msid : mod_self_id -> substitution -> bool
-val occur_mbid : mod_bound_id -> substitution -> bool
+val subst_con :
+  substitution -> constant -> constant * constr
 
-val subst_kn : substitution -> kernel_name -> kernel_name
-val subst_con : substitution -> constant -> constant
+(* Here the semantics is completely unclear.
+   What does "Hint Unfold t" means when "t" is a parameter?
+   Does the user mean "Unfold X.t" or does she mean "Unfold y"
+   where X.t is later on instantiated with y? I choose the first
+   interpretation (i.e. an evaluable reference is never expanded). *)
 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
 
 (* [subst_mps sub c] performs the substitution [sub] on all kernel
    names appearing in [c] *)
 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