--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 19 17:24:17 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 19 17:52:58 2013 +0100
@@ -8,7 +8,8 @@
signature SLEDGEHAMMER_MINIMIZE =
sig
type stature = ATP_Problem_Generate.stature
- type play = Sledgehammer_Reconstructor.play
+ type reconstructor = Sledgehammer_Reconstructor.reconstructor
+ type play_outcome = Sledgehammer_Reconstructor.play_outcome
type mode = Sledgehammer_Provers.mode
type params = Sledgehammer_Provers.params
type prover = Sledgehammer_Provers.prover
@@ -16,12 +17,12 @@
val binary_min_facts : int Config.T
val auto_minimize_min_facts : int Config.T
val auto_minimize_max_time : real Config.T
- val minimize_facts :
- (thm list -> unit) -> string -> params -> bool -> int -> int
- -> Proof.state -> thm -> play Lazy.lazy option
- -> ((string * stature) * thm list) list
- -> ((string * stature) * thm list) list option
- * (play Lazy.lazy * (play -> string) * string)
+ val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
+ Proof.state -> thm -> (reconstructor * play_outcome) Lazy.lazy option ->
+ ((string * stature) * thm list) list ->
+ ((string * stature) * thm list) list option
+ * ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string)
+ * string)
val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list ->
Proof.state -> unit
@@ -53,11 +54,10 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
-fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters,
- max_new_mono_instances, type_enc, strict, lam_trans,
- uncurried_aliases, isar_proofs, isar_compress, isar_try0,
- preplay_timeout, ...} : params)
- silent (prover : prover) timeout i n state goal facts =
+fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
+ type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, isar_compress, isar_try0,
+ preplay_timeout, ...} : params)
+ silent (prover : prover) timeout i n state goal facts =
let
val _ =
print silent (fn () =>
@@ -220,7 +220,7 @@
"Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
\timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", ""))
| {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, "")))
- handle ERROR msg => (NONE, (Lazy.value (Play_Failed plain_metis), fn _ => "Error: " ^ msg, ""))
+ handle ERROR msg => (NONE, (Lazy.value (plain_metis, Play_Failed), fn _ => "Error: " ^ msg, ""))
end
fun adjust_reconstructor_params override_params
@@ -270,7 +270,7 @@
fun prover_fast_enough () = can_min_fast_enough run_time
in
(case Lazy.force preplay of
- Played (reconstr as Metis _, timeout) =>
+ (reconstr as Metis _, Played timeout) =>
if isar_proofs = SOME true then
(* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
itself. *)
@@ -281,7 +281,7 @@
adjust_reconstructor_params override_params params))
else
(prover_fast_enough (), (name, params))
- | Played (SMT, timeout) =>
+ | (SMT, Played timeout) =>
(* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
itself. *)
(can_min_fast_enough timeout, (name, params))
@@ -294,9 +294,8 @@
val (used_facts, (preplay, message, _)) =
if minimize then
minimize_facts do_learn minimize_name params
- (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal
- subgoal_count state goal (SOME preplay)
- (filter_used_facts true used_facts (map (apsnd single) used_from))
+ (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state
+ goal (SOME preplay) (filter_used_facts true used_facts (map (apsnd single) used_from))
|>> Option.map (map fst)
else
(SOME used_facts, (preplay, message, ""))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Dec 19 17:24:17 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Dec 19 17:52:58 2013 +0100
@@ -82,15 +82,15 @@
|> pairself (sort_distinct (string_ord o pairself fst))
fun one_line_proof_text num_chained
- (preplay, banner, used_facts, minimize_command, subgoal, subgoal_count) =
+ ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
let
val (chained, extra) = split_used_facts used_facts
- val (failed, reconstr, ext_time) =
- (case preplay of
- Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
- | Not_Played reconstr => (false, reconstr, NONE)
- | Play_Timed_Out (reconstr, time) => (false, reconstr, SOME (true, time))
- | Play_Failed reconstr => (true, reconstr, NONE))
+ val (failed, ext_time) =
+ (case play of
+ Played time => (false, (SOME (false, time)))
+ | Play_Timed_Out time => (false, SOME (true, time))
+ | Play_Failed => (true, NONE)
+ | Not_Played => (false, NONE))
val try_line =
([], map fst extra)
|> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
@@ -111,10 +111,9 @@
fun string_of_proof ctxt type_enc lam_trans i n proof =
let
+ (* Make sure only type constraints inserted by the type annotation code are printed. *)
val ctxt =
- (* make sure type constraint are actually printed *)
ctxt |> Config.put show_markup false
- (* make sure only type constraints inserted by sh_annotate are printed *)
|> Config.put Printer.show_type_emphasis false
|> Config.put show_types false
|> Config.put show_sorts false
@@ -195,9 +194,10 @@
(s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
fun add_fix _ [] = I
- | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
- #> add_frees xs
- #> add_suffix "\n"
+ | add_fix ind xs =
+ add_suffix (of_indent ind ^ "fix ")
+ #> add_frees xs
+ #> add_suffix "\n"
fun add_assm ind (l, t) =
add_suffix (of_indent ind ^ "assume " ^ of_label l)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 17:24:17 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 17:52:58 2013 +0100
@@ -13,7 +13,7 @@
type type_enc = ATP_Problem_Generate.type_enc
type fact = Sledgehammer_Fact.fact
type reconstructor = Sledgehammer_Reconstructor.reconstructor
- type play = Sledgehammer_Reconstructor.play
+ type play_outcome = Sledgehammer_Reconstructor.play_outcome
type minimize_command = Sledgehammer_Reconstructor.minimize_command
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
@@ -57,8 +57,8 @@
used_facts : (string * stature) list,
used_from : fact list,
run_time : Time.time,
- preplay : play Lazy.lazy,
- message : play -> string,
+ preplay : (reconstructor * play_outcome) Lazy.lazy,
+ message : reconstructor * play_outcome -> string,
message_tail : string}
type prover =
@@ -298,8 +298,8 @@
used_facts : (string * stature) list,
used_from : fact list,
run_time : Time.time,
- preplay : play Lazy.lazy,
- message : play -> string,
+ preplay : (reconstructor * play_outcome) Lazy.lazy,
+ message : reconstructor * play_outcome -> string,
message_tail : string}
type prover =
@@ -358,18 +358,13 @@
Metis (really_full_type_enc, lam_trans true),
SMT]
-fun extract_reconstructor ({type_enc, lam_trans, ...} : params)
- (Metis (type_enc', lam_trans')) =
+fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) =
let
val override_params =
- (if is_none type_enc andalso type_enc' = hd partial_type_encs then
- []
- else
- [("type_enc", [hd (unalias_type_enc type_enc')])]) @
- (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then
- []
- else
- [("lam_trans", [lam_trans'])])
+ (if is_none type_enc andalso type_enc' = hd partial_type_encs then []
+ else [("type_enc", [hd (unalias_type_enc type_enc')])]) @
+ (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then []
+ else [("lam_trans", [lam_trans'])])
in (metisN, override_params) end
| extract_reconstructor _ SMT = (smtN, [])
@@ -382,8 +377,7 @@
TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
end
-fun tac_of_reconstructor (Metis (type_enc, lam_trans)) =
- metis_tac [type_enc] lam_trans
+fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans
| tac_of_reconstructor SMT = SMT_Solver.smt_tac
fun timed_reconstructor reconstr debug timeout ths =
@@ -404,13 +398,13 @@
else List.last reconstrs
in
if timeout = Time.zeroTime then
- Not_Played (get_preferred reconstrs)
+ (get_preferred reconstrs, Not_Played)
else
let
val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
val ths = pairs |> sort_wrt (fst o fst) |> map snd
- fun play [] [] = Play_Failed (get_preferred reconstrs)
- | play timed_outs [] = Play_Timed_Out (get_preferred timed_outs, timeout)
+ fun play [] [] = (get_preferred reconstrs, Play_Failed)
+ | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
| play timed_out (reconstr :: reconstrs) =
let
val _ =
@@ -422,11 +416,13 @@
val timer = Timer.startRealTimer ()
in
case timed_reconstructor reconstr debug timeout ths state i of
- SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
+ SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer))
| _ => play timed_out reconstrs
end
handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
- in play [] reconstrs end
+ in
+ play [] reconstrs
+ end
end
@@ -511,17 +507,15 @@
(* See the analogous logic in the function "maybe_minimize" in
"sledgehammer_minimize.ML". *)
-fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command
- name preplay =
+fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command name preplay =
let
- val maybe_isar_name =
- name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
+ val maybe_isar_name = name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
val (min_name, override_params) =
- case preplay of
- Played (reconstr, _) =>
+ (case preplay of
+ (reconstr, Played _) =>
if isar_proofs = SOME true then (maybe_isar_name, [])
else extract_reconstructor params reconstr
- | _ => (maybe_isar_name, [])
+ | _ => (maybe_isar_name, []))
in minimize_command override_params min_name end
val max_fact_instances = 10 (* FUDGE *)
@@ -551,14 +545,13 @@
val max_fact_factor_fudge = 5
fun run_atp mode name
- ({exec, arguments, proof_delims, known_failures, prem_role, best_slices,
- best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
- (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
- uncurried_aliases, fact_filter, max_facts, max_mono_iters,
- max_new_mono_instances, isar_proofs, isar_compress,
- isar_try0, slice, timeout, preplay_timeout, ...})
- minimize_command
- ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+ ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
+ best_max_new_mono_instances, ...} : atp_config)
+ (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
+ fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, isar_compress,
+ isar_try0, slice, timeout, preplay_timeout, ...})
+ minimize_command
+ ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
@@ -776,7 +769,7 @@
else
""
val (used_facts, preplay, message, message_tail) =
- case outcome of
+ (case outcome of
NONE =>
let
val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
@@ -787,20 +780,13 @@
in
(used_facts,
Lazy.lazy (fn () =>
- let
- val used_pairs =
- used_from |> filter_used_facts false used_facts
- in
- play_one_line_proof mode debug verbose preplay_timeout
- used_pairs state subgoal (hd reconstrs) reconstrs
+ let val used_pairs = used_from |> filter_used_facts false used_facts in
+ play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+ (hd reconstrs) reconstrs
end),
fn preplay =>
let
- val _ =
- if verbose then
- Output.urgent_message "Generating proof text..."
- else
- ()
+ val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
fun isar_params () =
let
val metis_type_enc =
@@ -824,26 +810,19 @@
in
proof_text ctxt isar_proofs isar_params num_chained one_line_params
end,
- (if verbose then
- "\nATP real CPU time: " ^ string_of_time run_time ^ "."
- else
- "") ^
+ (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
(if important_message <> "" then
- "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
- important_message
+ "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
else
""))
end
| SOME failure =>
- ([], Lazy.value (Play_Failed plain_metis), fn _ => string_of_atp_failure failure, "")
+ ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
in
- {outcome = outcome, used_facts = used_facts, used_from = used_from,
- run_time = run_time, preplay = preplay, message = message,
- message_tail = message_tail}
+ {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
+ preplay = preplay, message = message, message_tail = message_tail}
end
-fun rotate_one (x :: xs) = xs @ [x]
-
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
these are sorted out properly in the SMT module, we have to interpret these
ourselves. *)
@@ -962,7 +941,7 @@
Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
val weighted_factss as (new_fact_filter, _) :: _ =
weighted_factss
- |> rotate_one
+ |> (fn (x :: xs) => xs @ [x])
|> app_hd (apsnd (take new_num_facts))
val show_filter = fact_filter <> new_fact_filter
fun num_of_facts fact_filter num_facts =
@@ -983,15 +962,15 @@
do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
end
else
- {outcome = if is_none outcome then NONE else the outcome0,
- used_facts = used_facts, used_from = map (apsnd snd) weighted_facts,
- run_time = time_so_far}
+ {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
+ used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
end
- in do_slice timeout 1 NONE Time.zeroTime end
+ in
+ do_slice timeout 1 NONE Time.zeroTime
+ end
-fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
- minimize_command
- ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command
+ ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val ctxt = Proof.context_of state
fun weight_facts facts =
@@ -1016,19 +995,15 @@
let
val one_line_params =
(preplay, proof_banner mode name, used_facts,
- choose_minimize_command ctxt params minimize_command name
- preplay,
+ choose_minimize_command ctxt params minimize_command name preplay,
subgoal, subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
one_line_proof_text num_chained one_line_params
end,
- if verbose then
- "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "."
- else
- "")
+ if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
| SOME failure =>
- (Lazy.value (Play_Failed plain_metis),
+ (Lazy.value (plain_metis, Play_Failed),
fn _ => string_of_atp_failure failure, "")
in
{outcome = outcome, used_facts = used_facts, used_from = used_from,
@@ -1052,20 +1027,19 @@
raise Fail ("unknown reconstructor: " ^ quote name)
val used_facts = facts |> map fst
in
- case play_one_line_proof (if mode = Minimize then Normal else mode) debug
+ (case play_one_line_proof (if mode = Minimize then Normal else mode) debug
verbose timeout facts state subgoal reconstr
[reconstr] of
- play as Played (_, time) =>
- {outcome = NONE, used_facts = used_facts, used_from = facts,
- run_time = time, preplay = Lazy.value play,
+ play as (_, Played time) =>
+ {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
+ preplay = Lazy.value play,
message =
fn play =>
let
val (_, override_params) = extract_reconstructor params reconstr
val one_line_params =
- (play, proof_banner mode name, used_facts,
- minimize_command override_params name, subgoal,
- subgoal_count)
+ (play, proof_banner mode name, used_facts, minimize_command override_params name,
+ subgoal, subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
one_line_proof_text num_chained one_line_params
@@ -1073,12 +1047,12 @@
message_tail = ""}
| play =>
let
- val failure = case play of Play_Failed _ => GaveUp | _ => TimedOut
+ val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
in
{outcome = SOME failure, used_facts = [], used_from = [],
run_time = Time.zeroTime, preplay = Lazy.value play,
message = fn _ => string_of_atp_failure failure, message_tail = ""}
- end
+ end)
end
fun get_prover ctxt mode name =