Generalize now works on a list of convertible terms, generalizing all of

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

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index a51ab3909e8c157ba058595062c3457596ae035c..5cc513deb7a682281653d55d9a0ebc318e8ab520 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -261,88 +261,98 @@ let replace_lifting ~equality ~what ~with_what ~where =
   substaux 1 what where
 ;;
 
-(* replaces in a term a term with another one. *)
-(* Lifting are performed as usual.             *)
+(* replaces in a term a list of terms with other ones. *)
+(* Lifting are performed as usual.                     *)
 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
- let rec substaux k =
-  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 ->
-       if n < k then C.Rel n else C.Rel (n + nnn)
-    | C.Var (uri,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
-       in
-        C.Var (uri,exp_named_subst')
-    | C.Meta (i, l) as t -> 
-       let l' =
-        List.map
-         (function
-             None -> None
-           | Some t -> Some (substaux k t)
-         ) l
-       in
-        C.Meta(i,l')
-    | C.Sort _ as t -> t
-    | C.Implicit as t -> t
-    | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
-    | C.Prod (n,s,t) ->
-       C.Prod (n, substaux k s, substaux (k + 1) t)
-    | C.Lambda (n,s,t) ->
-       C.Lambda (n, substaux k s, substaux (k + 1) t)
-    | C.LetIn (n,s,t) ->
-       C.LetIn (n, substaux k s, substaux (k + 1) t)
-    | C.Appl (he::tl) ->
-       (* Invariant: no Appl applied to another Appl *)
-       let tl' = List.map (substaux k) tl in
-        begin
-         match substaux k he with
-            C.Appl l -> C.Appl (l@tl')
-          | _ as he' -> C.Appl (he'::tl')
-        end
-    | C.Appl _ -> assert false
-    | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
-       in
-       C.Const (uri,exp_named_subst')
-    | C.MutInd (uri,i,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
-       in
-        C.MutInd (uri,i,exp_named_subst')
-    | C.MutConstruct (uri,i,j,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
-       in
-        C.MutConstruct (uri,i,j,exp_named_subst')
-    | C.MutCase (sp,i,outt,t,pl) ->
-       C.MutCase (sp,i,substaux k outt, substaux k t,
-        List.map (substaux k) pl)
-    | C.Fix (i,fl) ->
-       let len = List.length fl in
-       let substitutedfl =
-        List.map
-         (fun (name,i,ty,bo) ->
-           (name, i, substaux k ty, substaux (k+len) bo))
-          fl
-       in
-        C.Fix (i, substitutedfl)
-    | C.CoFix (i,fl) ->
-       let len = List.length fl in
-       let substitutedfl =
-        List.map
-         (fun (name,ty,bo) ->
-           (name, substaux k ty, substaux (k+len) bo))
-          fl
-       in
-        C.CoFix (i, substitutedfl)
+ let module C = Cic in
+ let module S = CicSubstitution in
+  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
+  let rec substaux k t =
+   try
+    S.lift (k-1) (find_image t)
+   with Not_found ->
+    match t with
+       C.Rel n as t ->
+        if n < k then C.Rel n else C.Rel (n + nnn)
+     | C.Var (uri,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+        in
+         C.Var (uri,exp_named_subst')
+     | C.Meta (i, l) as t -> 
+        let l' =
+         List.map
+          (function
+              None -> None
+            | Some t -> Some (substaux k t)
+          ) l
+        in
+         C.Meta(i,l')
+     | C.Sort _ as t -> t
+     | C.Implicit as t -> t
+     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
+     | C.Prod (n,s,t) ->
+        C.Prod (n, substaux k s, substaux (k + 1) t)
+     | C.Lambda (n,s,t) ->
+        C.Lambda (n, substaux k s, substaux (k + 1) t)
+     | C.LetIn (n,s,t) ->
+        C.LetIn (n, substaux k s, substaux (k + 1) t)
+     | C.Appl (he::tl) ->
+        (* Invariant: no Appl applied to another Appl *)
+        let tl' = List.map (substaux k) tl in
+         begin
+          match substaux k he with
+             C.Appl l -> C.Appl (l@tl')
+           | _ as he' -> C.Appl (he'::tl')
+         end
+     | C.Appl _ -> assert false
+     | C.Const (uri,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+        in
+        C.Const (uri,exp_named_subst')
+     | C.MutInd (uri,i,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+        in
+         C.MutInd (uri,i,exp_named_subst')
+     | C.MutConstruct (uri,i,j,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+        in
+         C.MutConstruct (uri,i,j,exp_named_subst')
+     | C.MutCase (sp,i,outt,t,pl) ->
+        C.MutCase (sp,i,substaux k outt, substaux k t,
+         List.map (substaux k) pl)
+     | C.Fix (i,fl) ->
+        let len = List.length fl in
+        let substitutedfl =
+         List.map
+          (fun (name,i,ty,bo) ->
+            (name, i, substaux k ty, substaux (k+len) bo))
+           fl
+        in
+         C.Fix (i, substitutedfl)
+     | C.CoFix (i,fl) ->
+        let len = List.length fl in
+        let substitutedfl =
+         List.map
+          (fun (name,ty,bo) ->
+            (name, substaux k ty, substaux (k+len) bo))
+           fl
+        in
+         C.CoFix (i, substitutedfl)
  in
-let res =  
   substaux 1 where
-in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res
 ;;
 
 (* Takes a well-typed term and fully reduces it. *)