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, 51 insertions, 2 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 0a18978327..2808973fa6 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -124,6 +124,9 @@ let rec check_modpath_equiv env mp1 mp2 =
 
 
 let rec subst_modtype sub = function
+    (* This is the case in which I am substituting a whole module.
+       For instance "Module M(X). Module N := X. End M". When I apply
+       M to M' I must substitute M' for X in "Module N := X". *)
   | MTBident ln -> MTBident (subst_kn sub ln)
   | MTBfunsig (arg_id, arg_b, body_b) ->
       if occur_mbid arg_id sub then failwith "capture";
@@ -149,16 +152,62 @@ and subst_signature sub sign =
 
 and subst_module sub mb =
   let mtb' = subst_modtype sub mb.msb_modtype in
+  (* This is similar to the previous case. In this case we have
+     a module M in a signature that is knows to be equivalent to a module M'
+     (because the signature is "K with Module M := M'") and we are substituting
+     M' with some M''. *)
   let mpo' = option_smartmap (subst_mp sub) mb.msb_equiv in
     if mtb'==mb.msb_modtype && mpo'==mb.msb_equiv then mb else
       { msb_modtype=mtb'; 
 	msb_equiv=mpo'; 
 	msb_constraints=mb.msb_constraints}
 
-
 let subst_signature_msid msid mp = 
   subst_signature (map_msid msid mp)
 
+let rec constants_of_specification env mp sign =
+ let aux res (l,elem) =
+  match elem with
+   | SPBconst cb -> (make_con mp empty_dirpath l)::res
+   | SPBmind _ -> res
+   | SPBmodule mb ->
+      (constants_of_modtype env (MPdot (mp,l))
+        (module_body_of_spec mb).mod_type) @ res
+   | SPBmodtype mtb -> res (* ???? *)
+ in
+  List.fold_left aux [] sign
+
+and constants_of_modtype env mp modtype =
+ match scrape_modtype env modtype with
+    MTBident _ -> anomaly "scrape_modtype does not work!"
+  | MTBsig (msid,sign) ->
+     constants_of_specification env mp
+      (subst_signature_msid msid mp sign)
+  | MTBfunsig _ -> []
+
+(* returns a resolver for kn that maps mbid to mp and then delta-expands
+   the obtained constants according to env *)
+let resolver_of_environment mbid modtype mp env =
+ let constants = constants_of_modtype env (MPbound mbid) modtype in
+ let resolve =
+  List.map
+   (fun con ->
+     let con' = replace_mp_in_con (MPbound mbid) mp con in
+     let constr =
+      try
+       let constant = lookup_constant con' env in
+        if constant.Declarations.const_opaque then
+         None
+        else
+         option_app Declarations.force
+          constant.Declarations.const_body
+      with Not_found -> assert false
+     in
+      con,constr
+   ) constants
+ in
+  Mod_subst.make_resolver resolve
+
 (* we assume that the substitution of "mp" into "msid" is already done
 (or unnecessary) *)
 let rec add_signature mp sign env = 
@@ -182,7 +231,6 @@ and add_module mp mb env =
       | MTBident _ -> anomaly "scrape_modtype does not work!"
       | MTBsig (msid,sign) -> 
 	  add_signature mp (subst_signature_msid msid mp sign) env
-
       | MTBfunsig _ -> env
 
 
@@ -247,3 +295,4 @@ and strengthen_sig env msid sign mp = match sign with
 	item::rest'
 
 let strengthen env mtb mp = strengthen_mtb env mp mtb
+