--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sun Feb 02 20:53:51 2014 +0100
@@ -98,7 +98,7 @@
(* Precondition: The proof must be labeled canonically
(cf. "Slegehammer_Isar_Proof.relabel_isar_proof_canonically"). *)
fun compress_isar_proof compress_isar
- ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data) proof =
+ ({preplay_step, preplay_outcome, set_preplay_outcomes, ...} : isar_preplay_data) proof =
if compress_isar <= 1.0 then
proof
else
@@ -161,8 +161,8 @@
val step'' = Prove (qs, fix, l, t, subs'', by)
(* check if the modified step can be preplayed fast enough *)
- val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
- val Played time'' = preplay_quietly timeout step''
+ val timeout = time_mult merge_timeout_slack (Time.+ (time, time'))
+ val Played time'' = preplay_step timeout (hd meths)(*FIXME*) step''
in
decrement_step_count (); (* l' successfully eliminated! *)
map (replace_successor l' [l]) lfs';
@@ -238,7 +238,7 @@
()
(* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
- val play_outcomes = map2 preplay_quietly timeouts succs'
+ val play_outcomes = map3 preplay_step timeouts succ_meths succs'
(* ensure none of the modified successors timed out *)
val true = forall (fn Played _ => true) play_outcomes
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 20:53:51 2014 +0100
@@ -26,7 +26,7 @@
val slack = seconds 0.1
fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
- | minimize_isar_step_dependencies {set_preplay_outcomes, preplay_outcome, preplay_quietly, ...}
+ | minimize_isar_step_dependencies {preplay_step, set_preplay_outcomes, preplay_outcome, ...}
(step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
(case Lazy.force (preplay_outcome l meth) of
Played time =>
@@ -36,7 +36,7 @@
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
+ (case preplay_step (Time.+ (time, slack)) meth (mk_step (min_facts @ facts)) of
Played time => minimize_facts mk_step time min_facts facts
| _ => minimize_facts mk_step time (f :: min_facts) facts)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100
@@ -16,9 +16,9 @@
val trace : bool Config.T
type isar_preplay_data =
- {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
+ {preplay_step: Time.time -> proof_method -> isar_step -> play_outcome,
+ set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
- preplay_quietly: Time.time -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> Time.time ->
@@ -95,7 +95,7 @@
| _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
-fun preplay_raw debug type_enc lam_trans ctxt timeout meth
+fun raw_preplay_step debug type_enc lam_trans ctxt timeout meth
(Prove (_, xs, _, t, subproofs, (fact_names, _))) =
let
val goal =
@@ -137,7 +137,7 @@
type isar_preplay_data =
{set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
- preplay_quietly: Time.time -> isar_step -> play_outcome,
+ preplay_step: Time.time -> proof_method -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
fun enrich_context_with_local_facts proof ctxt =
@@ -176,22 +176,9 @@
let
val ctxt = enrich_context_with_local_facts proof ctxt
- fun preplay quietly timeout meth step =
- preplay_raw debug type_enc lam_trans ctxt timeout meth step
- handle exn =>
- if Exn.is_interrupt exn then
- reraise exn
- else
- (if not quietly andalso debug then
- warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn)
- else
- ();
- Play_Failed)
-
- (* preplay steps treating exceptions like timeouts *)
- fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) =
- preplay true timeout meth step
- | preplay_quietly _ _ = Played Time.zeroTime
+ fun preplay_step timeout meth =
+ try (raw_preplay_step debug type_enc lam_trans ctxt timeout meth)
+ #> the_default Play_Failed
val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
@@ -216,15 +203,15 @@
fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
- (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
+ (meth, Lazy.lazy (fn () => preplay_step preplay_timeout meth step))) meths)
(!preplay_tab)
| reset_preplay_outcomes _ = ()
val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
in
- {set_preplay_outcomes = set_preplay_outcomes,
+ {preplay_step = preplay_step,
+ set_preplay_outcomes = set_preplay_outcomes,
preplay_outcome = preplay_outcome,
- preplay_quietly = preplay_quietly,
overall_preplay_outcome = overall_preplay_outcome}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Sun Feb 02 20:53:51 2014 +0100
@@ -22,31 +22,30 @@
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
-fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meths))) =
- map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) (tl meths)
- | variants_of_step _ = raise Fail "Sledgehammer_Isar_Try0: variants_of_step"
+fun step_with_method meth (Prove (qs, xs, l, t, subproofs, (facts, _))) =
+ Prove (qs, xs, l, t, subproofs, (facts, [meth]))
val slack = seconds 0.05
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
- ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data)
- (step as Prove (_, _, l, _, _, (_, meth :: _))) =
+ ({preplay_step, set_preplay_outcomes, preplay_outcome, ...} : isar_preplay_data)
+ (step as Prove (_, _, l, _, _, (_, meths as meth :: _))) =
let
val timeout =
(case Lazy.force (preplay_outcome l meth) of
Played time => Time.+ (time, slack)
| _ => preplay_timeout)
- fun try_variant variant =
- (case preplay_quietly timeout variant of
- result as Played _ => SOME (variant, result)
+ fun try_method meth =
+ (case preplay_step timeout meth step of
+ outcome as Played _ => SOME (meth, outcome)
| _ => NONE)
in
(* FIXME: create variant after success *)
- (case Par_List.get_some try_variant (variants_of_step step) of
- SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), outcome) =>
- (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step')
+ (case Par_List.get_some try_method meths of
+ SOME (meth', outcome) =>
+ (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step_with_method meth' step)
| NONE => step)
end