--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Dec 17 23:18:39 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Dec 18 12:46:58 2010 +0100
@@ -11,7 +11,12 @@
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
+ val run_prover :
+ params -> bool -> (string -> minimize_command) -> prover_problem -> string
+ -> prover_result
val run_sledgehammer :
params -> bool -> int -> relevance_override -> (string -> minimize_command)
-> Proof.state -> bool * Proof.state
@@ -41,9 +46,50 @@
val implicit_minimization_threshold = 50
-fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...})
- auto minimize_command only
- {state, goal, subgoal, subgoal_count, facts, smt_head} name =
+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 launch_prover
+ (params as {debug, blocking, max_relevant, timeout, expect, ...})
+ auto minimize_command only
+ {state, goal, subgoal, subgoal_count, facts, smt_head} name =
let
val ctxt = Proof.context_of state
val birth_time = Time.now ()
@@ -53,41 +99,14 @@
val num_facts = length facts |> not only ? Integer.min max_relevant
val desc =
prover_description ctxt params name num_facts subgoal subgoal_count goal
- val prover = get_prover ctxt auto name
val problem =
{state = state, goal = goal, subgoal = subgoal,
subgoal_count = subgoal_count, facts = take num_facts facts,
smt_head = smt_head}
fun really_go () =
- prover params (minimize_command name) problem
- |> (fn {outcome, used_facts, message, ...} =>
- if is_some outcome then
- ("none", message)
- else
- let
- val (used_facts, message) =
- if length used_facts >= implicit_minimization_threshold then
- minimize_facts params true 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)
- val _ =
- case (debug, used_facts) of
- (true, SOME (used_facts as _ :: _)) =>
- 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 num_facts ^ " in " ^
- quote name ^ " proof (of " ^
- string_of_int num_facts ^ "): ") "."
- |> Output.urgent_message
- | _ => ()
- in ("some", message) end)
+ run_prover params auto minimize_command problem name
+ |> (fn {outcome, message, ...} =>
+ (if is_some outcome then "none" else "some" (* sic *), message))
fun go () =
let
val (outcome_code, message) =
@@ -171,7 +190,7 @@
| NONE => ()
val _ = if auto then () else Output.urgent_message "Sledgehammering..."
val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
- fun run_provers state get_facts translate maybe_smt_head provers =
+ fun launch_provers state get_facts translate maybe_smt_head provers =
let
val facts = get_facts ()
val num_facts = length facts
@@ -182,16 +201,15 @@
facts = facts,
smt_head = maybe_smt_head
(fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
- val run_prover = run_prover params auto minimize_command only
+ val launch = launch_prover params auto minimize_command only
in
if auto then
fold (fn prover => fn (true, state) => (true, state)
- | (false, _) => run_prover problem prover)
+ | (false, _) => launch problem prover)
provers (false, state)
else
provers
- |> (if blocking then smart_par_list_map else map)
- (run_prover problem)
+ |> (if blocking then smart_par_list_map else map) (launch problem)
|> exists fst |> rpair state
end
fun get_facts label no_dangerous_types relevance_fudge provers =
@@ -222,15 +240,15 @@
else
())
end
- fun run_atps (accum as (success, _)) =
+ fun launch_atps (accum as (success, _)) =
if success orelse null atps then
accum
else
- run_provers state
+ launch_provers state
(get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
(ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
(K (K NONE)) atps
- fun run_smts (accum as (success, _)) =
+ fun launch_smts (accum as (success, _)) =
if success orelse null smts then
accum
else
@@ -242,17 +260,17 @@
in
smts |> map (`(class_of_smt_solver ctxt))
|> AList.group (op =)
- |> map (run_provers state (K facts) weight smt_head o snd)
+ |> map (launch_provers state (K facts) weight smt_head o snd)
|> exists fst |> rpair state
end
- fun run_atps_and_smt_solvers () =
- [run_atps, run_smts]
+ fun launch_atps_and_smt_solvers () =
+ [launch_atps, launch_smts]
|> smart_par_list_map (fn f => f (false, state) |> K ())
handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg)
in
(false, state)
- |> (if blocking then run_atps #> not auto ? run_smts
- else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
+ |> (if blocking then launch_atps #> not auto ? launch_smts
+ else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
end
end;