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

8 files changed, 260 insertions, 75 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 8e31f59761..cccb184433 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -255,7 +255,7 @@ let subst_patch s (ri,pos) =
       let ci = {a.ci with ci_ind = (subst_kn s kn,i)} in
       (Reloc_annot {a with ci = ci},pos)
   | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
-  | Reloc_getglobal kn -> (Reloc_getglobal (subst_con s kn), pos)
+  | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con s kn)), pos)
 
 let subst_to_patch s (code,pl,fv) = 
   code,List.rev_map (subst_patch s) pl,fv
@@ -267,7 +267,7 @@ type body_code =
 
 let subst_body_code s = function
   | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp)
-  | BCallias kn -> BCallias (subst_con s kn)
+  | BCallias kn -> BCallias (fst (subst_con s kn))
   | BCconstant -> BCconstant
 
 type to_patch_substituted = body_code substituted
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 48bb9933ce..e0d16d4995 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -13,6 +13,20 @@ open Util
 open Names
 open Term
 
+(* WARNING: not every constant in the associative list domain used to exist
+   in the environment. This allows a simple implementation of the join
+   operation. However, iterating over the associative list becomes a non-sense
+*)
+type resolver = (constant * constr option) list
+
+let make_resolver resolve = resolve
+
+let apply_opt_resolver resolve kn =
+ match resolve with
+    None -> None
+  | Some resolve ->
+     try List.assoc kn resolve with Not_found -> assert false
+
 type substitution_domain = MSI of mod_self_id | MBI of mod_bound_id
 
 let string_of_subst_domain = function
@@ -24,21 +38,21 @@ module Umap = Map.Make(struct
 			 let compare = Pervasives.compare
 		       end)
 
-(* this is correct under the condition that bound and struct
-   identifiers can never be identical (i.e. get the same stamp)! *) 
-
-type substitution = module_path Umap.t
+type substitution = (module_path * resolver option) Umap.t
 
 let empty_subst = Umap.empty
 
-let add_msid sid = Umap.add (MSI sid)
-let add_mbid bid = Umap.add (MBI bid)
+let add_msid msid mp =
+  Umap.add (MSI msid) (mp,None)
+let add_mbid mbid mp resolve =
+ let mp' = MBI mbid in
+  Umap.add (MBI mbid) (mp,resolve)
 
 let map_msid msid mp = add_msid msid mp empty_subst
-let map_mbid mbid mp = add_mbid mbid mp empty_subst
+let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst
 
 let list_contents sub = 
-  let one_pair uid mp l =
+  let one_pair uid (mp,_) l =
     (string_of_subst_domain uid, string_of_mp mp)::l
   in
     Umap.fold one_pair sub []
@@ -53,22 +67,155 @@ let debug_pr_subst sub =
   in
     str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" 
 
