--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 27 10:30:08 2011 +0200
@@ -327,7 +327,8 @@
hd (#provers (Sledgehammer_Isar.default_params ctxt []))
handle Empty => error "No ATP available."
fun get_prover name =
- (name, Sledgehammer_Run.get_minimizing_prover ctxt false name)
+ (name, Sledgehammer_Run.get_minimizing_prover ctxt
+ Sledgehammer_Provers.Normal name)
in
(case AList.lookup (op =) args proverK of
SOME name => get_prover name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:08 2011 +0200
@@ -232,7 +232,7 @@
val infinity_time_in_secs = 60 * 60 * 24 * 365
val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
-fun extract_params auto default_params override_params =
+fun extract_params mode default_params override_params =
let
val override_params = map unalias_raw_param override_params
val raw_params = rev override_params @ rev default_params
@@ -266,19 +266,19 @@
case lookup name of
SOME "smart" => NONE
| _ => SOME (lookup_int name)
- val debug = not auto andalso lookup_bool "debug"
- val verbose = debug orelse (not auto andalso lookup_bool "verbose")
+ val debug = mode <> Auto_Try andalso lookup_bool "debug"
+ val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
val blocking =
- Isabelle_Process.is_active () orelse auto orelse debug orelse
+ Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
lookup_bool "blocking"
val provers = lookup_string "provers" |> space_explode " "
- |> auto ? single o hd
+ |> mode = Auto_Try ? single o hd
val type_sys =
- if auto then
+ if mode = Auto_Try then
Smart_Type_Sys true
else case lookup_string "type_sys" of
- "smart" => Smart_Type_Sys (lookup_bool "full_types")
+ "smart" => Smart_Type_Sys (mode = Try orelse lookup_bool "full_types")
| s => Dumb_Type_Sys (type_sys_from_string s)
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
val max_relevant = lookup_int_option "max_relevant"
@@ -287,10 +287,11 @@
val explicit_apply = lookup_bool "explicit_apply"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
- val slicing = not auto andalso lookup_bool "slicing"
- val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
+ val slicing = mode <> Auto_Try andalso lookup_bool "slicing"
+ val timeout =
+ (if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout
val preplay_timeout =
- if auto then Time.zeroTime
+ if mode = Auto_Try then Time.zeroTime
else lookup_time "preplay_timeout" |> the_timeout
val expect = lookup_string "expect"
in
@@ -303,8 +304,8 @@
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
-fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)
-fun default_params thy = get_params false thy o map (apsnd single)
+fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)
+fun default_params thy = get_params Normal thy o map (apsnd single)
(* Sledgehammer the given subgoal *)
@@ -328,14 +329,14 @@
in
if subcommand = runN then
let val i = the_default 1 opt_i in
- run_sledgehammer (get_params false ctxt override_params) false i
+ run_sledgehammer (get_params Normal ctxt override_params) Normal i
relevance_override (minimize_command override_params i)
state
|> K ()
end
else if subcommand = minN then
- run_minimize (get_params false ctxt override_params) (the_default 1 opt_i)
- (#add relevance_override) state
+ run_minimize (get_params Minimize ctxt override_params)
+ (the_default 1 opt_i) (#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
else if subcommand = supported_proversN then
@@ -406,9 +407,10 @@
fun try_sledgehammer auto state =
let
val ctxt = Proof.context_of state
+ val mode = if auto then Auto_Try else Try
val i = 1
in
- run_sledgehammer (get_params auto ctxt []) auto i no_relevance_override
+ run_sledgehammer (get_params mode ctxt []) mode i no_relevance_override
(minimize_command [] i) state
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri May 27 10:30:08 2011 +0200
@@ -152,7 +152,7 @@
silent i n state facts =
let
val ctxt = Proof.context_of state
- val prover = get_prover ctxt false prover_name
+ val prover = get_prover ctxt Minimize prover_name
val msecs = Time.toMilliseconds timeout
val _ = print silent (fn () => "Sledgehammer minimize: " ^
quote prover_name ^ ".")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200
@@ -15,6 +15,8 @@
type type_system = Sledgehammer_ATP_Translate.type_system
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
+ datatype mode = Auto_Try | Try | Normal | Minimize
+
datatype rich_type_system =
Dumb_Type_Sys of type_system |
Smart_Type_Sys of bool
@@ -97,7 +99,7 @@
val kill_provers : unit -> unit
val running_provers : unit -> unit
val messages : int option -> unit
- val get_prover : Proof.context -> bool -> string -> prover
+ val get_prover : Proof.context -> mode -> string -> prover
end;
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
@@ -114,6 +116,8 @@
(** The Sledgehammer **)
+datatype mode = Auto_Try | Try | Normal | Minimize
+
(* Identifier to distinguish Sledgehammer from other tools using
"Async_Manager". *)
val das_tool = "Sledgehammer"
@@ -320,10 +324,13 @@
|> Exn.release
|> tap (after path)
-fun proof_banner auto blocking name =
- if auto then "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
- else if blocking then quote name ^ " found a proof"
- else "Try this command"
+fun proof_banner mode blocking name =
+ case mode of
+ Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
+ | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
+ | Normal => if blocking then quote name ^ " found a proof"
+ else "Try this command"
+ | Minimize => "Try this command"
val smt_triggers =
Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
@@ -473,7 +480,7 @@
#> Config.put SMT_Config.monomorph_limit max_mono_iters
#> Config.put SMT_Config.monomorph_instances max_mono_instances
-fun run_atp auto name
+fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,
conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
({debug, verbose, overlord, blocking, type_sys, max_relevant,
@@ -696,7 +703,7 @@
(output, msecs, type_sys, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name
val important_message =
- if not auto andalso
+ if mode = Normal andalso
random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
extract_important_message output
else
@@ -715,7 +722,7 @@
val isar_params =
(debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
val metis_params =
- (proof_banner auto blocking name, minimize_command, type_sys, atp_proof,
+ (proof_banner mode blocking name, minimize_command, type_sys, atp_proof,
facts_offset, fact_names, typed_helpers, goal, subgoal)
val (outcome, (message, used_facts)) =
case outcome of
@@ -894,7 +901,7 @@
| NONE => Preplay_Timed_Out
end
-fun run_smt_solver auto name
+fun run_smt_solver mode name
(params as {debug, verbose, blocking, preplay_timeout, ...})
minimize_command
({state, subgoal, subgoal_count, facts, smt_filter, ...}
@@ -920,7 +927,7 @@
else "smt_solver = " ^ maybe_quote name,
"smt", NONE)
in
- try_command_line (proof_banner auto blocking name)
+ try_command_line (proof_banner mode blocking name)
(apply_on_subgoal settings subgoal subgoal_count ^
command_call method (map fst other_lemmas)) ^
minimize_line minimize_command
@@ -938,12 +945,12 @@
run_time_in_msecs = run_time_in_msecs, message = message}
end
-fun get_prover ctxt auto name =
+fun get_prover ctxt mode name =
let val thy = Proof_Context.theory_of ctxt in
if is_smt_prover ctxt name then
- run_smt_solver auto name
+ run_smt_solver mode name
else if member (op =) (supported_atps thy) name then
- run_atp auto name (get_atp thy name)
+ run_atp mode name (get_atp thy name)
else
error ("No such prover: " ^ name ^ ".")
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:08 2011 +0200
@@ -10,6 +10,7 @@
sig
type relevance_override = Sledgehammer_Filter.relevance_override
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
+ type mode = Sledgehammer_Provers.mode
type params = Sledgehammer_Provers.params
type prover = Sledgehammer_Provers.prover
@@ -18,9 +19,9 @@
val timeoutN : string
val unknownN : string
val auto_minimize_min_facts : int Config.T
- val get_minimizing_prover : Proof.context -> bool -> string -> prover
+ val get_minimizing_prover : Proof.context -> mode -> string -> prover
val run_sledgehammer :
- params -> bool -> int -> relevance_override -> (string -> minimize_command)
+ params -> mode -> int -> relevance_override -> (string -> minimize_command)
-> Proof.state -> bool * (string * Proof.state)
end;
@@ -66,10 +67,10 @@
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
(fn generic => Config.get_generic generic binary_min_facts)
-fun get_minimizing_prover ctxt auto name
+fun get_minimizing_prover ctxt mode name
(params as {debug, verbose, explicit_apply, ...}) minimize_command
(problem as {state, subgoal, subgoal_count, facts, ...}) =
- get_prover ctxt auto name params minimize_command problem
+ get_prover ctxt mode name params minimize_command problem
|> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
if is_some outcome then
result
@@ -108,7 +109,7 @@
fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
expect, ...})
- auto minimize_command only
+ mode minimize_command only
{state, goal, subgoal, subgoal_count, facts, smt_filter} name =
let
val ctxt = Proof.context_of state
@@ -127,7 +128,7 @@
smt_filter = smt_filter}
fun really_go () =
problem
- |> get_minimizing_prover ctxt auto name params (minimize_command name)
+ |> get_minimizing_prover ctxt mode name params (minimize_command name)
|> (fn {outcome, message, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN
@@ -159,7 +160,7 @@
warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
in (outcome_code, message) end
in
- if auto then
+ if mode = Auto_Try then
let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
(outcome_code,
state
@@ -196,12 +197,12 @@
fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
| dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
-val auto_max_relevant_divisor = 2 (* FUDGE *)
+val auto_try_max_relevant_divisor = 2 (* FUDGE *)
fun run_sledgehammer (params as {debug, verbose, blocking, provers,
relevance_thresholds, max_relevant, slicing,
timeout, ...})
- auto i (relevance_override as {only, ...}) minimize_command state =
+ mode i (relevance_override as {only, ...}) minimize_command state =
if null provers then
error "No prover is set."
else case subgoal_count state of
@@ -209,7 +210,7 @@
| n =>
let
val _ = Proof.assert_backward state
- val print = if auto then K () else Output.urgent_message
+ val print = if mode = Normal then Output.urgent_message else K ()
val state =
state |> Proof.map_context (Config.put SMT_Config.verbose debug)
val ctxt = Proof.context_of state
@@ -234,11 +235,11 @@
facts = facts,
smt_filter = maybe_smt_filter
(fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
- val launch = launch_prover params auto minimize_command only
+ val launch = launch_prover params mode minimize_command only
in
- if auto then
+ if mode = Auto_Try orelse mode = Try then
(unknownN, state)
- |> fold (fn prover => fn accum as (outcome_code, state) =>
+ |> fold (fn prover => fn accum as (outcome_code, _) =>
if outcome_code = someN then accum
else launch problem prover)
provers
@@ -257,7 +258,8 @@
0 |> fold (Integer.max
o default_max_relevant_for_prover ctxt slicing)
provers
- |> auto ? (fn n => n div auto_max_relevant_divisor)
+ |> mode = Auto_Try
+ ? (fn n => n div auto_try_max_relevant_divisor)
val is_built_in_const =
is_built_in_const_for_prover ctxt (hd provers)
in
@@ -315,12 +317,15 @@
launch_atps "Unit equational provers" is_unit_equality ueq_atps
fun launch_atps_and_smt_solvers () =
[launch_full_atps, launch_ueq_atps, launch_smts]
- |> smart_par_list_map (fn f => f (unknownN, state) |> K ())
+ |> smart_par_list_map (fn f => ignore (f (unknownN, state)))
handle ERROR msg => (print ("Error: " ^ msg); error msg)
+ fun maybe f (accum as (outcome_code, _)) =
+ accum |> (mode = Normal orelse outcome_code <> someN) ? f
in
(unknownN, state)
|> (if blocking then
- launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts)
+ launch_full_atps
+ #> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts)
else
(fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
handle TimeLimit.TimeOut =>
--- a/src/HOL/ex/sledgehammer_tactics.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Fri May 27 10:30:08 2011 +0200
@@ -23,7 +23,8 @@
@ [("timeout", string_of_int (Time.toSeconds timeout))])
(* @ [("overlord", "true")] *)
|> Sledgehammer_Isar.default_params ctxt
- val prover = Sledgehammer_Provers.get_prover ctxt false name
+ val prover =
+ Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
val is_built_in_const =
--- a/src/Tools/try.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/try.ML Fri May 27 10:30:08 2011 +0200
@@ -57,6 +57,7 @@
fun try_tools state =
get_tools (Proof.theory_of state)
+ |> tap (fn _ => Output.urgent_message "Trying...")
|> Par_List.get_some
(fn (name, (_, tool)) =>
case try (tool false) state of