# HG changeset patch # User blanchet # Date 1391370831 -3600 # Node ID 0dc4993b4f560aeafd2e36e8847eb6d1a59e9eee # Parent 85f5d7da4ab684d0c36480f82bd749d0d2a4b944 refactor data structure (step 1) diff -r 85f5d7da4ab6 -r 0dc4993b4f56 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_outcome, preplay_quietly, ...} : isar_preplay_data) proof = + ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data) proof = if compress_isar <= 1.0 then proof else @@ -137,9 +137,10 @@ end (* elimination of trivial, one-step subproofs *) - fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs = + fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: meths') subs nontriv_subs = if null subs orelse not (compress_further ()) then - (set_preplay_outcome l meth (Played time); + (set_preplay_outcomes l ((meth, Lazy.value (Played time)) :: + map (rpair (Lazy.value Not_Played)(*FIXME*)) meths'); Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meths))) else (case subs of @@ -215,7 +216,8 @@ val ((cand as Prove (_, _, l, _, _, ((lfs, _), meth :: _))) :: steps') = drop i steps val succs = collect_successors steps' succ_lbls - val succ_meths = map (hd o snd o the o byline_of_isar_step) succs + val succ_methss = map (snd o the o byline_of_isar_step) succs + val succ_meths = map hd succ_methss (* FIXME *) (* only touch steps that can be preplayed successfully *) val Played time = Lazy.force (preplay_outcome l meth) @@ -244,9 +246,13 @@ val (steps1, _ :: steps2) = chop i steps (* replace successors with their modified versions *) val steps2 = update_steps steps2 succs' + + val succ_meths_outcomess = + map2 (fn meth :: meths => fn outcome => (meth, Lazy.value outcome) :: + map (rpair (Lazy.value Not_Played)(*FIXME*)) meths) succ_methss play_outcomes in decrement_step_count (); (* candidate successfully eliminated *) - map3 set_preplay_outcome succ_lbls succ_meths play_outcomes; + map2 set_preplay_outcomes succ_lbls succ_meths_outcomess; 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 85f5d7da4ab6 -r 0dc4993b4f56 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,8 +26,7 @@ val slack = seconds 0.1 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step - | minimize_isar_step_dependencies - {reset_preplay_outcomes, set_preplay_outcome, preplay_outcome, preplay_quietly, ...} + | minimize_isar_step_dependencies {set_preplay_outcomes, preplay_outcome, preplay_quietly, ...} (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) = (case Lazy.force (preplay_outcome l meth) of Played time => @@ -43,12 +42,9 @@ 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 - - val step' = mk_step_lfs_gfs min_lfs min_gfs in - reset_preplay_outcomes step'; - set_preplay_outcome l meth (Played time); - step' + set_preplay_outcomes l [(meth, Lazy.value (Played time))]; + mk_step_lfs_gfs min_lfs min_gfs end | _ => step (* don't touch steps that time out or fail *)) diff -r 85f5d7da4ab6 -r 0dc4993b4f56 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,8 +16,7 @@ val trace : bool Config.T type isar_preplay_data = - {reset_preplay_outcomes: isar_step -> unit, - set_preplay_outcome: label -> proof_method -> play_outcome -> unit, + {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} @@ -136,8 +135,7 @@ end type isar_preplay_data = - {reset_preplay_outcomes: isar_step -> unit, - set_preplay_outcome: label -> proof_method -> play_outcome -> unit, + {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} @@ -177,8 +175,7 @@ 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 *) - {reset_preplay_outcomes = K (), - set_preplay_outcome = K (K (K ())), + {set_preplay_outcomes = K (K ()), preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))), preplay_quietly = K (K (Played Time.zeroTime)), overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data @@ -205,15 +202,9 @@ val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty - 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) - (!preplay_tab) - | reset_preplay_outcomes _ = () - - 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 set_preplay_outcomes l meths_outcomes = + preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes) + (!preplay_tab) fun preplay_outcome l meth = (case Canonical_Label_Tab.lookup (!preplay_tab) l of @@ -223,17 +214,22 @@ | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method") | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label") - val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) () - 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) + + 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) + (!preplay_tab) + | reset_preplay_outcomes _ = () + + val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) () in - {reset_preplay_outcomes = reset_preplay_outcomes, - set_preplay_outcome = set_preplay_outcome, + {set_preplay_outcomes = set_preplay_outcomes, preplay_outcome = preplay_outcome, preplay_quietly = preplay_quietly, overall_preplay_outcome = overall_preplay_outcome} diff -r 85f5d7da4ab6 -r 0dc4993b4f56 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 @@ -30,7 +30,7 @@ fun try0_step _ _ (step as Let _) = step | try0_step preplay_timeout - ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) + ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data) (step as Prove (_, _, l, _, _, (_, meth :: _))) = let val timeout = @@ -45,8 +45,8 @@ in (* FIXME: create variant after success *) (case Par_List.get_some try_variant (variants_of_step step) of - SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), result) => - (set_preplay_outcome l meth' result; step') + SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), outcome) => + (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step') | NONE => step) end