-let rec subst_mp sub mp = (* 's like subst *)
+let subst_mp0 sub mp = (* 's like subst *)
+ let rec aux mp =
   match mp with
     | MPself sid -> 
-	(try Umap.find (MSI sid) sub with Not_found -> mp)
+        let mp',resolve = Umap.find (MSI sid) sub in
+         mp',resolve
     | MPbound bid ->
-	(try Umap.find (MBI bid) sub with Not_found -> mp)
+        let mp',resolve = Umap.find (MBI bid) sub in
+         mp',resolve
+    | MPdot (mp1,l) -> 
+	let mp1',resolve = aux mp1 in
+	 MPdot (mp1',l),resolve
+    | _ -> raise Not_found
+ in
+  try Some (aux mp) with Not_found -> None
+
+let subst_mp sub mp =
+ match subst_mp0 sub mp with
+    None -> mp
+  | Some (mp',_) -> mp'
+
+
+let subst_kn0 sub kn =
+ let mp,dir,l = repr_kn kn in
+  match subst_mp0 sub mp with
+     Some (mp',_) ->
+      Some (make_kn mp' dir l)
+   | None -> None
+
+let subst_kn sub kn =
+ match subst_kn0 sub kn with
+    None -> kn
+  | Some kn' -> kn'
+
+let subst_con sub con =
+ let mp,dir,l = repr_con con in
+  match subst_mp0 sub mp with
+     None -> con,mkConst con
+   | Some (mp',resolve) ->
+      let con' = make_con mp' dir l in
+       match apply_opt_resolver resolve con with
+          None -> con',mkConst con'
+        | Some t -> con',t
+
+(* 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). *)
+let subst_evaluable_reference subst = function
+  | EvalVarRef id -> EvalVarRef id
+  | EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn))
+
+(* 
+This should be rewritten to prevent duplication of constr's when not
+necessary.
+For now, it uses map_constr and is rather ineffective
+*)
+
+let rec map_kn f f' c = 
+  let func = map_kn f f' in
+    match kind_of_term c with
+      | Const kn -> f' kn
+      | Ind (kn,i) -> 
+         (match f kn with
+             None -> c
+           | Some kn' ->
+	      mkInd (kn',i))
+      | Construct ((kn,i),j) -> 
+         (match f kn with
+             None -> c
+           | Some kn' ->
+	      mkConstruct ((kn',i),j))
+      | Case (ci,p,c,l) ->
+	  let ci' =
+           { ci with
+              ci_ind =
+               let (kn,i) = ci.ci_ind in
+                match f kn with None -> ci.ci_ind | Some kn' -> kn',i } in
+	  mkCase (ci', func p, func c, array_smartmap func l) 
+      | _ -> map_constr func c
+
+let subst_mps sub = 
+  map_kn (subst_kn0 sub) (fun con -> snd (subst_con sub con))
+
+let rec replace_mp_in_mp mpfrom mpto mp =
+  match mp with
+    | _ when mp = mpfrom -> mpto
     | MPdot (mp1,l) -> 
-	let mp1' = subst_mp sub mp1 in
-	  if mp1==mp1' then 
-	    mp
-	  else
-	    MPdot (mp1',l)
+	let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
+	  if mp1==mp1' then mp
+	  else MPdot (mp1',l)
     | _ -> mp
 
-let join subst1 subst2 = 
-  let subst = Umap.map (subst_mp subst2) subst1 in
+let replace_mp_in_con mpfrom mpto kn =
+ let mp,dir,l = repr_con kn in
+  let mp'' = replace_mp_in_mp mpfrom mpto mp in
+    if mp==mp'' then kn
+    else make_con mp'' dir l
+
+exception BothSubstitutionsAreIdentitySubstitutions
+exception ChangeDomain of resolver
+
+let join (subst1 : substitution) (subst2 : substitution) = 
+  let apply_subst (sub : substitution) key (mp,resolve) =
+   let mp',resolve' =
+    match subst_mp0 sub mp with
+       None -> mp, None
+     | Some (mp',resolve') -> mp',resolve' in
+   let resolve'' : resolver option =
+    try
+     let res =
+      match resolve with
+         Some res -> res
+       | None ->
+          match resolve' with
+             None -> raise BothSubstitutionsAreIdentitySubstitutions
+           | Some res -> raise (ChangeDomain res)
+     in
+      Some
+       (List.map
+         (fun (kn,topt) ->
+           kn,
+           match topt with
+              None ->
+               (match key with
+                   MSI msid ->
+                    let kn' = replace_mp_in_con (MPself msid) mp kn in
+                     apply_opt_resolver resolve' kn'
+                 | MBI mbid ->
+                    let kn' = replace_mp_in_con (MPbound mbid) mp kn in
+                     apply_opt_resolver resolve' kn')
+            | Some t -> Some (subst_mps sub t)) res)
+    with
+       BothSubstitutionsAreIdentitySubstitutions -> None
+     | ChangeDomain res ->
+        Some
+         ((List.map
+            (fun (kn,topt) ->
+              let key' =
+               match key with
+                  MSI msid -> MPself msid
+                | MBI mbid -> MPbound mbid in
+              (* let's replace mp with key in kn *)
+              let kn' = replace_mp_in_con mp key' kn in
+               kn',topt)) res)
+   in
+    mp',resolve'' in
+  let subst = Umap.mapi (apply_subst subst2) subst1 in
   Umap.fold Umap.add subst2 subst
 
 let rec occur_in_path uid path =
@@ -79,7 +226,7 @@ let rec occur_in_path uid path =
   | _ -> false
     
 let occur_uid uid sub = 
-  let check_one uid' mp =
+  let check_one uid' (mp,_) =
     if uid = uid' || occur_in_path uid mp then raise Exit
   in
     try 
@@ -112,42 +259,3 @@ let subst_substituted s r =
   | LSlazy(s',a) ->
       let s'' = join s' s in
       ref (LSlazy(s'',a))
-
-let subst_kn sub kn =
- let mp,dir,l = repr_kn kn in
-  let mp' = subst_mp sub mp in
-    if mp==mp' then kn else make_kn mp' dir l
-
-let subst_con sub con =
- let mp,dir,l = repr_con con in
-  let mp' = subst_mp sub mp in
-    if mp==mp' then con else make_con mp' dir l
-
-let subst_evaluable_reference subst = function
-  | EvalVarRef id -> EvalVarRef id
-  | EvalConstRef kn -> EvalConstRef (subst_con subst kn)
-
-(* 
-map_kn : (kernel_name -> kernel_name) -> constr -> constr
-
-This should be rewritten to prevent duplication of constr's when not
-necessary.
-For now, it uses map_constr and is rather ineffective
-*)
-
-let rec map_kn f f_con c = 
-  let func = map_kn f f_con in
-    match kind_of_term c with
-      | Const kn -> 
-	  mkConst (f_con kn)
-      | Ind (kn,i) -> 
-	  mkInd (f kn,i)
-      | Construct ((kn,i),j) -> 
-	  mkConstruct ((f kn,i),j)
-      | Case (ci,p,c,l) ->
-	  let ci' = { ci with ci_ind = let (kn,i) = ci.ci_ind in f kn, i } in
-	  mkCase (ci', func p, func c, array_smartmap func l) 
-      | _ -> map_constr func c
-
-let subst_mps sub = 
-  map_kn (subst_kn sub) (subst_con sub)
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
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 0001a6c5ed..1d63486ba1 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -259,8 +259,13 @@ and translate_mexpr env mexpr = match mexpr with
 	  | Not_path -> error_application_to_not_path mexpr
 	      (* place for nondep_supertype *)
       in
+       let resolve = Modops.resolver_of_environment farg_id farg_b mp env in
 	MEBapply(feb,meb,cst),
-	subst_modtype (map_mbid farg_id mp) fbody_b
+        (* This is the place where the functor formal parameter is
+           substituted by the given argument to compute the type of the
+           functor application. *)
+	subst_modtype
+         (map_mbid farg_id mp (Some resolve)) fbody_b
   | MEstruct (msid,structure) ->
       let structure,signature = translate_entry_list env msid true structure in
 	MEBstruct (msid,structure),
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 73dc914819..cfcc7bd585 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -19,6 +19,8 @@ val translate_modtype : env -> module_type_entry -> module_type_body
 
 val translate_module : env -> module_entry -> module_body
 
+val translate_mexpr : env -> module_expr -> module_expr_body * module_type_body
+
 val add_modtype_constraints : env -> module_type_body -> env
 
 val add_module_constraints : env -> module_body -> env
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
+
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 0e1d9cd34a..e770edc93e 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -95,3 +95,6 @@ val error_with_incorrect : label -> 'a
 val error_local_context : label option -> 'a
 
 val error_circular_with_module : identifier -> 'a
+
+val resolver_of_environment :
+ mod_bound_id -> module_type_body -> module_path -> env -> resolver
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 383f7c2c95..9f03b57c5d 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -249,8 +249,10 @@ and check_modtypes cst env mtb1 mtb2 equiv =
 	    add_module (MPbound arg_id2) (module_body_of_type arg_t2) env 
 	  in
 	  let body_t1' = 
+            (* since we are just checking well-typedness we do not need
+               to expand any constant. Hence the identity resolver. *)
 	    subst_modtype 
-	      (map_mbid arg_id1 (MPbound arg_id2)) 
+              (map_mbid arg_id1 (MPbound arg_id2) None)
 	      body_t1
 	  in
 	  check_modtypes cst env' body_t1' body_t2 equiv