--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 10:19:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 11:30:53 2014 +0100
@@ -95,7 +95,7 @@
val compress_degree = 2
val merge_timeout_slack_time = seconds 0.005
-val merge_timeout_slack_factor = 1.5
+val merge_timeout_slack_factor = 1.25
fun slackify_merge_timeout time =
time_mult merge_timeout_slack_factor (Time.+ (merge_timeout_slack_time, time))
@@ -146,8 +146,7 @@
val subproofs = List.revAppend (nontriv_subs, subs)
val step = Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meths))
in
- set_preplay_outcomes_of_isar_step ctxt time preplay_data step
- [(meth, Lazy.value (Played time))];
+ set_preplay_outcomes_of_isar_step ctxt time preplay_data step [(meth, Played time)];
step
end
else
@@ -169,7 +168,7 @@
(* check if the modified step can be preplayed fast enough *)
val timeout = slackify_merge_timeout (Time.+ (time, time'))
- val Played time'' = preplay_isar_step ctxt timeout (hd meths)(*FIXME*) step''
+ val outcomes as (_, Played time'') :: _ = preplay_isar_step ctxt timeout step''
in
decrement_step_count (); (* l' successfully eliminated! *)
map (replace_successor l' [l]) lfs';
@@ -221,7 +220,6 @@
val ((cand as Prove (_, _, _, _, _, ((lfs, _), _))) :: steps') = drop i steps
val succs = collect_successors steps' labels
- val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
(* only touch steps that can be preplayed successfully *)
val Played time = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l
@@ -233,23 +231,18 @@
val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
val timeouts = map (curry Time.+ time_slice #> slackify_merge_timeout) times0
- (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
- val play_outcomes = map3 (preplay_isar_step ctxt) timeouts succ_meths succs'
+ val meths_outcomess = map2 (preplay_isar_step ctxt) timeouts succs'
(* ensure none of the modified successors timed out *)
- val times = map (fn Played time => time) play_outcomes
+ val times = map (fn (_, Played time) :: _ => time) meths_outcomess
val (steps1, _ :: steps2) = chop i steps
(* replace successors with their modified versions *)
val steps2 = update_steps steps2 succs'
-
- val succ_meths_outcomess =
- map2 (fn meth => fn outcome => [(meth, Lazy.value outcome)]) succ_meths
- play_outcomes
in
decrement_step_count (); (* candidate successfully eliminated *)
map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times
- succs' succ_meths_outcomess;
+ succs' meths_outcomess;
map (replace_successor l labels) 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_isar_minimize.ML Mon Feb 03 10:19:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 11:30:53 2014 +0100
@@ -41,7 +41,7 @@
fun minimize_facts _ time min_facts [] = (time, min_facts)
| minimize_facts mk_step time min_facts (f :: facts) =
- (case preplay_isar_step ctxt (Time.+ (time, slack)) meth
+ (case preplay_isar_step_for_method ctxt (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)
@@ -51,8 +51,7 @@
val step' = mk_step_lfs_gfs min_lfs min_gfs
in
- set_preplay_outcomes_of_isar_step ctxt time preplay_data step'
- [(meth, Lazy.value (Played time))];
+ set_preplay_outcomes_of_isar_step ctxt time preplay_data step' [(meth, Played time)];
step'
end
| _ => step (* don't touch steps that time out or fail *))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 10:19:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 11:30:53 2014 +0100
@@ -18,10 +18,12 @@
type isar_preplay_data
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
- val preplay_isar_step : Proof.context -> Time.time -> proof_method -> isar_step -> play_outcome
+ val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step ->
+ play_outcome
+ val preplay_isar_step : Proof.context -> Time.time -> isar_step ->
+ (proof_method * play_outcome) list
val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
- isar_preplay_data Unsynchronized.ref -> isar_step ->
- (proof_method * play_outcome Lazy.lazy) list -> unit
+ isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit
val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method ->
play_outcome Lazy.lazy
@@ -120,7 +122,8 @@
| _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step ctxt timeout meth (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
+fun raw_preplay_step_for_method ctxt timeout meth
+ (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
let
val goal =
(case xs of
@@ -156,8 +159,20 @@
play_outcome)
end
-fun preplay_isar_step ctxt timeout meth =
- try (raw_preplay_step ctxt timeout meth) #> the_default Play_Failed
+fun preplay_isar_step_for_method ctxt timeout meth =
+ try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed
+
+fun preplay_isar_step ctxt timeout step =
+ let
+ fun try_method meth =
+ (case preplay_isar_step_for_method ctxt timeout meth step of
+ outcome as Played _ => SOME (meth, outcome)
+ | _ => NONE)
+
+ val meths = snd (byline_of_isar_step step)
+ in
+ the_list (Par_List.get_some try_method meths)
+ end
type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table
@@ -173,9 +188,11 @@
fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
(step as Prove (_, _, l, _, _, (_, meths))) meths_outcomes0 =
let
- fun preplay meth = Lazy.lazy (fn () => preplay_isar_step ctxt timeout meth step)
- val meths_outcomes =
- fold (fn meth => AList.default (op =) (meth, preplay meth)) meths meths_outcomes0
+ fun lazy_preplay meth =
+ Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
+ val meths_outcomes = meths_outcomes0
+ |> map (apsnd Lazy.value)
+ |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
in
preplay_data := Canonical_Label_Tab.map_default (l, [])
(fold (AList.update (op =)) meths_outcomes) (!preplay_data)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 10:19:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 11:30:53 2014 +0100
@@ -43,7 +43,7 @@
val steps_of_isar_proof : isar_proof -> isar_step list
val label_of_isar_step : isar_step -> label option
- val byline_of_isar_step : isar_step -> (facts * proof_method list) option
+ val byline_of_isar_step : isar_step -> facts * proof_method list
val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
@@ -127,8 +127,8 @@
fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
| subproofs_of_isar_step _ = NONE
-fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = SOME byline
- | byline_of_isar_step _ = NONE
+fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = byline
+ | byline_of_isar_step _ = (([], []), [])
fun fold_isar_step f step =
fold (steps_of_isar_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
@@ -169,7 +169,7 @@
fun kill_useless_labels_in_isar_proof proof =
let
val used_ls =
- fold_isar_steps (byline_of_isar_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
+ fold_isar_steps (byline_of_isar_step #> (fn ((ls, _), _) => union (op =) ls | _ => I))
(steps_of_isar_proof proof) []
fun kill_label l = if member (op =) used_ls l then l else no_label