--- 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_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
+ ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data) proof =
if compress_isar <= 1.0 then
proof
else
@@ -137,9 +137,10 @@
end
(* elimination of trivial, one-step subproofs *)
- fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs =
+ fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: meths') subs nontriv_subs =
if null subs orelse not (compress_further ()) then
- (set_preplay_outcome l meth (Played time);
+ (set_preplay_outcomes l ((meth, Lazy.value (Played time)) ::
+ map (rpair (Lazy.value Not_Played)(*FIXME*)) meths');
Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meths)))
else
(case subs of
@@ -215,7 +216,8 @@
val ((cand as Prove (_, _, l, _, _, ((lfs, _), meth :: _))) :: steps') = drop i steps
val succs = collect_successors steps' succ_lbls
- val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
+ val succ_methss = map (snd o the o byline_of_isar_step) succs
+ val succ_meths = map hd succ_methss (* FIXME *)
(* only touch steps that can be preplayed successfully *)
val Played time = Lazy.force (preplay_outcome l meth)
@@ -244,9 +246,13 @@
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 :: meths => fn outcome => (meth, Lazy.value outcome) ::
+ map (rpair (Lazy.value Not_Played)(*FIXME*)) meths) succ_methss play_outcomes
in
decrement_step_count (); (* candidate successfully eliminated *)
- map3 set_preplay_outcome succ_lbls succ_meths play_outcomes;
+ map2 set_preplay_outcomes succ_lbls succ_meths_outcomess;
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_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,8 +26,7 @@
val slack = seconds 0.1
fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
- | minimize_isar_step_dependencies
- {reset_preplay_outcomes, set_preplay_outcome, preplay_outcome, preplay_quietly, ...}
+ | minimize_isar_step_dependencies {set_preplay_outcomes, preplay_outcome, preplay_quietly, ...}
(step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
(case Lazy.force (preplay_outcome l meth) of
Played time =>
@@ -43,12 +42,9 @@
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
-
- val step' = mk_step_lfs_gfs min_lfs min_gfs
in
- reset_preplay_outcomes step';
- set_preplay_outcome l meth (Played time);
- step'
+ set_preplay_outcomes l [(meth, Lazy.value (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_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,8 +16,7 @@
val trace : bool Config.T
type isar_preplay_data =
- {reset_preplay_outcomes: isar_step -> unit,
- set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
+ {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}
@@ -136,8 +135,7 @@
end
type isar_preplay_data =
- {reset_preplay_outcomes: isar_step -> unit,
- set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
+ {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}
@@ -177,8 +175,7 @@
fun preplay_data_of_isar_proof 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 *)
- {reset_preplay_outcomes = K (),
- set_preplay_outcome = K (K (K ())),
+ {set_preplay_outcomes = K (K ()),
preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
preplay_quietly = K (K (Played Time.zeroTime)),
overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
@@ -205,15 +202,9 @@
val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
- 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)
- (!preplay_tab)
- | reset_preplay_outcomes _ = ()
-
- fun set_preplay_outcome l meth result =
- preplay_tab := Canonical_Label_Tab.map_entry l
- (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
+ fun set_preplay_outcomes l meths_outcomes =
+ preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes)
+ (!preplay_tab)
fun preplay_outcome l meth =
(case Canonical_Label_Tab.lookup (!preplay_tab) l of
@@ -223,17 +214,22 @@
| NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
| NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
- val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
-
fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) =
Lazy.force (preplay_outcome l meth)
| result_of_step _ = Played Time.zeroTime
fun overall_preplay_outcome (Proof (_, _, steps)) =
fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
+
+ 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)
+ (!preplay_tab)
+ | reset_preplay_outcomes _ = ()
+
+ val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
in
- {reset_preplay_outcomes = reset_preplay_outcomes,
- set_preplay_outcome = set_preplay_outcome,
+ {set_preplay_outcomes = set_preplay_outcomes,
preplay_outcome = preplay_outcome,
preplay_quietly = preplay_quietly,
overall_preplay_outcome = overall_preplay_outcome}
--- 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
@@ -30,7 +30,7 @@
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
- ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
+ ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data)
(step as Prove (_, _, l, _, _, (_, meth :: _))) =
let
val timeout =
@@ -45,8 +45,8 @@
in
(* FIXME: create variant after success *)
(case Par_List.get_some try_variant (variants_of_step step) of
- SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), result) =>
- (set_preplay_outcome l meth' result; step')
+ SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), outcome) =>
+ (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step')
| NONE => step)
end