generalized preplaying infrastructure to store various results for various methods
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 19:16:41 2014 +0100
@@ -277,11 +277,15 @@
|> postprocess_isar_proof_remove_unreferenced_steps I
|> relabel_isar_proof_canonically
- val preplay_data as {string_of_preplay_outcome, overall_preplay_outcome, ...} =
+ val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
preplay_timeout isar_proof
- fun str_of_meth l meth = string_of_proof_method meth ^ " " ^ string_of_preplay_outcome l
+ fun str_of_preplay_outcome outcome =
+ if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
+
+ fun str_of_meth l meth =
+ string_of_proof_method meth ^ " " ^ str_of_preplay_outcome (preplay_outcome l meth)
fun comment_of l = map (map (str_of_meth l)) #> map commas #> space_implode "; "
fun trace_isar_proof label proof =
--- 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jan 31 19:16:41 2014 +0100
@@ -27,11 +27,11 @@
fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
| minimize_isar_step_dependencies {preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
- (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
- (case preplay_outcome l of
+ (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss as (meth :: _) :: _))) =
+ (case Lazy.force (preplay_outcome l meth) of
Played time =>
let
- fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
+ fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))
val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
fun minimize_facts _ time min_facts [] = (time, min_facts)
@@ -43,7 +43,7 @@
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_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs
+ set_preplay_outcome l meth (Played time); mk_step_lfs_gfs min_lfs min_gfs
end
| _ => step (* don't touch steps that time out or fail *))
@@ -62,7 +62,7 @@
fold_rev do_step steps (refed, [concl])
end
and do_step step (refed, accu) =
- (case label_of_step step of
+ (case label_of_isar_step step of
NONE => (refed, step :: accu)
| SOME l =>
if Ord_List.member label_ord refed l then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 19:16:41 2014 +0100
@@ -8,6 +8,7 @@
signature SLEDGEHAMMER_ISAR_PREPLAY =
sig
type play_outcome = Sledgehammer_Reconstructor.play_outcome
+ type proof_method = Sledgehammer_Isar_Proof.proof_method
type isar_step = Sledgehammer_Isar_Proof.isar_step
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
type label = Sledgehammer_Isar_Proof.label
@@ -15,9 +16,8 @@
val trace : bool Config.T
type isar_preplay_data =
- {preplay_outcome: label -> play_outcome,
- set_preplay_outcome: label -> play_outcome -> unit,
- string_of_preplay_outcome: label -> string,
+ {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+ set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
preplay_quietly: Time.time -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
@@ -106,9 +106,8 @@
| _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
-fun preplay_raw _ _ _ _ _ (Let _) = Played Time.zeroTime
- | preplay_raw debug type_enc lam_trans ctxt timeout
- (Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) =
+fun preplay_raw debug type_enc lam_trans ctxt timeout meth
+ (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
let
val goal =
(case xs of
@@ -147,9 +146,8 @@
end
type isar_preplay_data =
- {preplay_outcome: label -> play_outcome,
- set_preplay_outcome: label -> play_outcome -> unit,
- string_of_preplay_outcome: label -> string,
+ {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+ set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
preplay_quietly: Time.time -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
@@ -188,17 +186,16 @@
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 *)
- {preplay_outcome = K (Played Time.zeroTime),
- set_preplay_outcome = K (K ()),
- string_of_preplay_outcome = K "",
+ {preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
+ set_preplay_outcome = K (K (K ())),
preplay_quietly = K (K (Played Time.zeroTime)),
overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
else
let
val ctxt = enrich_context_with_local_facts proof ctxt
- fun preplay quietly timeout step =
- preplay_raw debug type_enc lam_trans ctxt timeout step
+ 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
@@ -210,43 +207,42 @@
Play_Failed)
(* preplay steps treating exceptions like timeouts *)
- fun preplay_quietly timeout = preplay true timeout
+ fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, (meth :: _) :: _))) =
+ preplay true timeout meth step
+ | preplay_quietly _ _ = Played Time.zeroTime
+
+ fun add_step_to_tab (step as Prove (_, _, l, _, _, (_, methss))) =
+ Canonical_Label_Tab.update_new
+ (l, maps (map (fn meth =>
+ (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
+ | add_step_to_tab _ = I
val preplay_tab =
- let
- fun add_step_to_tab step tab =
- (case label_of_step step of
- NONE => tab
- | SOME l =>
- Canonical_Label_Tab.update_new
- (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab)
- handle Canonical_Label_Tab.DUP _ =>
- raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
- in
- Canonical_Label_Tab.empty
- |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
- |> Unsynchronized.ref
- end
+ Canonical_Label_Tab.empty
+ |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
+ |> Unsynchronized.ref
- fun preplay_outcome l =
- Canonical_Label_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
- handle Option.Option => raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
+ fun preplay_outcome l meth =
+ (case Canonical_Label_Tab.lookup (!preplay_tab) l of
+ SOME meths_outcomes =>
+ (case AList.lookup (op =) meths_outcomes meth of
+ SOME outcome => outcome
+ | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
+ | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
- fun set_preplay_outcome l result =
- preplay_tab := Canonical_Label_Tab.update (l, Lazy.value result) (!preplay_tab)
+ 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 string_of_preplay_outcome l = @{make_string} (preplay_outcome l)
-
- val result_of_step =
- try (label_of_step #> the #> preplay_outcome)
- #> the_default (Played Time.zeroTime)
+ 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)
in
{preplay_outcome = preplay_outcome,
set_preplay_outcome = set_preplay_outcome,
- string_of_preplay_outcome = string_of_preplay_outcome,
preplay_quietly = preplay_quietly,
overall_preplay_outcome = overall_preplay_outcome}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 19:16:41 2014 +0100
@@ -34,8 +34,8 @@
val steps_of_proof : isar_proof -> isar_step list
- val label_of_step : isar_step -> label option
- val byline_of_step : isar_step -> (facts * proof_method list list) option
+ val label_of_isar_step : isar_step -> label option
+ val byline_of_isar_step : isar_step -> (facts * proof_method list list) option
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
@@ -103,17 +103,17 @@
fun steps_of_proof (Proof (_, _, steps)) = steps
-fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l
- | label_of_step _ = NONE
+fun label_of_isar_step (Prove (_, _, l, _, _, _)) = SOME l
+ | label_of_isar_step _ = NONE
-fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
- | subproofs_of_step _ = NONE
+fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
+ | subproofs_of_isar_step _ = NONE
-fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
- | byline_of_step _ = NONE
+fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = SOME byline
+ | byline_of_isar_step _ = NONE
fun fold_isar_step f step =
- fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step)) #> f step
+ fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
and fold_isar_steps f = fold (fold_isar_step f)
fun map_isar_steps f =
@@ -143,15 +143,15 @@
| chain_isar_step _ step = step
and chain_isar_steps _ [] = []
| chain_isar_steps (prev as SOME _) (i :: is) =
- chain_isar_step prev i :: chain_isar_steps (label_of_step i) is
- | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_step i) is
+ chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
+ | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_isar_step i) is
and chain_isar_proof (Proof (fix, assms, steps)) =
Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
fun kill_useless_labels_in_isar_proof proof =
let
val used_ls =
- fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
+ fold_isar_steps (byline_of_isar_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
(steps_of_proof proof) []
fun kill_label l = if member (op =) used_ls l then l else no_label
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 19:16:41 2014 +0100
@@ -31,10 +31,10 @@
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
- (step as Prove (_, _, l, _, _, _)) =
+ (step as Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
let
val timeout =
- (case preplay_outcome l of
+ (case Lazy.force (preplay_outcome l meth) of
Played time => Time.+ (time, slack)
| _ => preplay_timeout)
@@ -44,7 +44,8 @@
| _ => NONE)
in
(case Par_List.get_some try_variant (variants_of_step step) of
- SOME (step', result) => (set_preplay_outcome l result; step')
+ SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
+ (set_preplay_outcome l meth' result; step')
| NONE => step)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jan 31 19:16:41 2014 +0100
@@ -8,6 +8,7 @@
sig
val sledgehammerN : string
val log2 : real -> real
+ val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
val app_hd : ('a -> 'a) -> 'a list -> 'a list
val n_fold_cartesian_product : 'a list list -> 'a list list
val plural_s : int -> string
@@ -38,6 +39,8 @@
val log10_2 = Math.log10 2.0
fun log2 n = Math.log10 n / log10_2
+fun map3 xs = Ctr_Sugar_Util.map3 xs
+
fun app_hd f (x :: xs) = f x :: xs
fun cartesian_product [] _ = []