* fold_tac has now a new parameter, which is the reduction to ``undo''

* The Fold button is replaced with Fold_whd and Fold_reduce
* Minor interfaces modifications

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index c08183bebf889300aa8c56893930d4a842e3deaf..9076ae70fffce795573bb6733e8140a60e73da04 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -775,7 +775,8 @@ let r =
      (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
      Tacticals.then_
       ~start:
-        (ReductionTactics.fold_tac ~also_in_hypotheses:false
+        (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+          ~also_in_hypotheses:false
           ~term:
             (Cic.Appl
               [_Rle ; _R0 ;

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index a6dfd3a7b74a2f6656f2505564e70f1a84919dff..4878088b709748ef9bc5d0168965420ebe5985a9 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2270,7 +2270,8 @@ let elimtype = call_tactic_with_input ProofEngine.elim_type;;
 let whd = call_tactic_with_goal_input ProofEngine.whd;;
 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
-let fold = call_tactic_with_input ProofEngine.fold;;
+let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
+let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
 let cut = call_tactic_with_input ProofEngine.cut;;
 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
 let letin = call_tactic_with_input ProofEngine.letin;;
@@ -2709,14 +2710,17 @@ object(self)
    let simplb =
     GButton.button ~label:"Simpl"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let foldb =
-    GButton.button ~label:"Fold"
-     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let cutb =
-    GButton.button ~label:"Cut"
-     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
    let hbox4 =
     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+   let foldwhdb =
+    GButton.button ~label:"Fold_whd"
+     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+   let foldreduceb =
+    GButton.button ~label:"Fold_reduce"
+     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+   let cutb =
+    GButton.button ~label:"Cut"
+     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
    let changeb =
     GButton.button ~label:"Change"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2732,17 +2736,17 @@ object(self)
    let clearb =
     GButton.button ~label:"Clear"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+   let hbox5 =
+    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
    let fourierb =
     GButton.button ~label:"Fourier"
-     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
    let rewritesimplb =
     GButton.button ~label:"RewriteSimpl ->"
-     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
    let reflexivityb =
     GButton.button ~label:"Reflexivity"
-     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
-   let hbox5 =
-    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
    let symmetryb =
     GButton.button ~label:"Symmetry"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2755,20 +2759,20 @@ object(self)
    let splitb =
     GButton.button ~label:"Split"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+   let hbox6 =
+    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
    let leftb =
     GButton.button ~label:"Left"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let rightb =
     GButton.button ~label:"Right"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let assumptionb =
     GButton.button ~label:"Assumption"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let generalizeb =
     GButton.button ~label:"Generalize"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
-   let hbox6 =
-    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let absurdb =
     GButton.button ~label:"Absurd"
      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2786,7 +2790,8 @@ object(self)
    ignore(whdb#connect#clicked whd) ;
    ignore(reduceb#connect#clicked reduce) ;
    ignore(simplb#connect#clicked simpl) ;
-   ignore(foldb#connect#clicked fold) ;
+   ignore(foldwhdb#connect#clicked fold_whd) ;
+   ignore(foldreduceb#connect#clicked fold_reduce) ;
    ignore(cutb#connect#clicked cut) ;
    ignore(changeb#connect#clicked change) ;
    ignore(letinb#connect#clicked letin) ;

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 173c1c59d3195f374fe087513c8d188d411d9855..14a0dc8543a6a511c33ab5bee6428bcc417ab041 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -199,8 +199,14 @@ let simpl term =
  apply_tactic
   (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~term:(Some term))
 
-let fold term =
- apply_tactic (ReductionTactics.fold_tac ~also_in_hypotheses:true ~term)
+let fold_whd term =
+ apply_tactic
+  (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+    ~also_in_hypotheses:true ~term)
+let fold_reduce term =
+ apply_tactic
+  (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.reduce
+    ~also_in_hypotheses:true ~term)
 
   (* other tactics *)
 

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index 006471e9a961da81db2668a0a4e20d6542ff5bc6..710f8efacfad39a52c031fad2959f8d5730cd7b6 100644 (file)
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -34,7 +34,8 @@ val perforate : Cic.context -> Cic.term -> Cic.term -> unit
 val whd : Cic.term -> unit
 val reduce : Cic.term -> unit
 val simpl : Cic.term -> unit
-val fold : Cic.term -> unit
+val fold_whd : Cic.term -> unit
+val fold_reduce : Cic.term -> unit
 
   (* scratch area reduction tactics *)
 val whd_in_scratch : Cic.term -> Cic.term -> Cic.term

diff --git a/helm/gTopLevel/reductionTactics.ml b/helm/gTopLevel/reductionTactics.ml
index 0080e4571255062d85a4b91be1bdb8b2e701a2f4..54b439b25ae40ef31a0fc0c8356eadec95774383 100644 (file)
--- a/helm/gTopLevel/reductionTactics.ml
+++ b/helm/gTopLevel/reductionTactics.ml
@@ -92,10 +92,10 @@ 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 ~also_in_hypotheses ~term ~status:(proof,goal) =
+let fold_tac ~reduction ~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
+  let term' = reduction 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 *)

diff --git a/helm/gTopLevel/reductionTactics.mli b/helm/gTopLevel/reductionTactics.mli
index 00784be7e00da815d4c00a90f5f213b66ae9198b..8df6c2468777854d87d2fc2d2bf0a5c56811b6a5 100644 (file)
--- a/helm/gTopLevel/reductionTactics.mli
+++ b/helm/gTopLevel/reductionTactics.mli
@@ -32,4 +32,5 @@ val whd_tac:
  also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic
 
 val fold_tac:
+ reduction:(Cic.context -> Cic.term -> Cic.term) ->
  also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic