--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Jan 31 19:16:41 2014 +0100
@@ -79,14 +79,15 @@
| _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
end
-(* Tries merging the first step into the second step. Arbitrarily picks the second step's method. *)
+(* Tries merging the first step into the second step.
+ FIXME: Arbitrarily picks the second step's method. *)
fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
- (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
+ (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), methss2))) =
let
val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
val gfs = union (op =) gfs1 gfs2
in
- SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth2)))
+ SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), methss2)))
end
| try_merge _ _ = NONE
@@ -136,57 +137,55 @@
(** elimination of trivial, one-step subproofs **)
- fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
+ fun elim_subproofs' time qs fix l t lfs gfs (methss as (meth :: _) :: _) subs nontriv_subs =
if null subs orelse not (compress_further ()) then
- (set_preplay_outcome l (Played time);
- Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
+ (set_preplay_outcome l meth (Played time);
+ Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), methss)))
else
(case subs of
(sub as Proof (_, assms, sub_steps)) :: subs =>
(let
- (* trivial subproofs have exactly one Prove step *)
- val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
+ (* trivial subproofs have exactly one "Prove" step *)
+ val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), (meth' :: _) :: _))) =
+ try the_single sub_steps
(* only touch proofs that can be preplayed sucessfully *)
- val Played time' = preplay_outcome l'
+ val Played time' = Lazy.force (preplay_outcome l' meth')
(* merge steps *)
val subs'' = subs @ nontriv_subs
- val lfs'' =
- subtract (op =) (map fst assms) lfs'
- |> union (op =) lfs
+ val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
val gfs'' = union (op =) gfs' gfs
- val by = ((lfs'', gfs''), meth)
+ val by = ((lfs'', gfs''), methss(*FIXME*))
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''
-
in
decrement_step_count (); (* l' successfully eliminated! *)
map (replace_successor l' [l]) lfs';
- elim_subproofs' time'' qs fix l t lfs'' gfs'' meth subs nontriv_subs
+ elim_subproofs' time'' qs fix l t lfs'' gfs'' methss subs nontriv_subs
end
handle Bind =>
- elim_subproofs' time qs fix l t lfs gfs meth subs (sub :: nontriv_subs))
+ elim_subproofs' time qs fix l t lfs gfs methss subs (sub :: nontriv_subs))
| _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
fun elim_subproofs (step as Let _) = step
- | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
+ | elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
+ ((lfs, gfs), methss as (meth :: _) :: _))) =
if subproofs = [] then
step
else
- (case preplay_outcome l of
- Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+ (case Lazy.force (preplay_outcome l meth) of
+ Played time => elim_subproofs' time qs fix l t lfs gfs methss subproofs []
| _ => step)
(** top_level compression: eliminate steps by merging them into their successors **)
-
fun compress_top_level steps =
let
(* (#successors, (size_of_term t, position)) *)
- fun cand_key (i, l, t_size) = (get_successors l |> length, (t_size, i))
+ fun cand_key (i, l, t_size) = (length (get_successors l), (t_size, i))
val compression_ord =
prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
@@ -207,32 +206,36 @@
| add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
in
(steps
- |> split_last |> fst (* keep last step *)
- |> fold_index add_cand) []
+ |> split_last |> fst (* keep last step *)
+ |> fold_index add_cand) []
end
fun try_eliminate (i, l, _) succ_lbls steps =
let
+ val ((cand as Prove (_, _, l, _, _, ((lfs, _), (meth :: _) :: _))) :: steps') =
+ drop i steps
+
+ val succs = collect_successors steps' succ_lbls
+ val succ_meths = map (hd o hd o snd o the o byline_of_isar_step) succs
+
(* only touch steps that can be preplayed successfully *)
- val Played time = preplay_outcome l
+ val Played time = Lazy.force (preplay_outcome l meth)
- val succ_times = map (preplay_outcome #> (fn Played t => t)) succ_lbls
+ val succs' = map (try_merge cand #> the) succs
+
+ val succ_times =
+ map2 ((fn Played t => t) o Lazy.force oo preplay_outcome) succ_lbls succ_meths
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
- val ((cand as Prove (_, _, l, _, _, ((lfs, _), _))) :: steps') = drop i steps
-
(* FIXME: debugging *)
val _ =
- if the (label_of_step cand) <> l then
+ if the (label_of_isar_step cand) <> l then
raise Fail "Sledgehammer_Isar_Compress: try_eliminate"
else
()
- val succs = collect_successors steps' succ_lbls
- val succs' = map (try_merge cand #> the) succs
-
(* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
val play_outcomes = map2 preplay_quietly timeouts succs'
@@ -244,7 +247,7 @@
val steps2 = update_steps steps2 succs'
in
decrement_step_count (); (* candidate successfully eliminated *)
- map2 set_preplay_outcome succ_lbls play_outcomes;
+ map3 set_preplay_outcome succ_lbls succ_meths 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