From b0f879da074adb838681869bf401c97d0a860c6b Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Nov 2002 13:13:10 +0000
Subject: [PATCH] The fold tactic of proofEngine now uses
 ReductionTactics.fold_tac. A parameter was added to choose if the reduction
 must be performed also in the hypotheses.

---
 helm/gTopLevel/fourierR.ml          |  2 +-
 helm/gTopLevel/proofEngine.ml       | 50 ++++-------------------------
 helm/gTopLevel/reductionTactics.ml  | 28 +++++++++-------
 helm/gTopLevel/reductionTactics.mli |  3 +-
 4 files changed, 26 insertions(+), 57 deletions(-)

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index bdba62319..62e5d0f9a 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -714,7 +714,7 @@ let r =
      (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
      Tacticals.then_
       ~start:
-        (ReductionTactics.fold_tac
+        (ReductionTactics.fold_tac ~also_in_hypotheses:false
           ~term:
             (Cic.Appl
               [_Rle ; _R0 ;
diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index b47f8856a..788e46bd1 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -215,49 +215,8 @@ let reduce = reduction_tactic ProofEngineReduction.reduce
 let simpl  = reduction_tactic ProofEngineReduction.simpl
 
 let whd_in_scratch    = reduction_tactic_in_scratch CicReduction.whd
-let reduce_in_scratch =
- reduction_tactic_in_scratch ProofEngineReduction.reduce
-let simpl_in_scratch  =
- reduction_tactic_in_scratch ProofEngineReduction.simpl
-
-(* It is just the opposite of whd. The code should probably be merged. *)
-let fold term =
- let curi,metasenv,pbo,pty =
-  match !proof with
-     None -> assert false
-   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,context,ty =
-  match !goal with
-     None -> assert false
-   | Some metano -> List.find (function (m,_,_) -> m=metano) 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
-      proof := Some (curi,metasenv',pbo,pty) ;
-      goal := Some metano
+let reduce_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.reduce
+let simpl_in_scratch  = reduction_tactic_in_scratch ProofEngineReduction.simpl
 
 (************************************************************)
 (*              Tactics defined elsewhere                   *)
@@ -282,6 +241,11 @@ let change ~goal_input:what ~input:with_what =
 let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp)
 let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)
 
+  (* reduction tactics *)
+
+let fold term =
+ apply_tactic (ReductionTactics.fold_tac ~also_in_hypotheses:true ~term)
+
   (* other tactics *)
 
 let elim_type term = apply_tactic (Ring.elim_type_tac ~term)
diff --git a/helm/gTopLevel/reductionTactics.ml b/helm/gTopLevel/reductionTactics.ml
index 67e225c6d..c15598cac 100644
--- a/helm/gTopLevel/reductionTactics.ml
+++ b/helm/gTopLevel/reductionTactics.ml
@@ -41,7 +41,7 @@ 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 fold_tac ~also_in_hypotheses ~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
@@ -53,20 +53,24 @@ let fold_tac ~term ~status:(proof,goal) =
     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' = 
+    let metasenv' =
+     let context' =
+      if also_in_hypotheses then
+       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
+      else
+       context
+     in
       List.map
        (function
            (n,_,_) when n = metano -> (metano,context',ty')
          | _ as t -> t
        ) metasenv
-     in
-      (curi,metasenv',pbo,pty), [metano]
+     
+    in
+     (curi,metasenv',pbo,pty), [metano]
 ;;
diff --git a/helm/gTopLevel/reductionTactics.mli b/helm/gTopLevel/reductionTactics.mli
index 9237deb57..a4cf407f0 100644
--- a/helm/gTopLevel/reductionTactics.mli
+++ b/helm/gTopLevel/reductionTactics.mli
@@ -26,4 +26,5 @@
 val simpl_tac: ProofEngineTypes.tactic
 val reduce_tac: ProofEngineTypes.tactic
 val whd_tac: ProofEngineTypes.tactic
-val fold_tac: term:Cic.term -> ProofEngineTypes.tactic
+val fold_tac:
+ also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic
-- 
2.39.2