Added an almost working version of Generalize tactic.

[helm.git] / helm / gTopLevel / proofEngineReduction.ml

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 1b36e686e4337da522ce688450316af2ce94e4b4..710a48164585c97aefe718f90d53a409cdd5c690 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -247,6 +247,90 @@ 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.             *)
+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)
+ in
+let res =  
+  substaux 1 where
+in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res
+;;
+
 (* Takes a well-typed term and fully reduces it. *)
 (*CSC: It does not perform reduction in a Case *)
 let reduce context =