# HG changeset patch # User blanchet # Date 1391595756 -3600 # Node ID 803a7400cc58e861491a0421f802930b9939acbf # Parent c7561e87cba7bcf74a24c90916ceff3af116f98b tuned code to avoid noncanonical (and risky) exception handling diff -r c7561e87cba7 -r 803a7400cc58 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Feb 05 09:25:48 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Feb 05 11:22:36 2014 +0100 @@ -42,7 +42,7 @@ rev (snd (collect_steps steps (lbls, []))) end -fun update_steps steps updates = +fun update_steps updates steps = let fun update_steps [] updates = ([], updates) | update_steps steps [] = (steps, []) @@ -87,17 +87,16 @@ (hopeful @ hopeless, hopeless) end -fun try_merge_steps preplay_data (Prove ([], fix1, l1, _, subproofs1, (lfs1, gfs1), meths1, comment1)) +fun merge_steps preplay_data (Prove ([], fix1, l1, _, subproofs1, (lfs1, gfs1), meths1, comment1)) (Prove (qs2, fix2, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) = - let - val (meths, hopeless) = merge_methods preplay_data (l1, meths1) (l2, meths2) - val lfs = union (op =) lfs1 (remove (op =) l1 lfs2) - val gfs = union (op =) gfs1 gfs2 - in - SOME (Prove (qs2, union (op =) fix1 fix2, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths, - comment1 ^ comment2), hopeless) - end - | try_merge_steps _ _ _ = NONE + let + val (meths, hopeless) = merge_methods preplay_data (l1, meths1) (l2, meths2) + val lfs = union (op =) lfs1 (remove (op =) l1 lfs2) + val gfs = union (op =) gfs1 gfs2 + in + (Prove (qs2, union (op =) fix1 fix2, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths, + comment1 ^ comment2), hopeless) + end val merge_slack_time = seconds 0.005 val merge_slack_factor = 1.5 @@ -176,7 +175,8 @@ val meths_outcomes as (_, Played time'') :: _ = preplay_isar_step ctxt timeout hopeless step'' in - decrement_step_count (); (* l' successfully eliminated! *) + (* l' successfully eliminated *) + decrement_step_count (); set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes; map (replace_successor l' [l]) lfs'; elim_one_subproof time'' step'' subs nontriv_subs @@ -200,45 +200,38 @@ fold (fn x => fn y => if cand_ord (x, y) = LESS then x else y) cands' cand |> (fn best => (SOME best, remove (op =) best cands)) - fun try_eliminate (l, _) labels steps = + fun try_eliminate i l labels steps = let val (steps_before, (cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps_after) = - chop (find_index (curry (op =) (SOME l) o label_of_isar_step) steps) steps - - val time = - (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of - Played time => time - | _ => preplay_timeout) - + chop i steps val succs = collect_successors steps_after labels - val (succs', hopelesses) = - map (try_merge_steps (!preplay_data) cand #> the) succs - |> split_list - - val times0 = map ((fn Played time => time) o - forced_intermediate_preplay_outcome_of_isar_step (!preplay_data)) labels - val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time - val timeouts = - map (curry Time.+ time_slice #> adjust_merge_timeout preplay_timeout) times0 - (* FIXME: "preplay_timeout" should be an ultimate maximum *) - - val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs' - - (* ensure none of the modified successors timed out *) - val times = map (fn (_, Played time) :: _ => time) meths_outcomess - - (* replace successors with their modified versions *) - val steps_after' = update_steps steps_after succs' + val (succs', hopelesses) = split_list (map (merge_steps (!preplay_data) cand) succs) in - decrement_step_count (); (* candidate successfully eliminated *) - map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times - succs' meths_outcomess; - map (replace_successor l labels) lfs; - steps_before @ steps_after' + (case try (map ((fn Played time => time) o + forced_intermediate_preplay_outcome_of_isar_step (!preplay_data))) labels of + NONE => steps + | SOME times0 => + let + val full_time = + (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of + Played time => time + | _ => preplay_timeout) + val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) full_time + val timeouts = + map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0 + val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs' + in + (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of + NONE => steps + | SOME times => + (* candidate successfully eliminated *) + (decrement_step_count (); + map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) + times succs' meths_outcomess; + map (replace_successor l labels) lfs; + steps_before @ update_steps succs' steps_after)) + end) end - handle Bind => steps - | Match => steps - | Option.Option => steps fun compression_loop candidates steps = if not (compress_further ()) then @@ -246,11 +239,14 @@ else (case pop_next_candidate candidates of (NONE, _) => steps (* no more candidates for elimination *) - | (SOME (cand as (l, _)), candidates') => - let val successors = get_successors l in - if length successors > compress_degree then steps - else compression_loop candidates' (try_eliminate cand successors steps) - end) + | (SOME (l, _), candidates') => + (case find_index (curry (op =) (SOME l) o label_of_isar_step) steps of + ~1 => steps + | i => + let val successors = get_successors l in + if length successors > compress_degree then steps + else compression_loop candidates' (try_eliminate i l successors steps) + end)) fun add_cand (Prove (_, _, l, t, _, _, _, _)) = cons (l, size_of_term t) | add_cand _ = I