* The Fold button is replaced with Fold_whd and Fold_reduce
* Minor interfaces modifications
(*CSC: Patch to undo the over-simplification of RewriteSimpl *)
Tacticals.then_
~start:
(*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 ;
~term:
(Cic.Appl
[_Rle ; _R0 ;
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 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;;
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;;
let simplb =
GButton.button ~label:"Simpl"
~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
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 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
let changeb =
GButton.button ~label:"Change"
~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
let clearb =
GButton.button ~label:"Clear"
~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
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"
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 ->"
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"
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
let symmetryb =
GButton.button ~label:"Symmetry"
~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
let splitb =
GButton.button ~label:"Split"
~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
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"
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"
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"
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"
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
let absurdb =
GButton.button ~label:"Absurd"
~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
ignore(whdb#connect#clicked whd) ;
ignore(reduceb#connect#clicked reduce) ;
ignore(simplb#connect#clicked simpl) ;
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) ;
ignore(cutb#connect#clicked cut) ;
ignore(changeb#connect#clicked change) ;
ignore(letinb#connect#clicked letin) ;
apply_tactic
(ReductionTactics.simpl_tac ~also_in_hypotheses:true ~term:(Some 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)
val whd : Cic.term -> unit
val reduce : Cic.term -> unit
val simpl : 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
(* scratch area reduction tactics *)
val whd_in_scratch : Cic.term -> Cic.term -> Cic.term
let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;;
let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;
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 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 *)
(* 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 *)
also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic
val fold_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
also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic