# HG changeset patch
# User blanchet
# Date 1284193312 -7200
# Node ID ad9a1f9b05585d1e3e05c1643b7d21789a59ce56
# Parent  6ec8d46836996a1df286bed73cab224aafa79083
implemented Auto Sledgehammer

diff -r 6ec8d4683699 -r ad9a1f9b0558 src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Sat Sep 11 10:20:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Sat Sep 11 10:21:52 2010 +0200
@@ -270,7 +270,7 @@
     val tvars = gen_TVars (length args)
     val tvars_srts = ListPair.zip (tvars, args)
   in
-    ArityClause {name = name, 
+    ArityClause {name = name,
                  conclLit = TConsLit (`make_type_class cls,
                                       `make_fixed_type_const tcons,
                                       tvars ~~ tvars),
diff -r 6ec8d4683699 -r ad9a1f9b0558 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Sep 11 10:20:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Sep 11 10:21:52 2010 +0200
@@ -28,7 +28,7 @@
      timeout: Time.time,
      expect: string}
   type problem =
-    {ctxt: Proof.context,
+    {state: Proof.state,
      goal: thm,
      subgoal: int,
      axioms: (term * ((string * locality) * fol_formula) option) list}
@@ -52,8 +52,8 @@
   val messages: int option -> unit
   val get_prover_fun : theory -> string -> prover
   val run_sledgehammer :
-    params -> int -> relevance_override -> (string -> minimize_command)
-    -> Proof.state -> unit
+    params -> bool -> int -> relevance_override -> (string -> minimize_command)
+    -> Proof.state -> bool * Proof.state
   val setup : theory -> theory
 end;
 
@@ -97,7 +97,7 @@
    expect: string}
 
 type problem =
-  {ctxt: Proof.context,
+  {state: Proof.state,
    goal: thm,
    subgoal: int,
    axioms: (term * ((string * locality) * fol_formula) option) list}
@@ -230,18 +230,18 @@
 
 (* generic TPTP-based provers *)
 
-fun prover_fun atp_name
+fun prover_fun auto atp_name
         {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
          known_failures, default_max_relevant, explicit_forall,
          use_conjecture_for_hypotheses}
         ({debug, verbose, overlord, full_types, explicit_apply,
           max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
-        minimize_command ({ctxt, goal, subgoal, axioms} : problem) =
+        minimize_command ({state, goal, subgoal, axioms} : problem) =
   let
+    val ctxt = Proof.context_of state
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
     val max_relevant = the_default default_max_relevant max_relevant
     val axioms = take max_relevant axioms
-    (* path to unique problem file *)
     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
                        else Config.get ctxt dest_dir
     val the_problem_prefix = Config.get ctxt problem_prefix
@@ -285,7 +285,7 @@
       | [] =>
         if File.exists command then
           let
-            fun do_run complete timeout =
+            fun run complete timeout =
               let
                 val command = command_line complete timeout probfile
                 val ((output, msecs), res_code) =
@@ -309,17 +309,17 @@
             val conjecture_shape =
               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
               |> map single
+            val run_twice = has_incomplete_mode andalso not auto
             val timer = Timer.startRealTimer ()
             val result =
-              do_run false (if has_incomplete_mode then
-                              Time.fromMilliseconds
+              run false (if run_twice then
+                           Time.fromMilliseconds
                                          (2 * Time.toMilliseconds timeout div 3)
-                            else
-                              timeout)
-              |> has_incomplete_mode
+                         else
+                           timeout)
+              |> run_twice
                  ? (fn (_, msecs0, _, SOME _) =>
-                       do_run true
-                              (Time.- (timeout, Timer.checkRealTimer timer))
+                       run true (Time.- (timeout, Timer.checkRealTimer timer))
                        |> (fn (output, msecs, proof, outcome) =>
                               (output, msecs0 + msecs, proof, outcome))
                      | result => result)
@@ -367,14 +367,15 @@
      conjecture_shape = conjecture_shape}
   end
 
-fun get_prover_fun thy name = prover_fun name (get_prover thy name)
+fun get_prover_fun thy name = prover_fun false name (get_prover thy name)
 
-fun run_prover ctxt (params as {blocking, verbose, max_relevant, timeout,
-                                expect, ...})
-               i n relevance_override minimize_command
-               (problem as {goal, axioms, ...})
+fun run_prover (params as {blocking, verbose, max_relevant, timeout, expect,
+                           ...})
+               auto i n relevance_override minimize_command
+               (problem as {state, goal, axioms, ...})
                (prover as {default_max_relevant, ...}, atp_name) =
   let
+    val ctxt = Proof.context_of state
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, timeout)
     val max_relevant = the_default default_max_relevant max_relevant
@@ -390,72 +391,94 @@
          ""
        else
          "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
-    fun run () =
+    fun go () =
       let
         val (outcome_code, message) =
-          prover_fun atp_name prover params (minimize_command atp_name) problem
+          prover_fun auto atp_name prover params (minimize_command atp_name)
+                     problem
           |> (fn {outcome, message, ...} =>
                  (if is_some outcome then "none" else "some", message))
           handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
                | exn => ("unknown", "Internal error:\n" ^
                                     ML_Compiler.exn_message exn ^ "\n")
-      in
-        if expect = "" orelse outcome_code = expect then
-          ()
-        else if blocking then
-          error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
-        else
-          warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
-        message
+        val _ =
+          if expect = "" orelse outcome_code = expect then
+            ()
+          else if blocking then
+            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+          else
+            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
+      in (outcome_code = "some", message) end
+  in
+    if auto then
+      let val (success, message) = TimeLimit.timeLimit timeout go () in
+        (success, state |> success ? Proof.goal_message (fn () =>
+             Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
+                 (Pretty.str ("Sledgehammer found a proof! " ^ message))]))
       end
-  in
-    if blocking then priority (desc ^ "\n" ^ TimeLimit.timeLimit timeout run ())
-    else Async_Manager.launch das_Tool birth_time death_time desc run
+    else if blocking then
+      let val (success, message) = TimeLimit.timeLimit timeout go () in
+        priority (desc ^ "\n" ^ message); (success, state)
+      end
+    else
+      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
+       (false, state))
   end
 
