# HG changeset patch # User blanchet # Date 1391192201 -3600 # Node ID 3c593bad6b3116583f6b8106b1521350ce2953d4 # Parent a4ef6eb1fc20fa603dcb8ac9b843249dfa9b9e46 generalized preplaying infrastructure to store various results for various methods diff -r a4ef6eb1fc20 -r 3c593bad6b31 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 = diff -r a4ef6eb1fc20 -r 3c593bad6b31 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- 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 diff -r a4ef6eb1fc20 -r 3c593bad6b31 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- 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 diff -r a4ef6eb1fc20 -r 3c593bad6b31 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- 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 diff -r a4ef6eb1fc20 -r 3c593bad6b31 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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 diff -r a4ef6eb1fc20 -r 3c593bad6b31 src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML --- 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 diff -r a4ef6eb1fc20 -r 3c593bad6b31 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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 [] _ = []