# HG changeset patch # User blanchet # Date 1391418858 -3600 # Node ID 236114c5eb44ba1827330a6621f31572bbe3c9c0 # Parent e78476a99c705ca7d394bccae195750bf93f1028 tuning diff -r e78476a99c70 -r 236114c5eb44 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 @@ -155,11 +155,10 @@ (sub as Proof (_, assms, sub_steps)) :: subs => (let (* trivial subproofs have exactly one "Prove" step *) - val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), meth' :: _))) = - try the_single sub_steps + val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps (* only touch proofs that can be preplayed sucessfully *) - val Played time' = forced_preplay_outcome_of_isar_step (!preplay_data) l' + val Played time' = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l' (* merge steps *) val subs'' = subs @ nontriv_subs @@ -181,12 +180,11 @@ | _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof") fun elim_subproofs (step as Let _) = step - | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, - ((lfs, gfs), meths as meth :: _))) = + | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meths))) = if subproofs = [] then step else - (case forced_preplay_outcome_of_isar_step (!preplay_data) l of + (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs [] | _ => step) @@ -220,18 +218,18 @@ fun try_eliminate (i, l, _) labels steps = let - val ((cand as Prove (_, _, l, _, _, ((lfs, _), meth :: _))) :: steps') = drop i steps + val ((cand as Prove (_, _, _, _, _, ((lfs, _), _))) :: steps') = drop i steps val succs = collect_successors steps' labels 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 = forced_preplay_outcome_of_isar_step (!preplay_data) l + val Played time = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l val succs' = map (try_merge cand #> the) succs val times0 = map ((fn Played time => time) o - forced_preplay_outcome_of_isar_step (!preplay_data)) labels + 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 #> slackify_merge_timeout) times0 diff -r e78476a99c70 -r 236114c5eb44 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,7 +22,7 @@ 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 forced_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome + val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome 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 @@ -184,9 +184,7 @@ fun peek_at_outcome outcome = if Lazy.is_finished outcome then Lazy.force outcome else Not_Played -(* -*) -fun forced_preplay_outcome_of_isar_step preplay_data l = +fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l = let fun get_best_outcome_available get_one = the (Canonical_Label_Tab.lookup preplay_data l)