From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Nov 2002 11:50:58 +0000 (+0000)
Subject: - new fold tactic
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5d7a6ea089e670ac1e42794b69cedaa69057ac8b;p=helm.git

- new fold tactic
---

diff --git a/helm/gTopLevel/reductionTactics.ml b/helm/gTopLevel/reductionTactics.ml
index 0e5688e02..67e225c6d 100644
--- a/helm/gTopLevel/reductionTactics.ml
+++ b/helm/gTopLevel/reductionTactics.ml
@@ -40,3 +40,33 @@ let reduction_tac ~reduction ~status:(proof,goal) =
 let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;;
 let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;;
 let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;
+
+let fold_tac ~term ~status:(proof,goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let term' = CicReduction.whd context term in
+   (* We don't know if [term] is a subterm of [ty] or a subterm of *)
+   (* the type of one metavariable. So we replace it everywhere.   *)
+   (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
+   (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
+   let replace =
+    ProofEngineReduction.replace ~equality:(=) ~what:term' ~with_what:term
+   in
+    let ty' = replace ty in
+    let context' =
+     List.map
+      (function
+          Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
+        | Some (n,Cic.Def t)  -> Some (n,Cic.Def  (replace t))
+        | None -> None
+      ) context
+    in
+     let metasenv' = 
+      List.map
+       (function
+           (n,_,_) when n = metano -> (metano,context',ty')
+         | _ as t -> t
+       ) metasenv
+     in
+      (curi,metasenv',pbo,pty), [metano]
+;;
diff --git a/helm/gTopLevel/reductionTactics.mli b/helm/gTopLevel/reductionTactics.mli
index 97418b4da..9237deb57 100644
--- a/helm/gTopLevel/reductionTactics.mli
+++ b/helm/gTopLevel/reductionTactics.mli
@@ -26,3 +26,4 @@
 val simpl_tac: ProofEngineTypes.tactic
 val reduce_tac: ProofEngineTypes.tactic
 val whd_tac: ProofEngineTypes.tactic
+val fold_tac: term:Cic.term -> ProofEngineTypes.tactic