--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 18:39:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 19:16:44 2013 +0100
@@ -18,6 +18,7 @@
struct
open Sledgehammer_Util
+open Sledgehammer_Reconstructor
open Sledgehammer_Proof
open Sledgehammer_Preplay
@@ -93,7 +94,7 @@
(* Precondition: The proof must be labeled canonically
(cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
fun compress_proof isar_compress
- ({get_preplay_result, set_preplay_result, preplay_quietly, ...} : preplay_interface) proof =
+ ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface) proof =
if isar_compress <= 1.0 then
proof
else
@@ -135,7 +136,7 @@
fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
if null subs orelse not (compress_further ()) then
- (set_preplay_result l (Preplay_Success (false, time));
+ (set_preplay_outcome l (Played time);
Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
else
(case subs of
@@ -145,7 +146,7 @@
val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
(* only touch proofs that can be preplayed sucessfully *)
- val Preplay_Success (false, time') = get_preplay_result l'
+ val Played time' = get_preplay_outcome l'
(* merge steps *)
val subs'' = subs @ nontriv_subs
@@ -158,7 +159,7 @@
(* check if the modified step can be preplayed fast enough *)
val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
- val Preplay_Success (false, time'') = preplay_quietly timeout step''
+ val Played time'' = preplay_quietly timeout step''
in
decrement_step_count (); (* l' successfully eliminated! *)
@@ -174,9 +175,8 @@
if subproofs = [] then
step
else
- (case get_preplay_result l of
- Preplay_Success (false, time) =>
- elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+ (case get_preplay_outcome l of
+ Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
| _ => step)
(** top_level compression: eliminate steps by merging them into their
@@ -211,10 +211,10 @@
fun try_eliminate (i, l, _) succ_lbls steps =
let
(* only touch steps that can be preplayed successfully *)
- val Preplay_Success (false, time) = get_preplay_result l
+ val Played time = get_preplay_outcome l
val succ_times =
- map (get_preplay_result #> (fn Preplay_Success (false, t) => t)) succ_lbls
+ map (get_preplay_outcome #> (fn Played t => t)) succ_lbls
val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
val timeouts =
map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
@@ -232,17 +232,17 @@
val succs' = map (try_merge cand #> the) succs
(* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
- val preplay_results = map2 preplay_quietly timeouts succs'
+ val play_outcomes = map2 preplay_quietly timeouts succs'
(* ensure none of the modified successors timed out *)
- val true = List.all (fn Preplay_Success _ => true) preplay_results
+ val true = List.all (fn Played _ => true) play_outcomes
val (steps1, _ :: steps2) = chop i steps
(* replace successors with their modified versions *)
val steps2 = update_steps steps2 succs'
in
decrement_step_count (); (* candidate successfully eliminated *)
- map2 set_preplay_result succ_lbls preplay_results;
+ map2 set_preplay_outcome succ_lbls play_outcomes;
map (replace_successor l succ_lbls) lfs;
(* removing the step would mess up the indices -> replace with dummy step instead *)
steps1 @ dummy_isar_step :: steps2
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Thu Dec 19 18:39:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Thu Dec 19 19:16:44 2013 +0100
@@ -19,16 +19,17 @@
struct
open Sledgehammer_Util
+open Sledgehammer_Reconstructor
open Sledgehammer_Proof
open Sledgehammer_Preplay
val slack = seconds 0.1
fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
- | min_deps_of_step {get_preplay_result, set_preplay_result, preplay_quietly, ...}
+ | min_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
(step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
- (case get_preplay_result l of
- Preplay_Success (false, time) =>
+ (case get_preplay_outcome l of
+ Played time =>
let
fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
@@ -36,13 +37,13 @@
fun minimize_facts _ time min_facts [] = (time, min_facts)
| minimize_facts mk_step time min_facts (f :: facts) =
(case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of
- Preplay_Success (false, time) => minimize_facts mk_step time min_facts facts
+ Played time => minimize_facts mk_step time min_facts facts
| _ => minimize_facts mk_step time (f :: min_facts) facts)
val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
in
- set_preplay_result l (Preplay_Success (false, time)); mk_step_lfs_gfs min_lfs min_gfs
+ set_preplay_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs
end
| _ => step (* don't touch steps that time out or fail *))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Dec 19 18:39:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Dec 19 19:16:44 2013 +0100
@@ -7,21 +7,18 @@
signature SLEDGEHAMMER_PREPLAY =
sig
+ type play_outcome = Sledgehammer_Reconstructor.play_outcome
type isar_proof = Sledgehammer_Proof.isar_proof
type isar_step = Sledgehammer_Proof.isar_step
type label = Sledgehammer_Proof.label
- datatype preplay_result =
- Preplay_Success of bool * Time.time |
- Preplay_Failure
-
val trace: bool Config.T
type preplay_interface =
- {get_preplay_result: label -> preplay_result,
- set_preplay_result: label -> preplay_result -> unit,
- preplay_quietly: Time.time -> isar_step -> preplay_result,
- overall_preplay_stats: isar_proof -> preplay_result}
+ {get_preplay_outcome: label -> play_outcome,
+ set_preplay_outcome: label -> play_outcome -> unit,
+ preplay_quietly: Time.time -> isar_step -> play_outcome,
+ overall_preplay_stats: isar_proof -> play_outcome}
val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time ->
isar_proof -> preplay_interface
@@ -32,20 +29,15 @@
open ATP_Util
open Sledgehammer_Util
+open Sledgehammer_Reconstructor
open Sledgehammer_Proof
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
-datatype preplay_result =
- Preplay_Success of bool * Time.time |
- Preplay_Failure
-
-val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
-
-fun preplay_trace ctxt assms concl time =
+fun preplay_trace ctxt assms concl result =
let
val ctxt = ctxt |> Config.put show_markup true
- val time = "[" ^ string_of_ext_time time ^ "]" |> Pretty.str
+ val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str
val nr_of_assms = length assms
val assms = assms
|> map (Display.pretty_thm ctxt)
@@ -65,9 +57,8 @@
fun take_time timeout tac arg =
let val timing = Timing.start () in
- (TimeLimit.timeLimit timeout tac arg;
- Timing.result timing |> #cpu |> pair false)
- handle TimeLimit.TimeOut => (true, timeout)
+ (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing)))
+ handle TimeLimit.TimeOut => Play_Timed_Out timeout
end
fun resolve_fact_names ctxt names =
@@ -114,7 +105,7 @@
| _ => raise Fail "Sledgehammer_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
-fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time
+fun preplay_raw _ _ _ _ _ (Let _) = Played Time.zeroTime
| preplay_raw debug type_enc lam_trans ctxt timeout
(Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) =
let
@@ -147,20 +138,20 @@
HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts))
handle ERROR msg => error ("Preplay error: " ^ msg)
- val preplay_time = take_time timeout prove ()
+ val play_outcome = take_time timeout prove ()
in
- (if Config.get ctxt trace then preplay_trace ctxt facts goal preplay_time else ();
- preplay_time)
+ (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
+ play_outcome)
end
(*** proof preplay interface ***)
type preplay_interface =
- {get_preplay_result: label -> preplay_result,
- set_preplay_result: label -> preplay_result -> unit,
- preplay_quietly: Time.time -> isar_step -> preplay_result,
- overall_preplay_stats: isar_proof -> preplay_result}
+ {get_preplay_outcome: label -> play_outcome,
+ set_preplay_outcome: label -> play_outcome -> unit,
+ preplay_quietly: Time.time -> isar_step -> play_outcome,
+ overall_preplay_stats: isar_proof -> play_outcome}
fun enrich_context_with_local_facts proof ctxt =
let
@@ -180,9 +171,12 @@
enrich_with_proof proof ctxt
end
-fun merge_preplay_results (Preplay_Success (b1, t1)) (Preplay_Success (b2, t2)) =
- Preplay_Success (b1 orelse b2, Time.+ (t1, t2))
- | merge_preplay_results _ _ = Preplay_Failure
+fun merge_preplay_outcomes _ Play_Failed = Play_Failed
+ | merge_preplay_outcomes Play_Failed _ = Play_Failed
+ | merge_preplay_outcomes (Play_Timed_Out t1) (Play_Timed_Out t2) = Play_Timed_Out (Time.+ (t1, t2))
+ | merge_preplay_outcomes (Played t1) (Play_Timed_Out t2) = Play_Timed_Out (Time.+ (t1, t2))
+ | merge_preplay_outcomes (Play_Timed_Out t1) (Played t2) = Play_Timed_Out (Time.+ (t1, t2))
+ | merge_preplay_outcomes (Played t1) (Played t2) = Played (Time.+ (t1, t2))
(* Given a proof, produces an imperative preplay interface with a shared table mapping from labels
to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated
@@ -192,17 +186,17 @@
"Slegehammer_Proof.relabel_proof_canonically". *)
fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
if not do_preplay then
- (* the dont_preplay option pretends that everything works just fine *)
- {get_preplay_result = K (Preplay_Success zero_preplay_time),
- set_preplay_result = K (K ()),
- preplay_quietly = K (K (Preplay_Success zero_preplay_time)),
- overall_preplay_stats = K (Preplay_Success zero_preplay_time)} : preplay_interface
+ (* the "dont_preplay" option pretends that everything works just fine *)
+ {get_preplay_outcome = K (Played Time.zeroTime),
+ set_preplay_outcome = K (K ()),
+ preplay_quietly = K (K (Played Time.zeroTime)),
+ overall_preplay_stats = K (Played Time.zeroTime)} : preplay_interface
else
let
val ctxt = enrich_context_with_local_facts proof ctxt
fun preplay quietly timeout step =
- Preplay_Success (preplay_raw debug type_enc lam_trans ctxt timeout step)
+ preplay_raw debug type_enc lam_trans ctxt timeout step
handle exn =>
if Exn.is_interrupt exn then
reraise exn
@@ -212,7 +206,7 @@
@{make_string} exn)
else
();
- Preplay_Failure)
+ Play_Failed)
(* preplay steps treating exceptions like timeouts *)
fun preplay_quietly timeout = preplay true timeout
@@ -232,23 +226,22 @@
|> Unsynchronized.ref
end
- fun get_preplay_result l =
+ fun get_preplay_outcome l =
Canonical_Lbl_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
handle Option.Option => raise Fail "Sledgehammer_Preplay: preplay time table"
- fun set_preplay_result l result =
+ fun set_preplay_outcome l result =
preplay_tab := Canonical_Lbl_Tab.update (l, Lazy.value result) (!preplay_tab)
val result_of_step =
- try (label_of_step #> the #> get_preplay_result)
- #> the_default (Preplay_Success zero_preplay_time)
+ try (label_of_step #> the #> get_preplay_outcome)
+ #> the_default (Played Time.zeroTime)
fun overall_preplay_stats (Proof (_, _, steps)) =
- Preplay_Success (false, Time.zeroTime)
- |> fold_isar_steps (merge_preplay_results o result_of_step) steps
+ fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
in
- {get_preplay_result = get_preplay_result,
- set_preplay_result = set_preplay_result,
+ {get_preplay_outcome = get_preplay_outcome,
+ set_preplay_outcome = set_preplay_outcome,
preplay_quietly = preplay_quietly,
overall_preplay_stats = overall_preplay_stats}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 18:39:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 19:16:44 2013 +0100
@@ -1027,9 +1027,8 @@
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
- verbose timeout facts state subgoal reconstr
- [reconstr] of
+ (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,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 18:39:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 19:16:44 2013 +0100
@@ -212,7 +212,9 @@
|> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
|> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
val one_line_proof = one_line_proof_text 0 one_line_params
+
val do_preplay = preplay_timeout <> Time.zeroTime
+ val isar_try0 = isar_try0 andalso do_preplay
val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
@@ -355,7 +357,7 @@
|> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
preplay_timeout)
- val (preplay_result, isar_proof) =
+ val (play_outcome, isar_proof) =
isar_proof
|> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0)
preplay_interface
@@ -377,17 +379,12 @@
let
val msg =
(if verbose then
- let
- val num_steps = add_proof_steps (steps_of_proof isar_proof) 0
- in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end
+ let val num_steps = add_proof_steps (steps_of_proof isar_proof) 0 in
+ [string_of_int num_steps ^ " step" ^ plural_s num_steps]
+ end
else
[]) @
- (if do_preplay then
- [(case preplay_result of
- Preplay_Success ext_time => string_of_ext_time ext_time
- | Preplay_Failure => "may fail")]
- else
- [])
+ (if do_preplay then [string_of_play_outcome play_outcome] else [])
in
"\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
Active.sendback_markup [Markup.padding_command] isar_text
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Thu Dec 19 18:39:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Thu Dec 19 19:16:44 2013 +0100
@@ -19,6 +19,8 @@
Play_Failed |
Not_Played
+ val string_of_play_outcome: play_outcome -> string
+
type minimize_command = string list -> string
type one_line_params =
(reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
@@ -29,6 +31,7 @@
structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
struct
+open ATP_Util
open ATP_Problem_Generate
datatype reconstructor =
@@ -41,6 +44,11 @@
Play_Failed |
Not_Played
+fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
+ | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
+ | string_of_play_outcome Play_Failed = "failed"
+ | string_of_play_outcome _ = "unknown"
+
type minimize_command = string list -> string
type one_line_params =
(reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Thu Dec 19 18:39:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Thu Dec 19 19:16:44 2013 +0100
@@ -18,6 +18,7 @@
struct
open Sledgehammer_Util
+open Sledgehammer_Reconstructor
open Sledgehammer_Proof
open Sledgehammer_Preplay
@@ -29,21 +30,21 @@
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
- ({get_preplay_result, set_preplay_result, preplay_quietly, ...} : preplay_interface)
+ ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface)
(step as Prove (_, _, l, _, _, _)) =
let
val timeout =
- (case get_preplay_result l of
- Preplay_Success (false, t) => Time.+ (t, slack)
+ (case get_preplay_outcome l of
+ Played time => Time.+ (time, slack)
| _ => preplay_timeout)
fun try_variant variant =
(case preplay_quietly timeout variant of
- result as Preplay_Success _ => SOME (variant, result)
+ result as Played _ => SOME (variant, result)
| _ => NONE)
in
(case Par_List.get_some try_variant (variants_of_step step) of
- SOME (step', result) => (set_preplay_result l result; step')
+ SOME (step', result) => (set_preplay_outcome l result; step')
| NONE => step)
end