# HG changeset patch # User blanchet # Date 1391418858 -3600 # Node ID d9d31354834e286c117575b3264d654f49a0846e # Parent bd9f033b9896073d397484886390f9f20297aba3 centralize more preplaying diff -r bd9f033b9896 -r d9d31354834e src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 10:14:18 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 10:14:18 2014 +0100 @@ -296,7 +296,7 @@ fun str_of_meth l meth = string_of_proof_method meth ^ " " ^ - str_of_preplay_outcome (preplay_outcome_of_isar_step (!preplay_data) l meth) + str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) fun comment_of l = map (str_of_meth l) #> commas fun trace_isar_proof label proof = @@ -314,7 +314,8 @@ |> try0_isar ? try0_isar_proof ctxt preplay_timeout preplay_data |> tap (trace_isar_proof "Tried0") |> postprocess_isar_proof_remove_unreferenced_steps - (try0_isar ? minimize_isar_step_dependencies ctxt preplay_data) + (keep_fastest_method_of_isar_step (!preplay_data) + #> try0_isar(*### minimize*) ? minimize_isar_step_dependencies ctxt preplay_data) |> tap (trace_isar_proof "Minimized") |> `(preplay_outcome_of_isar_proof (!preplay_data)) ||> chain_isar_proof diff -r bd9f033b9896 -r d9d31354834e src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 10:14:18 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 10:14:18 2014 +0100 @@ -156,7 +156,8 @@ try the_single sub_steps (* only touch proofs that can be preplayed sucessfully *) - val Played time' = Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l' meth') + val Played time' = + Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l' meth') (* merge steps *) val subs'' = subs @ nontriv_subs @@ -183,7 +184,7 @@ if subproofs = [] then step else - (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of + (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs [] | _ => step) @@ -223,12 +224,13 @@ 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 = Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) + val Played time = + Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) val succs' = map (try_merge cand #> the) succs val times0 = map2 ((fn Played time => time) o Lazy.force oo - preplay_outcome_of_isar_step (!preplay_data)) labels succ_meths + preplay_outcome_of_isar_step_for_method (!preplay_data)) labels succ_meths val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time val timeouts = map (curry Time.+ time_slice #> time_mult merge_timeout_slack) times0 diff -r bd9f033b9896 -r d9d31354834e src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 10:14:18 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 10:14:18 2014 +0100 @@ -11,6 +11,7 @@ type isar_proof = Sledgehammer_Isar_Proof.isar_proof type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data + val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref -> isar_step -> isar_step val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> @@ -24,12 +25,16 @@ open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay +fun keep_fastest_method_of_isar_step preplay_data + (Prove (qs, xs, l, t, subproofs, (facts, _))) = + Prove (qs, xs, l, t, subproofs, (facts, [fastest_method_of_isar_step preplay_data l])) + | keep_fastest_method_of_isar_step _ step = step + val slack = seconds 0.1 -fun minimize_isar_step_dependencies _ _ (step as Let _) = step - | minimize_isar_step_dependencies ctxt preplay_data +fun minimize_isar_step_dependencies ctxt preplay_data (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) = - (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of + (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of Played time => let fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths)) @@ -51,6 +56,7 @@ step' end | _ => step (* don't touch steps that time out or fail *)) + | minimize_isar_step_dependencies _ _ step = step fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = let diff -r bd9f033b9896 -r d9d31354834e src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 10:14:18 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 10:14:18 2014 +0100 @@ -22,8 +22,9 @@ 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 - val preplay_outcome_of_isar_step : isar_preplay_data -> label -> proof_method -> + val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method -> play_outcome Lazy.lazy + val fastest_method_of_isar_step : isar_preplay_data -> label -> proof_method val preplay_outcome_of_isar_proof : isar_preplay_data -> isar_proof -> play_outcome end; @@ -180,16 +181,20 @@ end | set_preplay_outcomes_of_isar_step _ _ _ _ _ = () -fun preplay_outcome_of_isar_step preplay_data l meth = - (case Canonical_Label_Tab.lookup preplay_data 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 preplay_outcome_of_isar_step_for_method preplay_data l meth = + let val SOME meths_outcomes = Canonical_Label_Tab.lookup preplay_data l in + the (AList.lookup (op =) meths_outcomes meth) + end -fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meth :: _))) = - Lazy.force (preplay_outcome_of_isar_step preplay_data l meth) +fun fastest_method_of_isar_step preplay_data l = + the (Canonical_Label_Tab.lookup preplay_data l) + |> map (fn (meth, outcome) => + (meth, Time.toMilliseconds (case Lazy.force outcome of Played time => time | _ => one_year))) + |> sort (int_ord o pairself snd) + |> hd |> fst + +fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meths))) = + Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths)) | forced_outcome_of_step _ _ = Played Time.zeroTime fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) = diff -r bd9f033b9896 -r d9d31354834e src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Mon Feb 03 10:14:18 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Mon Feb 03 10:14:18 2014 +0100 @@ -33,7 +33,7 @@ (step as Prove (_, _, l, _, _, (_, meths as meth :: _))) = let val timeout = - (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of + (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of Played time => Time.+ (time, slack) | _ => preplay_timeout)