# HG changeset patch # User blanchet # Date 1387441700 -3600 # Node ID c8b04da1bd01c155e42ceeeb6aa32741993d932d # Parent a368cd086e46d7a1a85d02d55a437cc32f3753ba tuning diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 18 22:55:43 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Dec 19 09:28:20 2013 +0100 @@ -464,7 +464,7 @@ fun failed failure = ({outcome = SOME failure, used_facts = [], used_from = [], run_time = Time.zeroTime, - preplay = Lazy.value (Sledgehammer_Reconstructor.Failed_to_Play + preplay = Lazy.value (Sledgehammer_Reconstructor.Play_Failed Sledgehammer_Provers.plain_metis), message = K "", message_tail = ""}, ~1) val ({outcome, used_facts, run_time, preplay, message, message_tail, ...} diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed Dec 18 22:55:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 09:28:20 2013 +0100 @@ -1,6 +1,6 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_compress.ML + Author: Steffen Juilf Smolka, TU Muenchen Author: Jasmin Blanchette, TU Muenchen - Author: Steffen Juilf Smolka, TU Muenchen Compression of isar proofs by merging steps. Only proof steps using the same proof method are merged. @@ -170,13 +170,13 @@ | _ => raise Fail "Sledgehammer_Compress: elim_subproofs'") fun elim_subproofs (step as Let _) = step - | elim_subproofs - (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) = - if subproofs = [] then step else - case get_preplay_time l of - (true, _) => step (* timeout or fail *) - | (false, time) => - elim_subproofs' time qs fix l t lfs gfs meth subproofs [] + | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) = + if subproofs = [] then + step + else + (case get_preplay_time l of + (true, _) => step (* timeout or fail *) + | (false, time) => elim_subproofs' time qs fix l t lfs gfs meth subproofs []) (** top_level compression: eliminate steps by merging them into their successors **) @@ -229,8 +229,7 @@ val succs = collect_successors steps' succ_lbls val succs' = map (try_merge cand #> the) succs - (* TODO: should be lazy: stop preplaying as soon as one step - fails/times out *) + (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *) val preplay_times = map2 preplay_quietly timeouts succs' (* ensure none of the modified successors timed out *) @@ -243,8 +242,7 @@ decrement_step_count (); (* candidate successfully eliminated *) map2 set_preplay_time succ_lbls preplay_times; map (replace_successor l succ_lbls) lfs; - (* removing the step would mess up the indices - -> replace with dummy step instead *) + (* removing the step would mess up the indices -> replace with dummy step instead *) steps1 @ dummy_isar_step :: steps2 end handle Bind => steps diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 18 22:55:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 19 09:28:20 2013 +0100 @@ -239,8 +239,7 @@ | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, ""))) handle ERROR msg => - (NONE, (Lazy.value (Failed_to_Play plain_metis), - fn _ => "Error: " ^ msg, "")) + (NONE, (Lazy.value (Play_Failed plain_metis), fn _ => "Error: " ^ msg, "")) end fun adjust_reconstructor_params override_params diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Wed Dec 18 22:55:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Thu Dec 19 09:28:20 2013 +0100 @@ -28,8 +28,7 @@ | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...} (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) = (case get_preplay_time l of - (* don't touch steps that time out or fail; minimizing won't help (not true -- FIXME) *) - (true, _) => step + (true, _) => step (* don't touch steps that time out or fail *) | (false, time) => let fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth)) @@ -69,12 +68,12 @@ (case label_of_step step of NONE => (refed, step :: accu) | SOME l => - if Ord_List.member label_ord refed l then - do_refed_step step - |>> Ord_List.union label_ord refed - ||> (fn x => x :: accu) - else - (refed, accu)) + if Ord_List.member label_ord refed l then + do_refed_step step + |>> Ord_List.union label_ord refed + ||> (fn x => x :: accu) + else + (refed, accu)) and do_refed_step step = step |> postproc_step |> do_refed_step' and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar" | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) = diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Dec 18 22:55:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Dec 19 09:28:20 2013 +0100 @@ -132,9 +132,10 @@ (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis (cf. "~~/src/Pure/Isar/obtain.ML") *) let - val thesis = Term.Free ("thesis", HOLogic.boolT) + (* FIXME: generate fresh name *) + val thesis = Free ("thesis", HOLogic.boolT) val thesis_prop = thesis |> HOLogic.mk_Trueprop - val frees = map Term.Free xs + val frees = map Free xs (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Dec 18 22:55:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Dec 19 09:28:20 2013 +0100 @@ -88,12 +88,12 @@ val (failed, reconstr, ext_time) = case preplay of Played (reconstr, time) => (false, reconstr, (SOME (false, time))) - | Trust_Playable (reconstr, time) => + | Play_Timed_Out (reconstr, time) => (false, reconstr, (case time of NONE => NONE | SOME time => if time = Time.zeroTime then NONE else SOME (true, time))) - | Failed_to_Play reconstr => (true, reconstr, NONE) + | Play_Failed reconstr => (true, reconstr, NONE) val try_line = ([], map fst extra) |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 18 22:55:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 09:28:20 2013 +0100 @@ -403,16 +403,15 @@ else List.last reconstrs in if timeout = SOME Time.zeroTime then - Trust_Playable (get_preferred reconstrs, NONE) + Play_Timed_Out (get_preferred reconstrs, NONE) else let val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else () val ths = pairs |> sort_wrt (fst o fst) |> map snd - fun play [] [] = Failed_to_Play (get_preferred reconstrs) - | play timed_outs [] = - Trust_Playable (get_preferred timed_outs, timeout) + fun play [] [] = Play_Failed (get_preferred reconstrs) + | play timed_outs [] = Play_Timed_Out (get_preferred timed_outs, timeout) | play timed_out (reconstr :: reconstrs) = let val _ = @@ -861,8 +860,7 @@ "")) end | SOME failure => - ([], Lazy.value (Failed_to_Play plain_metis), - fn _ => string_of_atp_failure failure, "") + ([], Lazy.value (Play_Failed plain_metis), fn _ => string_of_atp_failure failure, "") in {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time, preplay = preplay, message = message, @@ -1063,7 +1061,7 @@ else "") | SOME failure => - (Lazy.value (Failed_to_Play plain_metis), + (Lazy.value (Play_Failed plain_metis), fn _ => string_of_atp_failure failure, "") in {outcome = outcome, used_facts = used_facts, used_from = used_from, @@ -1108,7 +1106,7 @@ message_tail = ""} | play => let - val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut + val failure = case play of Play_Failed _ => GaveUp | _ => TimedOut in {outcome = SOME failure, used_facts = [], used_from = [], run_time = Time.zeroTime, preplay = Lazy.value play, diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Dec 18 22:55:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 09:28:20 2013 +0100 @@ -410,8 +410,8 @@ fun isar_proof_would_be_a_good_idea preplay = (case preplay of Played (reconstr, _) => reconstr = SMT - | Trust_Playable _ => false - | Failed_to_Play _ => true) + | Play_Timed_Out _ => false + | Play_Failed _ => true) fun proof_text ctxt isar_proofs isar_params num_chained (one_line_params as (preplay, _, _, _, _, _)) = diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Wed Dec 18 22:55:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Thu Dec 19 09:28:20 2013 +0100 @@ -15,8 +15,8 @@ datatype play = Played of reconstructor * Time.time | - Trust_Playable of reconstructor * Time.time option | - Failed_to_Play of reconstructor + Play_Timed_Out of reconstructor * Time.time option | + Play_Failed of reconstructor type minimize_command = string list -> string type one_line_params = play * string * (string * stature) list * minimize_command * int * int @@ -35,8 +35,8 @@ datatype play = Played of reconstructor * Time.time | - Trust_Playable of reconstructor * Time.time option | - Failed_to_Play of reconstructor + Play_Timed_Out of reconstructor * Time.time option | + Play_Failed of reconstructor type minimize_command = string list -> string type one_line_params = play * string * (string * stature) list * minimize_command * int * int