# HG changeset patch # User blanchet # Date 1387474794 -3600 # Node ID 14e2c7616209c774143313dc3948d551e769a045 # Parent 79745ba60a5a53f97a38d19026c14191a901bece more data structure refactoring diff -r 79745ba60a5a -r 14e2c7616209 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 18:22:31 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 18:39:54 2013 +0100 @@ -158,7 +158,7 @@ (* check if the modified step can be preplayed fast enough *) val timeout = time_mult merge_timeout_slack (Time.+(time, time')) - val (false, time'') = preplay_quietly timeout step'' + val Preplay_Success (false, time'') = preplay_quietly timeout step'' in decrement_step_count (); (* l' successfully eliminated! *) @@ -232,17 +232,17 @@ val succs' = map (try_merge cand #> the) succs (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *) - val preplay_times = map2 preplay_quietly timeouts succs' + val preplay_results = map2 preplay_quietly timeouts succs' (* ensure none of the modified successors timed out *) - val false = List.exists fst preplay_times + val true = List.all (fn Preplay_Success _ => true) preplay_results val (steps1, _ :: steps2) = chop i steps (* replace successors with their modified versions *) val steps2 = update_steps steps2 succs' in decrement_step_count (); (* candidate successfully eliminated *) - map2 (fn l => set_preplay_result l o Preplay_Success) succ_lbls preplay_times; + map2 set_preplay_result succ_lbls preplay_results; 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 79745ba60a5a -r 14e2c7616209 src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Thu Dec 19 18:22:31 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Thu Dec 19 18:39:54 2013 +0100 @@ -36,8 +36,8 @@ fun minimize_facts _ time min_facts [] = (time, min_facts) | minimize_facts mk_step time min_facts (f :: facts) = (case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of - (true, _) => minimize_facts mk_step time (f :: min_facts) facts - | (false, time) => minimize_facts mk_step time min_facts facts) + Preplay_Success (false, time) => minimize_facts mk_step time min_facts facts + | _ => minimize_facts mk_step time (f :: min_facts) facts) 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 diff -r 79745ba60a5a -r 14e2c7616209 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Dec 19 18:22:31 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Dec 19 18:39:54 2013 +0100 @@ -16,14 +16,12 @@ Preplay_Failure val trace: bool Config.T - val add_preplay_time: bool * Time.time -> bool * Time.time -> bool * Time.time type preplay_interface = {get_preplay_result: label -> preplay_result, set_preplay_result: label -> preplay_result -> unit, - preplay_quietly: Time.time -> isar_step -> bool * Time.time, - (* the returned flag signals a preplay failure *) - overall_preplay_stats: isar_proof -> (bool * Time.time) * bool} + preplay_quietly: Time.time -> isar_step -> preplay_result, + overall_preplay_stats: isar_proof -> preplay_result} val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time -> isar_proof -> preplay_interface @@ -44,8 +42,6 @@ val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *) -fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+ (t1, t2)) - fun preplay_trace ctxt assms concl time = let val ctxt = ctxt |> Config.put show_markup true @@ -163,9 +159,8 @@ type preplay_interface = {get_preplay_result: label -> preplay_result, set_preplay_result: label -> preplay_result -> unit, - preplay_quietly: Time.time -> isar_step -> bool * Time.time, - (* the returned flag signals a preplay failure *) - overall_preplay_stats: isar_proof -> (bool * Time.time) * bool} + preplay_quietly: Time.time -> isar_step -> preplay_result, + overall_preplay_stats: isar_proof -> preplay_result} fun enrich_context_with_local_facts proof ctxt = let @@ -185,6 +180,10 @@ enrich_with_proof proof ctxt end +fun merge_preplay_results (Preplay_Success (b1, t1)) (Preplay_Success (b2, t2)) = + Preplay_Success (b1 orelse b2, Time.+ (t1, t2)) + | merge_preplay_results _ _ = Preplay_Failure + (* Given a proof, produces an imperative preplay interface with a shared table mapping from labels to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated calculation. @@ -196,8 +195,8 @@ (* the dont_preplay option pretends that everything works just fine *) {get_preplay_result = K (Preplay_Success zero_preplay_time), set_preplay_result = K (K ()), - preplay_quietly = K (K zero_preplay_time), - overall_preplay_stats = K (zero_preplay_time, false)} : preplay_interface + preplay_quietly = K (K (Preplay_Success zero_preplay_time)), + overall_preplay_stats = K (Preplay_Success zero_preplay_time)} : preplay_interface else let val ctxt = enrich_context_with_local_facts proof ctxt @@ -216,10 +215,7 @@ Preplay_Failure) (* preplay steps treating exceptions like timeouts *) - fun preplay_quietly timeout step = - (case preplay true timeout step of - Preplay_Success preplay_time => preplay_time - | Preplay_Failure => (true, timeout)) + fun preplay_quietly timeout = preplay true timeout val preplay_tab = let @@ -247,13 +243,9 @@ try (label_of_step #> the #> get_preplay_result) #> the_default (Preplay_Success zero_preplay_time) - fun do_step step = - (case result_of_step step of - Preplay_Success preplay_time => apfst (add_preplay_time preplay_time) - | Preplay_Failure => apsnd (K true)) - fun overall_preplay_stats (Proof (_, _, steps)) = - fold_isar_steps do_step steps (zero_preplay_time, false) + Preplay_Success (false, Time.zeroTime) + |> fold_isar_steps (merge_preplay_results o result_of_step) steps in {get_preplay_result = get_preplay_result, set_preplay_result = set_preplay_result, diff -r 79745ba60a5a -r 14e2c7616209 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 18:22:31 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 18:39:54 2013 +0100 @@ -355,7 +355,7 @@ |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay preplay_timeout) - val ((preplay_time, preplay_fail), isar_proof) = + val (preplay_result, isar_proof) = isar_proof |> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0) preplay_interface @@ -383,7 +383,9 @@ else []) @ (if do_preplay then - [(if preplay_fail then "may fail, " else "") ^ string_of_ext_time preplay_time] + [(case preplay_result of + Preplay_Success ext_time => string_of_ext_time ext_time + | Preplay_Failure => "may fail")] else []) in diff -r 79745ba60a5a -r 14e2c7616209 src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Thu Dec 19 18:22:31 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Thu Dec 19 18:39:54 2013 +0100 @@ -29,7 +29,7 @@ fun try0_step _ _ (step as Let _) = step | try0_step preplay_timeout - ({preplay_quietly, get_preplay_result, set_preplay_result, ...} : preplay_interface) + ({get_preplay_result, set_preplay_result, preplay_quietly, ...} : preplay_interface) (step as Prove (_, _, l, _, _, _)) = let val timeout = @@ -39,11 +39,11 @@ fun try_variant variant = (case preplay_quietly timeout variant of - (true, _) => NONE - | time as (false, _) => SOME (variant, time)) + result as Preplay_Success _ => SOME (variant, result) + | _ => NONE) in (case Par_List.get_some try_variant (variants_of_step step) of - SOME (step, time) => (set_preplay_result l (Preplay_Success time); step) + SOME (step', result) => (set_preplay_result l result; step') | NONE => step) end