New tactic Auto.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 5df73dc1cacbc71b3fb61443838829c32582888c..b13555740e9086724345aa3def6df0c8c1ccb9fd 100644 (file)
--- 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 5f01eff9f489d967fc9526eb4add5c3b71be4e80..e96928988628edb51b686714c9f9a8576f0eae43 100644 (file)
--- 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 41cc917b7bed4ed4fc134a9d5d7735ea525383a9..5578c43e519579e4763efe879b058edee2c8deae 100644 (file)
--- 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 1077f15c2bc6a03cdaa7b2c9cd6b854c857446a5..1d6ce4f203dc6d9a6211e808056ff9c3513b2a09 100644 (file)
--- 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 dd7e1c4128b48df9eb5313994656c837e09d71b1..58a9a369521b18342d658c0284c5e7a3e3081877 100644 (file)
--- 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