+val auto_max_relevant_divisor = 2
+
 fun run_sledgehammer (params as {blocking, verbose, atps, full_types,
                                  relevance_thresholds, max_relevant, ...})
-                     i relevance_override minimize_command state =
-    if null atps then error "No ATP is set."
-    else case subgoal_count state of
-      0 => priority "No subgoal!"
-    | n =>
-      let
-        val thy = Proof.theory_of state
-        val timer = Timer.startRealTimer ()
-        val _ = () |> not blocking ? kill_atps
-        val _ = priority "Sledgehammering..."
-        val provers = map (`(get_prover thy)) atps
-        fun run () =
-          let
-            val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
-            val (_, hyp_ts, concl_t) = strip_subgoal goal i
-            val max_max_relevant =
-              case max_relevant of
-                SOME n => n
-              | NONE => fold (Integer.max o #default_max_relevant o fst)
-                             provers 0
-            val axioms =
-              relevant_facts ctxt full_types relevance_thresholds
-                             max_max_relevant relevance_override chained_ths
-                             hyp_ts concl_t
-            val problem =
-              {ctxt = ctxt, goal = goal, subgoal = i,
-               axioms = map (prepare_axiom ctxt) axioms}
-            val num_axioms = length axioms
-            val _ =
-              (if blocking then Par_List.map else map)
-                  (run_prover ctxt params i n relevance_override
-                              minimize_command problem) provers
-          in
-            if verbose andalso blocking then
-              priority ("Total time: " ^
-                        signed_string_of_int (Time.toMilliseconds
-                            (Timer.checkRealTimer timer)) ^ " ms.")
-            else
-              ()
-          end
-      in if blocking then run () else Future.fork run |> K () end
+                     auto i relevance_override minimize_command state =
+  if null atps then
+    error "No ATP is set."
+  else case subgoal_count state of
+    0 => (priority "No subgoal!"; (false, state))
+  | n =>
+    let
+      val thy = Proof.theory_of state
+      val timer = Timer.startRealTimer ()
+      val _ = () |> not blocking ? kill_atps
+      val _ = if auto then () else priority "Sledgehammering..."
+      val provers = map (`(get_prover thy)) atps
+      fun go () =
+        let
+          val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
+          val (_, hyp_ts, concl_t) = strip_subgoal goal i
+          val max_max_relevant =
+            case max_relevant of
+              SOME n => n
+            | NONE =>
+              0 |> fold (Integer.max o #default_max_relevant o fst) provers
+                |> auto ? (fn n => n div auto_max_relevant_divisor)
+          val axioms =
+            relevant_facts ctxt full_types relevance_thresholds
+                           max_max_relevant relevance_override chained_ths
+                           hyp_ts concl_t
+          val problem =
+            {state = state, goal = goal, subgoal = i,
+             axioms = map (prepare_axiom ctxt) axioms}
+          val run_prover =
+            run_prover params auto i n relevance_override minimize_command
+                       problem
+          val num_axioms = length axioms
+        in
+          if auto then
+            fold (fn prover => fn (true, state) => (true, state)
+                                | (false, _) => run_prover prover)
+                 provers (false, state)
+          else
+            (if blocking then Par_List.map else map) run_prover provers
+            |> tap (fn _ =>
+                       if verbose then
+                         priority ("Total time: " ^
+                                   signed_string_of_int (Time.toMilliseconds
+                                       (Timer.checkRealTimer timer)) ^ " ms.")
+                       else
+                         ())
+            |> exists fst |> rpair state
+        end
+    in if blocking then go () else Future.fork (tap go) |> K (false, state) end
 
 val setup =
   dest_dir_setup
diff -r 6ec8d4683699 -r ad9a1f9b0558 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Sep 11 10:20:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Sep 11 10:21:52 2010 +0200
@@ -8,10 +8,12 @@
 sig
   type params = Sledgehammer.params
 
-  val atps: string Unsynchronized.ref
-  val timeout: int Unsynchronized.ref
-  val full_types: bool Unsynchronized.ref
+  val auto : bool Unsynchronized.ref
+  val atps : string Unsynchronized.ref
+  val timeout : int Unsynchronized.ref
+  val full_types : bool Unsynchronized.ref
   val default_params : theory -> (string * string) list -> params
+  val setup : theory -> theory
 end;
 
 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
@@ -22,11 +24,19 @@
 open Sledgehammer
 open Sledgehammer_Minimize
 
+val auto = Unsynchronized.ref false
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_tracing
+      (Preferences.bool_pref auto "auto-sledgehammer"
+           "Whether to run Sledgehammer automatically.")
+
 (** Sledgehammer commands **)
 
-fun add_to_relevance_override ns : relevance_override =
+val no_relevance_override = {add = [], del = [], only = false}
+fun add_relevance_override ns : relevance_override =
   {add = ns, del = [], only = false}
-fun del_from_relevance_override ns : relevance_override =
+fun del_relevance_override ns : relevance_override =
   {add = [], del = ns, only = false}
 fun only_relevance_override ns : relevance_override =
   {add = ns, del = [], only = true}
@@ -132,7 +142,7 @@
 val infinity_time_in_secs = 60 * 60 * 24 * 365
 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
 
-fun extract_params default_params override_params =
+fun extract_params auto default_params override_params =
   let
     val override_params = map unalias_raw_param override_params
     val raw_params = rev override_params @ rev default_params
@@ -145,9 +155,9 @@
     val lookup_bool = the o general_lookup_bool false (SOME false)
     val lookup_bool_option = general_lookup_bool true NONE
     fun lookup_time name =
-      the_timeout (case lookup name of
-                     NONE => NONE
-                   | SOME s => parse_time_option name s)
+      case lookup name of
+        SOME s => parse_time_option name s
+      | NONE => NONE
     fun lookup_int name =
       case lookup name of
         NONE => 0
@@ -167,11 +177,11 @@
       case lookup name of
         SOME "smart" => NONE
       | _ => SOME (lookup_int name)
-    val blocking = lookup_bool "blocking"
-    val debug = lookup_bool "debug"
-    val verbose = debug orelse lookup_bool "verbose"
+    val blocking = auto orelse lookup_bool "blocking"
+    val debug = not auto andalso lookup_bool "debug"
+    val verbose = debug orelse (not auto andalso lookup_bool "verbose")
     val overlord = lookup_bool "overlord"
-    val atps = lookup_string "atps" |> space_explode " "
+    val atps = lookup_string "atps" |> space_explode " " |> auto ? single o hd
     val full_types = lookup_bool "full_types"
     val explicit_apply = lookup_bool "explicit_apply"
     val relevance_thresholds =
@@ -180,7 +190,7 @@
     val max_relevant = lookup_int_option "max_relevant"
     val isar_proof = lookup_bool "isar_proof"
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
-    val timeout = lookup_time "timeout"
+    val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
     val expect = lookup_string "expect"
   in
     {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
@@ -190,8 +200,8 @@
      timeout = timeout, expect = expect}
   end
 
-fun get_params thy = extract_params (default_raw_params thy)
-fun default_params thy = get_params thy o map (apsnd single)
+fun get_params auto thy = extract_params auto (default_raw_params thy)
+fun default_params thy = get_params false thy o map (apsnd single)
 
 (* Sledgehammer the given subgoal *)
 
@@ -225,11 +235,13 @@
   in
     if subcommand = runN then
       let val i = the_default 1 opt_i in
-        run_sledgehammer (get_params thy override_params) i relevance_override
-                         (minimize_command override_params i) state
+        run_sledgehammer (get_params false thy override_params) false i
+                         relevance_override (minimize_command override_params i)
+                         state
+        |> K ()
       end
     else if subcommand = minimizeN then
-      run_minimize (get_params thy override_params) (the_default 1 opt_i)
+      run_minimize (get_params false thy override_params) (the_default 1 opt_i)
                    (#add relevance_override) state
     else if subcommand = messagesN then
       messages opt_i
@@ -254,7 +266,7 @@
 fun sledgehammer_params_trans params =
   Toplevel.theory
       (fold set_default_raw_param params
-       #> tap (fn thy => 
+       #> tap (fn thy =>
                   writeln ("Default parameters for Sledgehammer:\n" ^
                            (case rev (default_raw_params thy) of
                               [] => "none"
@@ -270,14 +282,13 @@
 val parse_fact_refs =
   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
 val parse_relevance_chunk =
-  (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
-  || (Args.del |-- Args.colon |-- parse_fact_refs
-      >> del_from_relevance_override)
+  (Args.add |-- Args.colon |-- parse_fact_refs >> add_relevance_override)
+  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_relevance_override)
   || (parse_fact_refs >> only_relevance_override)
 val parse_relevance_override =
   Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
                               >> merge_relevance_overrides))
-                (add_to_relevance_override [])
+                no_relevance_override
 val parse_sledgehammer_command =
   (Scan.optional Parse.short_ident runN -- parse_params
    -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
@@ -293,4 +304,16 @@
       "set and display the default parameters for Sledgehammer" Keyword.thy_decl
       parse_sledgehammer_params_command
 
+fun auto_sledgehammer state =
+  if not (!auto) then
+    (false, state)
+  else
+    let val thy = Proof.theory_of state in
+      run_sledgehammer (get_params true thy []) true 1 no_relevance_override
+                       (minimize_command [] 1) state
+    end
+
+val setup =
+  Auto_Counterexample.register_tool ("sledgehammer", auto_sledgehammer)
+
 end;
diff -r 6ec8d4683699 -r ad9a1f9b0558 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Sep 11 10:20:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Sep 11 10:21:52 2010 +0200
@@ -60,7 +60,7 @@
     val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
     val {context = ctxt, goal, ...} = Proof.goal state
     val problem =
-      {ctxt = ctxt, goal = goal, subgoal = subgoal,
+      {state = state, goal = goal, subgoal = subgoal,
        axioms = map (prepare_axiom ctxt) axioms}
     val result as {outcome, used_thm_names, ...} = prover params (K "") problem
   in
diff -r 6ec8d4683699 -r ad9a1f9b0558 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Sep 11 10:20:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Sep 11 10:21:52 2010 +0200
@@ -25,7 +25,7 @@
   val strip_subgoal : thm -> int -> (string * typ) list * term list * term
   val reserved_isar_keyword_table : unit -> unit Symtab.table
 end;
- 
+
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
 struct