All the reduction tactics have been modified to reduce several (sub)terms

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

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 710a48164585c97aefe718f90d53a409cdd5c690..a51ab3909e8c157ba058595062c3457596ae035c 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -117,53 +117,67 @@ let alpha_equivalence =
    aux
 ;;
 
-(* "textual" replacement of a subterm with another one *)
+exception WhatAndWithWhatDoNotHaveTheSameLength;;
+
+(* "textual" replacement of several subterms with other ones *)
 let replace ~equality ~what ~with_what ~where =
  let module C = Cic in
-  let rec aux =
-   function
-      t when (equality t what) -> with_what
-    | C.Rel _ as t -> t
-    | C.Var (uri,exp_named_subst) ->
-       C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
-    | C.Meta _ as t -> t
-    | C.Sort _ as t -> t
-    | C.Implicit as t -> t
-    | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
-    | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
-    | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
-    | C.Appl l ->
-       (* Invariant enforced: no application of an application *)
-       (match List.map aux l with
-           (C.Appl l')::tl -> C.Appl (l'@tl)
-         | l' -> C.Appl l')
-    | C.Const (uri,exp_named_subst) ->
-       C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
-    | C.MutInd (uri,i,exp_named_subst) ->
-       C.MutInd
-        (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
-    | C.MutConstruct (uri,i,j,exp_named_subst) ->
-       C.MutConstruct
-        (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
-    | C.MutCase (sp,i,outt,t,pl) ->
-       C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
-    | C.Fix (i,fl) ->
-       let substitutedfl =
-        List.map
-         (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
-          fl
-       in
-        C.Fix (i, substitutedfl)
-    | C.CoFix (i,fl) ->
-       let substitutedfl =
-        List.map
-         (fun (name,ty,bo) -> (name, aux ty, aux bo))
-          fl
-       in
-        C.CoFix (i, substitutedfl)
+  let find_image 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
-   aux where
+  let rec aux t =
+   try
+    find_image t
+   with Not_found ->
+    match t with
+       C.Rel _ -> t
+     | C.Var (uri,exp_named_subst) ->
+        C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+     | C.Meta _ -> t
+     | C.Sort _ -> t
+     | C.Implicit as t -> t
+     | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
+     | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
+     | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
+     | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
+     | C.Appl l ->
+        (* Invariant enforced: no application of an application *)
+        (match List.map aux l with
+            (C.Appl l')::tl -> C.Appl (l'@tl)
+          | l' -> C.Appl l')
+     | C.Const (uri,exp_named_subst) ->
+        C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+     | C.MutInd (uri,i,exp_named_subst) ->
+        C.MutInd
+         (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+     | C.MutConstruct (uri,i,j,exp_named_subst) ->
+        C.MutConstruct
+         (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+     | C.MutCase (sp,i,outt,t,pl) ->
+        C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
+     | C.Fix (i,fl) ->
+        let substitutedfl =
+         List.map
+          (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
+           fl
+        in
+         C.Fix (i, substitutedfl)
+     | C.CoFix (i,fl) ->
+        let substitutedfl =
+         List.map
+          (fun (name,ty,bo) -> (name, aux ty, aux bo))
+           fl
+        in
+         C.CoFix (i, substitutedfl)
+   in
+    aux where
 ;;
 
 (* replaces in a term a term with another one. *)
@@ -810,7 +824,7 @@ let simpl context =
       let simplified_term_to_fold =
        reduceaux context [] delta_expanded_term_to_fold
       in
-       replace (=) simplified_term_to_fold term_to_fold res
+       replace (=) [simplified_term_to_fold] [term_to_fold] res
    with
       WrongShape ->
        (* The constant does not unfold to a Fix lambda-abstracted  *)