# HG changeset patch
# User blanchet
# Date 1292673236 -3600
# Node ID 4cac389c005faafe781dea84fe6f2068315cb1f8
# Parent  095ecb0c687f5b781bd2a35d9ad19d9d57ed50e2
renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"

diff -r 095ecb0c687f -r 4cac389c005f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 18 12:46:58 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 18 12:53:56 2010 +0100
@@ -11,12 +11,9 @@
   type relevance_override = Sledgehammer_Filter.relevance_override
   type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
   type params = Sledgehammer_Provers.params
-  type prover_problem = Sledgehammer_Provers.prover_problem
-  type prover_result = Sledgehammer_Provers.prover_result
+  type prover = Sledgehammer_Provers.prover
 
-  val run_prover :
-    params -> bool -> (string -> minimize_command) -> prover_problem -> string
-    -> prover_result
+  val get_minimizing_prover : Proof.context -> bool -> string -> prover
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
     -> Proof.state -> bool * Proof.state
@@ -46,45 +43,44 @@
 
 val implicit_minimization_threshold = 50
 
-fun run_prover (params as {debug, verbose, ...}) auto minimize_command
-               (problem as {state, subgoal, subgoal_count, facts, ...}) name =
-  let val ctxt = Proof.context_of state in
-    get_prover ctxt auto name params (minimize_command name) problem
-    |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
-           if is_some outcome then
-             result
-           else
-             let
-               val (used_facts, message) =
-                 if length used_facts >= implicit_minimization_threshold then
-                   minimize_facts params (not verbose) subgoal subgoal_count
-                       state
-                       (filter_used_facts used_facts
-                            (map (apsnd single o untranslated_fact) facts))
-                   |>> Option.map (map fst)
-                 else
-                   (SOME used_facts, message)
-             in
-               case used_facts of
-                 SOME used_facts =>
-                 (if debug andalso not (null used_facts) then
-                    facts ~~ (0 upto length facts - 1)
-                    |> map (fn (fact, j) =>
-                               fact |> untranslated_fact |> apsnd (K j))
-                    |> filter_used_facts used_facts
-                    |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
-                    |> commas
-                    |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^
-                                quote name ^ " proof (of " ^
-                                string_of_int (length facts) ^ "): ") "."
-                    |> Output.urgent_message
-                  else
-                    ();
-                  {outcome = NONE, used_facts = used_facts,
-                   run_time_in_msecs = run_time_in_msecs, message = message})
-               | NONE => result
-             end)
-  end
+fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...})
+        minimize_command
+        (problem as {state, subgoal, subgoal_count, facts, ...}) =
+  get_prover ctxt auto name params minimize_command problem
+  |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
+         if is_some outcome then
+           result
+         else
+           let
+             val (used_facts, message) =
+               if length used_facts >= implicit_minimization_threshold then
+                 minimize_facts params (not verbose) subgoal subgoal_count
+                     state
+                     (filter_used_facts used_facts
+                          (map (apsnd single o untranslated_fact) facts))
+                 |>> Option.map (map fst)
+               else
+                 (SOME used_facts, message)
+           in
+             case used_facts of
+               SOME used_facts =>
+               (if debug andalso not (null used_facts) then
+                  facts ~~ (0 upto length facts - 1)
+                  |> map (fn (fact, j) =>
+                             fact |> untranslated_fact |> apsnd (K j))
+                  |> filter_used_facts used_facts
+                  |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
+                  |> commas
+                  |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^
+                              quote name ^ " proof (of " ^
+                              string_of_int (length facts) ^ "): ") "."
+                  |> Output.urgent_message
+                else
+                  ();
+                {outcome = NONE, used_facts = used_facts,
+                 run_time_in_msecs = run_time_in_msecs, message = message})
+             | NONE => result
+           end)
 
 fun launch_prover
         (params as {debug, blocking, max_relevant, timeout, expect, ...})
@@ -104,7 +100,8 @@
        subgoal_count = subgoal_count, facts = take num_facts facts,
        smt_head = smt_head}
     fun really_go () =
-      run_prover params auto minimize_command problem name
+      problem
+      |> get_minimizing_prover ctxt auto name params (minimize_command name)
       |> (fn {outcome, message, ...} =>
              (if is_some outcome then "none" else "some" (* sic *), message))
     fun go () =