From ba712be83ed64a934037e2310aa5bdef25e9d3b9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Dec 2002 10:20:32 +0000 Subject: [PATCH] * 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 --- helm/gTopLevel/fourierR.ml | 3 +- helm/gTopLevel/gTopLevel.ml | 43 ++++++++++++++++------------- helm/gTopLevel/proofEngine.ml | 10 +++++-- helm/gTopLevel/proofEngine.mli | 3 +- helm/gTopLevel/reductionTactics.ml | 4 +-- helm/gTopLevel/reductionTactics.mli | 1 + 6 files changed, 39 insertions(+), 25 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index c08183beb..9076ae70f 100644 --- 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 a6dfd3a7b..4878088b7 100644 --- 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 173c1c59d..14a0dc854 100644 --- 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 006471e9a..710f8efac 100644 --- 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 0080e4571..54b439b25 100644 --- 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 00784be7e..8df6c2468 100644 --- 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 -- 2.39.2