From 9fb6ab77869badc621194768935c8ddbb39193a0 Mon Sep 17 00:00:00 2001 From: acerioni Date: Fri, 12 Mar 2004 10:12:25 +0000 Subject: [PATCH] New tactic Auto. --- helm/gTopLevel/gTopLevel.ml | 5 +++++ helm/gTopLevel/invokeTactics.ml | 4 ++++ helm/gTopLevel/invokeTactics.mli | 2 ++ helm/gTopLevel/proofEngine.ml | 1 + helm/gTopLevel/proofEngine.mli | 1 + 5 files changed, 13 insertions(+) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 5df73dc1c..b13555740 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -658,6 +658,7 @@ module InvokeTacticsCallbacks = let decompose_uris_choice_callback = decompose_uris_choice_callback let mk_fresh_name_callback = mk_fresh_name_callback + let mqi_handle = mqi_handle end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; @@ -2372,6 +2373,9 @@ object(self) let contradictionb = GButton.button ~label:"Contradiction" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let autob= + GButton.button ~label:"Auto" + ~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 existsb = @@ -2503,6 +2507,7 @@ object(self) ignore(searchpatternb#connect#clicked searchPattern) ; ignore(injectionb#connect#clicked InvokeTactics'.injection) ; ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ; + ignore(autob#connect#clicked InvokeTactics'.auto) ; (* Zack: spostare in una toolbar ignore(whdb#connect#clicked whd) ; ignore(reduceb#connect#clicked reduce) ; diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml index 5f01eff9f..e96928988 100644 --- a/helm/gTopLevel/invokeTactics.ml +++ b/helm/gTopLevel/invokeTactics.ml @@ -61,6 +61,7 @@ module type Callbacks = (UriManager.uri * int * 'a) list -> (UriManager.uri * int * 'b list) list val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type + val mqi_handle : MQIConn.handle end ;; @@ -104,6 +105,7 @@ module type Tactics = val whd_in_scratch : unit -> unit val reduce_in_scratch : unit -> unit val simpl_in_scratch : unit -> unit + val auto : unit -> unit end module Make (C: Callbacks) : Tactics = @@ -297,11 +299,13 @@ module Make (C: Callbacks) : Tactics = | _ -> HelmLogger.log (`Error (`T "Too many hypotheses selected")) + let intros = call_tactic (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback) let exact = call_tactic_with_input ProofEngine.exact let apply = call_tactic_with_input ProofEngine.apply + let auto = call_tactic (ProofEngine.auto C.mqi_handle) let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl let elimtype = call_tactic_with_input ProofEngine.elim_type let whd = call_tactic_with_goal_inputs ProofEngine.whd diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli index 41cc917b7..5578c43e5 100644 --- a/helm/gTopLevel/invokeTactics.mli +++ b/helm/gTopLevel/invokeTactics.mli @@ -59,6 +59,7 @@ module type Callbacks = (UriManager.uri * int * 'a) list -> (UriManager.uri * int * 'b list) list val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type + val mqi_handle : MQIConn.handle end module type Tactics = @@ -101,6 +102,7 @@ module type Tactics = val whd_in_scratch : unit -> unit val reduce_in_scratch : unit -> unit val simpl_in_scratch : unit -> unit + val auto : unit -> unit end module Make (C : Callbacks) : Tactics diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 1077f15c2..1d6ce4f20 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -225,6 +225,7 @@ let fold_simpl term = let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term) let ring () = apply_tactic Ring.ring_tac let fourier () = apply_tactic FourierR.fourier_tac +let auto mqi_handle () = apply_tactic (VariousTactics.auto_tac mqi_handle) let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term) let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term) diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index dd7e1c412..58a9a3695 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -71,6 +71,7 @@ val fourier : unit -> unit val rewrite_simpl : Cic.term -> unit val rewrite_back_simpl : Cic.term -> unit val replace : goal_input:Cic.term -> input:Cic.term -> unit +val auto : MQIConn.handle -> unit -> unit val reflexivity : unit -> unit val symmetry : unit -> unit -- 2.39.2