replace_lifting generalized to the simultaneous replacement of n terms.

[helm.git] / helm / ocaml / tactics / proofEngineReduction.ml

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 5cc513deb7a682281653d55d9a0ebc318e8ab520..c70be1fb736b61b4da38d15c491f2e5d77579f18 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -183,12 +183,24 @@ let replace ~equality ~what ~with_what ~where =
 (* replaces in a term a term with another one. *)
 (* Lifting are performed as usual.             *)
 let replace_lifting ~equality ~what ~with_what ~where =
- let rec substaux k what =
-  let module C = Cic in
-  let module S = CicSubstitution in
-   function
-      t when (equality t what) -> S.lift (k-1) with_what
-    | C.Rel n as t -> t
+ let module C = Cic in
+ let module S = CicSubstitution in
+  let find_image what t =
+   let rec find_image_aux =
+    function
+       [],[] -> raise Not_found
+     | what::tl1,with_what::tl2 ->
+        if equality t what then with_what else find_image_aux (tl1,tl2)
+     | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
+   in
+    find_image_aux (what,with_what)
+  in
+  let rec substaux k what t =
+   try
+    S.lift (k-1) (find_image what t)
+   with Not_found ->
+    match t with
+      C.Rel n as t -> t
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
@@ -207,11 +219,14 @@ let replace_lifting ~equality ~what ~with_what ~where =
     | C.Implicit as t -> t
     | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
     | C.Prod (n,s,t) ->
-       C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+       C.Prod
+        (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
     | C.Lambda (n,s,t) ->
-       C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+       C.Lambda
+        (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
     | C.LetIn (n,s,t) ->
-       C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+       C.LetIn
+        (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
     | C.Appl (he::tl) ->
        (* Invariant: no Appl applied to another Appl *)
        let tl' = List.map (substaux k what) tl in
@@ -244,8 +259,9 @@ let replace_lifting ~equality ~what ~with_what ~where =
        let substitutedfl =
         List.map
          (fun (name,i,ty,bo) ->
-           (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo))
-          fl
+           (name, i, substaux k what ty,
+             substaux (k+len) (List.map (S.lift len) what) bo)
+         ) fl
        in
         C.Fix (i, substitutedfl)
     | C.CoFix (i,fl) ->
@@ -253,8 +269,9 @@ let replace_lifting ~equality ~what ~with_what ~where =
        let substitutedfl =
         List.map
          (fun (name,ty,bo) ->
-           (name, substaux k what ty, substaux (k+len) (S.lift len what) bo))
-          fl
+           (name, substaux k what ty,
+             substaux (k+len) (List.map (S.lift len) what) bo)
+         ) fl
        in
         C.CoFix (i, substitutedfl)
  in