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.

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index bdba623190cc8ab47fa6b533f232ff5a26aec7a7..62e5d0f9ae016dd2ecacef01d115fdd3f41a128b 100644 (file)
--- 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 b47f8856a682581d2a32d0ae18e984ea5a975810..788e46bd13d4db8daf3a3370e51d1842672966e5 100644 (file)
--- 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 67e225c6dd07c449e87034dd920c174ed191facc..c15598cac46ea5b4f04b70e15e0888cd1e6f2174 100644 (file)
--- 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 9237deb578e2e47e8d6c15af0be50698552fa520..a4cf407f08fc103a26a977b9895ad1179c068b90 100644 (file)
--- 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