# HG changeset patch # User blanchet # Date 1391370831 -3600 # Node ID eceebcea3e001bcddd19e8b2e205cdb7eaa5cc49 # Parent 2bc951e6761a87f3b99b8a8e5bddb8973d65db37 refactoring of data structure (step 2) diff -r 2bc951e6761a -r eceebcea3e00 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sun Feb 02 20:53:51 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sun Feb 02 20:53:51 2014 +0100 @@ -98,7 +98,7 @@ (* Precondition: The proof must be labeled canonically (cf. "Slegehammer_Isar_Proof.relabel_isar_proof_canonically"). *) fun compress_isar_proof compress_isar - ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data) proof = + ({preplay_step, preplay_outcome, set_preplay_outcomes, ...} : isar_preplay_data) proof = if compress_isar <= 1.0 then proof else @@ -161,8 +161,8 @@ 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'' + val timeout = time_mult merge_timeout_slack (Time.+ (time, time')) + val Played time'' = preplay_step timeout (hd meths)(*FIXME*) step'' in decrement_step_count (); (* l' successfully eliminated! *) map (replace_successor l' [l]) lfs'; @@ -238,7 +238,7 @@ () (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *) - val play_outcomes = map2 preplay_quietly timeouts succs' + val play_outcomes = map3 preplay_step timeouts succ_meths succs' (* ensure none of the modified successors timed out *) val true = forall (fn Played _ => true) play_outcomes diff -r 2bc951e6761a -r eceebcea3e00 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 20:53:51 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 20:53:51 2014 +0100 @@ -26,7 +26,7 @@ val slack = seconds 0.1 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step - | minimize_isar_step_dependencies {set_preplay_outcomes, preplay_outcome, preplay_quietly, ...} + | minimize_isar_step_dependencies {preplay_step, set_preplay_outcomes, preplay_outcome, ...} (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) = (case Lazy.force (preplay_outcome l meth) of Played time => @@ -36,7 +36,7 @@ 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 + (case preplay_step (Time.+ (time, slack)) meth (mk_step (min_facts @ facts)) of Played time => minimize_facts mk_step time min_facts facts | _ => minimize_facts mk_step time (f :: min_facts) facts) diff -r 2bc951e6761a -r eceebcea3e00 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100 @@ -16,9 +16,9 @@ val trace : bool Config.T type isar_preplay_data = - {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit, + {preplay_step: Time.time -> proof_method -> isar_step -> play_outcome, + set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit, preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy, - preplay_quietly: Time.time -> isar_step -> play_outcome, overall_preplay_outcome: isar_proof -> play_outcome} val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> Time.time -> @@ -95,7 +95,7 @@ | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method")) (* main function for preplaying Isar steps; may throw exceptions *) -fun preplay_raw debug type_enc lam_trans ctxt timeout meth +fun raw_preplay_step debug type_enc lam_trans ctxt timeout meth (Prove (_, xs, _, t, subproofs, (fact_names, _))) = let val goal = @@ -137,7 +137,7 @@ type isar_preplay_data = {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit, preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy, - preplay_quietly: Time.time -> isar_step -> play_outcome, + preplay_step: Time.time -> proof_method -> isar_step -> play_outcome, overall_preplay_outcome: isar_proof -> play_outcome} fun enrich_context_with_local_facts proof ctxt = @@ -176,22 +176,9 @@ let val ctxt = enrich_context_with_local_facts proof ctxt - 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 - else - (if not quietly andalso debug then - warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn) - else - (); - Play_Failed) - - (* preplay steps treating exceptions like timeouts *) - fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) = - preplay true timeout meth step - | preplay_quietly _ _ = Played Time.zeroTime + fun preplay_step timeout meth = + try (raw_preplay_step debug type_enc lam_trans ctxt timeout meth) + #> the_default Play_Failed val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty @@ -216,15 +203,15 @@ fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) = preplay_tab := Canonical_Label_Tab.update (l, map (fn meth => - (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths) + (meth, Lazy.lazy (fn () => preplay_step preplay_timeout meth step))) meths) (!preplay_tab) | reset_preplay_outcomes _ = () val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) () in - {set_preplay_outcomes = set_preplay_outcomes, + {preplay_step = preplay_step, + set_preplay_outcomes = set_preplay_outcomes, preplay_outcome = preplay_outcome, - preplay_quietly = preplay_quietly, overall_preplay_outcome = overall_preplay_outcome} end diff -r 2bc951e6761a -r eceebcea3e00 src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Sun Feb 02 20:53:51 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Sun Feb 02 20:53:51 2014 +0100 @@ -22,31 +22,30 @@ open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay -fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meths))) = - map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) (tl meths) - | variants_of_step _ = raise Fail "Sledgehammer_Isar_Try0: variants_of_step" +fun step_with_method meth (Prove (qs, xs, l, t, subproofs, (facts, _))) = + Prove (qs, xs, l, t, subproofs, (facts, [meth])) val slack = seconds 0.05 fun try0_step _ _ (step as Let _) = step | try0_step preplay_timeout - ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data) - (step as Prove (_, _, l, _, _, (_, meth :: _))) = + ({preplay_step, set_preplay_outcomes, preplay_outcome, ...} : isar_preplay_data) + (step as Prove (_, _, l, _, _, (_, meths as meth :: _))) = let val timeout = (case Lazy.force (preplay_outcome l meth) of Played time => Time.+ (time, slack) | _ => preplay_timeout) - fun try_variant variant = - (case preplay_quietly timeout variant of - result as Played _ => SOME (variant, result) + fun try_method meth = + (case preplay_step timeout meth step of + outcome as Played _ => SOME (meth, outcome) | _ => NONE) in (* FIXME: create variant after success *) - (case Par_List.get_some try_variant (variants_of_step step) of - SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), outcome) => - (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step') + (case Par_List.get_some try_method meths of + SOME (meth', outcome) => + (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step_with_method meth' step) | NONE => step) end