# HG changeset patch # User blanchet # Date 1387183202 -3600 # Node ID 430ca13d3e54b462f71c680986b3e8fc0185938c # Parent c3ef7b572213361defd80d2dd429a53a1e59e267 tuning diff -r c3ef7b572213 -r 430ca13d3e54 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Dec 16 09:17:58 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Dec 16 09:40:02 2013 +0100 @@ -2,7 +2,7 @@ Author: Steffen Juilf Smolka, TU Muenchen Author: Jasmin Blanchette, TU Muenchen -Preplaying of isar proofs. +Preplaying of Isar proofs. *) signature SLEDGEHAMMER_PREPLAY = @@ -11,24 +11,21 @@ type isar_step = Sledgehammer_Proof.isar_step type label = Sledgehammer_Proof.label - eqtype preplay_time - type preplay_result val trace: bool Config.T - val zero_preplay_time: preplay_time - val some_preplay_time: preplay_time - val add_preplay_time: preplay_time -> preplay_time -> preplay_time - val string_of_preplay_time: preplay_time -> string + val zero_preplay_time: bool * Time.time + val some_preplay_time: bool * Time.time + val add_preplay_time: bool * Time.time -> bool * Time.time -> bool * Time.time type preplay_interface = {get_preplay_result: label -> preplay_result, set_preplay_result: label -> preplay_result -> unit, - get_preplay_time: label -> preplay_time, - set_preplay_time: label -> preplay_time -> unit, - preplay_quietly: Time.time -> isar_step -> preplay_time, + get_preplay_time: label -> bool * Time.time, + set_preplay_time: label -> bool * Time.time -> unit, + preplay_quietly: Time.time -> isar_step -> bool * Time.time, (* the returned flag signals a preplay failure *) - overall_preplay_stats: isar_proof -> preplay_time * bool} + overall_preplay_stats: isar_proof -> (bool * Time.time) * bool} val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time -> isar_proof -> preplay_interface @@ -37,33 +34,25 @@ structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY = struct +open ATP_Util open Sledgehammer_Util open Sledgehammer_Proof -val trace = - Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) - -(* The boolean flag encodes whether the time is exact (false) or an lower bound - (true): - (t, false) = "t ms" - (t, true) = "> t ms" *) -type preplay_time = bool * Time.time +val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) datatype preplay_result = - Preplay_Success of preplay_time | + Preplay_Success of bool * Time.time | Preplay_Failure of exn val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *) val some_preplay_time = (true, Time.zeroTime) (* > 0 ms *) -fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) - -val string_of_preplay_time = ATP_Util.string_of_ext_time +fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+ (t1, t2)) fun preplay_trace ctxt assms concl time = let val ctxt = ctxt |> Config.put show_markup true - val time = "[" ^ (string_of_preplay_time time) ^ "]" |> Pretty.str + val time = "[" ^ string_of_ext_time time ^ "]" |> Pretty.str val nr_of_assms = length assms val assms = assms |> map (Display.pretty_thm ctxt) @@ -117,22 +106,22 @@ (case method of MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts | _ => - Method.insert_tac facts THEN' - (case method of - SimpM => Simplifier.asm_full_simp_tac - | AutoM => Clasimp.auto_tac #> K - | FastforceM => Clasimp.fast_force_tac - | ForceM => Clasimp.force_tac - | ArithM => Arith_Data.arith_tac - | BlastM => blast_tac - | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt) + Method.insert_tac facts THEN' + (case method of + SimpM => Simplifier.asm_full_simp_tac + | AutoM => Clasimp.auto_tac #> K + | FastforceM => Clasimp.fast_force_tac + | ForceM => Clasimp.force_tac + | ArithM => Arith_Data.arith_tac + | BlastM => blast_tac + | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt) (* main function for preplaying Isar steps; may throw exceptions *) fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time | preplay_raw debug type_enc lam_trans ctxt timeout (step as Prove (_, xs, _, t, subproofs, (fact_names, meth))) = let - val prop = + val goal = (case xs of [] => t | _ => @@ -152,19 +141,18 @@ val facts = map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names - val ctxt = ctxt - |> Config.put Metis_Tactic.verbose debug - |> Config.put Lin_Arith.verbose debug + val ctxt' = ctxt + |> debug ? (Config.put Metis_Tactic.verbose true #> Config.put Lin_Arith.verbose true) |> use_metis_new_skolem step ? Config.put Metis_Tactic.new_skolem true - val goal = Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop + val prove = Goal.prove ctxt' [] [] goal fun tac {context = ctxt, ...} = HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts) - fun run_tac () = goal tac handle ERROR msg => error ("Preplay error: " ^ msg) + fun run_tac () = prove tac handle ERROR msg => error ("Preplay error: " ^ msg) val preplay_time = take_time timeout run_tac () in - (if Config.get ctxt trace then preplay_trace ctxt facts prop preplay_time else (); + (if Config.get ctxt trace then preplay_trace ctxt facts goal preplay_time else (); preplay_time) end @@ -174,11 +162,11 @@ type preplay_interface = {get_preplay_result: label -> preplay_result, set_preplay_result: label -> preplay_result -> unit, - get_preplay_time: label -> preplay_time, - set_preplay_time: label -> preplay_time -> unit, - preplay_quietly: Time.time -> isar_step -> preplay_time, + get_preplay_time: label -> bool * Time.time, + set_preplay_time: label -> bool * Time.time -> unit, + preplay_quietly: Time.time -> isar_step -> bool * Time.time, (* the returned flag signals a preplay failure *) - overall_preplay_stats: isar_proof -> preplay_time * bool} + overall_preplay_stats: isar_proof -> (bool * Time.time) * bool} fun enrich_context_with_local_facts proof ctxt = let @@ -202,7 +190,7 @@ to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated calculation. - Precondition: The proof must be labeled canocially; cf. + Precondition: The proof must be labeled canonically; cf. "Slegehammer_Proof.relabel_proof_canonically". *) fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay preplay_timeout proof = if not do_preplay then @@ -218,8 +206,7 @@ val ctxt = enrich_context_with_local_facts proof ctxt fun preplay quietly timeout step = - preplay_raw debug type_enc lam_trans ctxt timeout step - |> Preplay_Success + Preplay_Success (preplay_raw debug type_enc lam_trans ctxt timeout step) handle exn => if Exn.is_interrupt exn then reraise exn @@ -239,11 +226,11 @@ val preplay_tab = let fun add_step_to_tab step tab = - case label_of_step step of - NONE => tab - | SOME l => - Canonical_Lbl_Tab.update_new - (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab + (case label_of_step step of + NONE => tab + | SOME l => + Canonical_Lbl_Tab.update_new + (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab) handle Canonical_Lbl_Tab.DUP _ => raise Fail "Sledgehammer_Preplay: preplay time table" in Canonical_Lbl_Tab.empty @@ -263,20 +250,19 @@ Preplay_Success preplay_time => preplay_time | Preplay_Failure _ => some_preplay_time) - fun set_preplay_time l time = set_preplay_result l (Preplay_Success time) + fun set_preplay_time l = set_preplay_result l o Preplay_Success + + val result_of_step = + try (label_of_step #> the #> get_preplay_result) + #> the_default (Preplay_Success zero_preplay_time) + + fun do_step step = + (case result_of_step step of + Preplay_Success preplay_time => apfst (add_preplay_time preplay_time) + | Preplay_Failure _ => apsnd (K true)) fun overall_preplay_stats (Proof (_, _, steps)) = - let - fun result_of_step step = - try (label_of_step #> the #> get_preplay_result) step - |> the_default (Preplay_Success zero_preplay_time) - fun do_step step = - (case result_of_step step of - Preplay_Success preplay_time => apfst (add_preplay_time preplay_time) - | Preplay_Failure _ => apsnd (K true)) - in - fold_isar_steps do_step steps (zero_preplay_time, false) - end + fold_isar_steps do_step steps (zero_preplay_time, false) in {get_preplay_result = get_preplay_result, set_preplay_result = set_preplay_result, diff -r c3ef7b572213 -r 430ca13d3e54 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 16 09:17:58 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 16 09:40:02 2013 +0100 @@ -436,8 +436,7 @@ else []) @ (if do_preplay then - [(if preplay_fail then "may fail, " else "") ^ - string_of_preplay_time preplay_time] + [(if preplay_fail then "may fail, " else "") ^ string_of_ext_time preplay_time] else []) in