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, 166 insertions, 58 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 48bb9933c..e0d16d499 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)