# HG changeset patch # User blanchet # Date 1387471978 -3600 # Node ID 4e58a38b330ba9023bb57f3209bda66b9873f63b # Parent a510fc40559c4972d80f3feffd4705c2cbfe9f5b refactored preplaying outcome data structure diff -r a510fc40559c -r 4e58a38b330b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Dec 19 17:24:17 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Dec 19 17:52:58 2013 +0100 @@ -464,8 +464,8 @@ fun failed failure = ({outcome = SOME failure, used_facts = [], used_from = [], run_time = Time.zeroTime, - preplay = Lazy.value (Sledgehammer_Reconstructor.Play_Failed - Sledgehammer_Provers.plain_metis), + preplay = Lazy.value (Sledgehammer_Provers.plain_metis, + Sledgehammer_Reconstructor.Play_Failed), message = K "", message_tail = ""}, ~1) val ({outcome, used_facts, run_time, preplay, message, message_tail, ...} : Sledgehammer_Provers.prover_result, diff -r a510fc40559c -r 4e58a38b330b src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 19 17:24:17 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 19 17:52:58 2013 +0100 @@ -8,7 +8,8 @@ signature SLEDGEHAMMER_MINIMIZE = sig type stature = ATP_Problem_Generate.stature - type play = Sledgehammer_Reconstructor.play + type reconstructor = Sledgehammer_Reconstructor.reconstructor + type play_outcome = Sledgehammer_Reconstructor.play_outcome type mode = Sledgehammer_Provers.mode type params = Sledgehammer_Provers.params type prover = Sledgehammer_Provers.prover @@ -16,12 +17,12 @@ val binary_min_facts : int Config.T val auto_minimize_min_facts : int Config.T val auto_minimize_max_time : real Config.T - val minimize_facts : - (thm list -> unit) -> string -> params -> bool -> int -> int - -> Proof.state -> thm -> play Lazy.lazy option - -> ((string * stature) * thm list) list - -> ((string * stature) * thm list) list option - * (play Lazy.lazy * (play -> string) * string) + val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int -> + Proof.state -> thm -> (reconstructor * play_outcome) Lazy.lazy option -> + ((string * stature) * thm list) list -> + ((string * stature) * thm list) list option + * ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string) + * string) val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit @@ -53,11 +54,10 @@ fun print silent f = if silent then () else Output.urgent_message (f ()) -fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, - max_new_mono_instances, type_enc, strict, lam_trans, - uncurried_aliases, isar_proofs, isar_compress, isar_try0, - preplay_timeout, ...} : params) - silent (prover : prover) timeout i n state goal facts = +fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, + type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, isar_compress, isar_try0, + preplay_timeout, ...} : params) + silent (prover : prover) timeout i n state goal facts = let val _ = print silent (fn () => @@ -220,7 +220,7 @@ "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", "")) | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, ""))) - handle ERROR msg => (NONE, (Lazy.value (Play_Failed plain_metis), fn _ => "Error: " ^ msg, "")) + handle ERROR msg => (NONE, (Lazy.value (plain_metis, Play_Failed), fn _ => "Error: " ^ msg, "")) end fun adjust_reconstructor_params override_params @@ -270,7 +270,7 @@ fun prover_fast_enough () = can_min_fast_enough run_time in (case Lazy.force preplay of - Played (reconstr as Metis _, timeout) => + (reconstr as Metis _, Played timeout) => if isar_proofs = SOME true then (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved itself. *) @@ -281,7 +281,7 @@ adjust_reconstructor_params override_params params)) else (prover_fast_enough (), (name, params)) - | Played (SMT, timeout) => + | (SMT, Played timeout) => (* Cheat: Assume the original prover is as fast as "smt" for the goal it proved itself. *) (can_min_fast_enough timeout, (name, params)) @@ -294,9 +294,8 @@ val (used_facts, (preplay, message, _)) = if minimize then minimize_facts do_learn minimize_name params - (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal - subgoal_count state goal (SOME preplay) - (filter_used_facts true used_facts (map (apsnd single) used_from)) + (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state + goal (SOME preplay) (filter_used_facts true used_facts (map (apsnd single) used_from)) |>> Option.map (map fst) else (SOME used_facts, (preplay, message, "")) diff -r a510fc40559c -r 4e58a38b330b src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Dec 19 17:24:17 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Dec 19 17:52:58 2013 +0100 @@ -82,15 +82,15 @@ |> pairself (sort_distinct (string_ord o pairself fst)) fun one_line_proof_text num_chained - (preplay, banner, used_facts, minimize_command, subgoal, subgoal_count) = + ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) = let val (chained, extra) = split_used_facts used_facts - val (failed, reconstr, ext_time) = - (case preplay of - Played (reconstr, time) => (false, reconstr, (SOME (false, time))) - | Not_Played reconstr => (false, reconstr, NONE) - | Play_Timed_Out (reconstr, time) => (false, reconstr, SOME (true, time)) - | Play_Failed reconstr => (true, reconstr, NONE)) + val (failed, ext_time) = + (case play of + Played time => (false, (SOME (false, time))) + | Play_Timed_Out time => (false, SOME (true, time)) + | Play_Failed => (true, NONE) + | Not_Played => (false, NONE)) val try_line = ([], map fst extra) |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained @@ -111,10 +111,9 @@ fun string_of_proof ctxt type_enc lam_trans i n proof = let + (* Make sure only type constraints inserted by the type annotation code are printed. *) val ctxt = - (* make sure type constraint are actually printed *) ctxt |> Config.put show_markup false - (* make sure only type constraints inserted by sh_annotate are printed *) |> Config.put Printer.show_type_emphasis false |> Config.put show_types false |> Config.put show_sorts false @@ -195,9 +194,10 @@ (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs) fun add_fix _ [] = I - | add_fix ind xs = add_suffix (of_indent ind ^ "fix ") - #> add_frees xs - #> add_suffix "\n" + | add_fix ind xs = + add_suffix (of_indent ind ^ "fix ") + #> add_frees xs + #> add_suffix "\n" fun add_assm ind (l, t) = add_suffix (of_indent ind ^ "assume " ^ of_label l) diff -r a510fc40559c -r 4e58a38b330b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 17:24:17 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 17:52:58 2013 +0100 @@ -13,7 +13,7 @@ type type_enc = ATP_Problem_Generate.type_enc type fact = Sledgehammer_Fact.fact type reconstructor = Sledgehammer_Reconstructor.reconstructor - type play = Sledgehammer_Reconstructor.play + type play_outcome = Sledgehammer_Reconstructor.play_outcome type minimize_command = Sledgehammer_Reconstructor.minimize_command datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize @@ -57,8 +57,8 @@ used_facts : (string * stature) list, used_from : fact list, run_time : Time.time, - preplay : play Lazy.lazy, - message : play -> string, + preplay : (reconstructor * play_outcome) Lazy.lazy, + message : reconstructor * play_outcome -> string, message_tail : string} type prover = @@ -298,8 +298,8 @@ used_facts : (string * stature) list, used_from : fact list, run_time : Time.time, - preplay : play Lazy.lazy, - message : play -> string, + preplay : (reconstructor * play_outcome) Lazy.lazy, + message : reconstructor * play_outcome -> string, message_tail : string} type prover = @@ -358,18 +358,13 @@ Metis (really_full_type_enc, lam_trans true), SMT] -fun extract_reconstructor ({type_enc, lam_trans, ...} : params) - (Metis (type_enc', lam_trans')) = +fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) = let val override_params = - (if is_none type_enc andalso type_enc' = hd partial_type_encs then - [] - else - [("type_enc", [hd (unalias_type_enc type_enc')])]) @ - (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then - [] - else - [("lam_trans", [lam_trans'])]) + (if is_none type_enc andalso type_enc' = hd partial_type_encs then [] + else [("type_enc", [hd (unalias_type_enc type_enc')])]) @ + (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then [] + else [("lam_trans", [lam_trans'])]) in (metisN, override_params) end | extract_reconstructor _ SMT = (smtN, []) @@ -382,8 +377,7 @@ TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end -fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = - metis_tac [type_enc] lam_trans +fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans | tac_of_reconstructor SMT = SMT_Solver.smt_tac fun timed_reconstructor reconstr debug timeout ths = @@ -404,13 +398,13 @@ else List.last reconstrs in if timeout = Time.zeroTime then - Not_Played (get_preferred reconstrs) + (get_preferred reconstrs, Not_Played) 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 [] [] = Play_Failed (get_preferred reconstrs) - | play timed_outs [] = Play_Timed_Out (get_preferred timed_outs, timeout) + fun play [] [] = (get_preferred reconstrs, Play_Failed) + | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout) | play timed_out (reconstr :: reconstrs) = let val _ = @@ -422,11 +416,13 @@ val timer = Timer.startRealTimer () in case timed_reconstructor reconstr debug timeout ths state i of - SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer) + SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer)) | _ => play timed_out reconstrs end handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs - in play [] reconstrs end + in + play [] reconstrs + end end @@ -511,17 +507,15 @@ (* See the analogous logic in the function "maybe_minimize" in "sledgehammer_minimize.ML". *) -fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command - name preplay = +fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command name preplay = let - val maybe_isar_name = - name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt + val maybe_isar_name = name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt val (min_name, override_params) = - case preplay of - Played (reconstr, _) => + (case preplay of + (reconstr, Played _) => if isar_proofs = SOME true then (maybe_isar_name, []) else extract_reconstructor params reconstr - | _ => (maybe_isar_name, []) + | _ => (maybe_isar_name, [])) in minimize_command override_params min_name end val max_fact_instances = 10 (* FUDGE *) @@ -551,14 +545,13 @@ val max_fact_factor_fudge = 5 fun run_atp mode name - ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, - best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) - (params as {debug, verbose, overlord, type_enc, strict, lam_trans, - uncurried_aliases, fact_filter, max_facts, max_mono_iters, - max_new_mono_instances, isar_proofs, isar_compress, - isar_try0, slice, timeout, preplay_timeout, ...}) - minimize_command - ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = + ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, + best_max_new_mono_instances, ...} : atp_config) + (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, + fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, isar_compress, + isar_try0, slice, timeout, preplay_timeout, ...}) + minimize_command + ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -776,7 +769,7 @@ else "" val (used_facts, preplay, message, message_tail) = - case outcome of + (case outcome of NONE => let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof @@ -787,20 +780,13 @@ in (used_facts, Lazy.lazy (fn () => - let - val used_pairs = - used_from |> filter_used_facts false used_facts - in - play_one_line_proof mode debug verbose preplay_timeout - used_pairs state subgoal (hd reconstrs) reconstrs + let val used_pairs = used_from |> filter_used_facts false used_facts in + play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal + (hd reconstrs) reconstrs end), fn preplay => let - val _ = - if verbose then - Output.urgent_message "Generating proof text..." - else - () + val _ = if verbose then Output.urgent_message "Generating proof text..." else () fun isar_params () = let val metis_type_enc = @@ -824,26 +810,19 @@ in proof_text ctxt isar_proofs isar_params num_chained one_line_params end, - (if verbose then - "\nATP real CPU time: " ^ string_of_time run_time ^ "." - else - "") ^ + (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^ (if important_message <> "" then - "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ - important_message + "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message else "")) end | SOME failure => - ([], Lazy.value (Play_Failed plain_metis), fn _ => string_of_atp_failure failure, "") + ([], Lazy.value (plain_metis, Play_Failed), 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, - message_tail = message_tail} + {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time, + preplay = preplay, message = message, message_tail = message_tail} end -fun rotate_one (x :: xs) = xs @ [x] - (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out properly in the SMT module, we have to interpret these ourselves. *) @@ -962,7 +941,7 @@ Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts) val weighted_factss as (new_fact_filter, _) :: _ = weighted_factss - |> rotate_one + |> (fn (x :: xs) => xs @ [x]) |> app_hd (apsnd (take new_num_facts)) val show_filter = fact_filter <> new_fact_filter fun num_of_facts fact_filter num_facts = @@ -983,15 +962,15 @@ do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss end else - {outcome = if is_none outcome then NONE else the outcome0, - used_facts = used_facts, used_from = map (apsnd snd) weighted_facts, - run_time = time_so_far} + {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts, + used_from = map (apsnd snd) weighted_facts, run_time = time_so_far} end - in do_slice timeout 1 NONE Time.zeroTime end + in + do_slice timeout 1 NONE Time.zeroTime + end -fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) - minimize_command - ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = +fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command + ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let val ctxt = Proof.context_of state fun weight_facts facts = @@ -1016,19 +995,15 @@ let val one_line_params = (preplay, proof_banner mode name, used_facts, - choose_minimize_command ctxt params minimize_command name - preplay, + choose_minimize_command ctxt params minimize_command name preplay, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in one_line_proof_text num_chained one_line_params end, - if verbose then - "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." - else - "") + if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "") | SOME failure => - (Lazy.value (Play_Failed plain_metis), + (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, "") in {outcome = outcome, used_facts = used_facts, used_from = used_from, @@ -1052,20 +1027,19 @@ raise Fail ("unknown reconstructor: " ^ quote name) val used_facts = facts |> map fst in - case play_one_line_proof (if mode = Minimize then Normal else mode) debug + (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts state subgoal reconstr [reconstr] of - play as Played (_, time) => - {outcome = NONE, used_facts = used_facts, used_from = facts, - run_time = time, preplay = Lazy.value play, + play as (_, Played time) => + {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time, + preplay = Lazy.value play, message = fn play => let val (_, override_params) = extract_reconstructor params reconstr val one_line_params = - (play, proof_banner mode name, used_facts, - minimize_command override_params name, subgoal, - subgoal_count) + (play, proof_banner mode name, used_facts, minimize_command override_params name, + subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in one_line_proof_text num_chained one_line_params @@ -1073,12 +1047,12 @@ message_tail = ""} | play => let - val failure = case play of Play_Failed _ => 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, message = fn _ => string_of_atp_failure failure, message_tail = ""} - end + end) end fun get_prover ctxt mode name = diff -r a510fc40559c -r 4e58a38b330b src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 17:24:17 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 17:52:58 2013 +0100 @@ -402,12 +402,12 @@ if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "") in one_line_proof ^ isar_proof end -fun isar_proof_would_be_a_good_idea preplay = - (case preplay of - Played (reconstr, _) => reconstr = SMT - | Not_Played _ => false +fun isar_proof_would_be_a_good_idea (reconstr, play) = + (case play of + Played _ => reconstr = SMT | Play_Timed_Out _ => true - | Play_Failed _ => true) + | Play_Failed => true + | Not_Played => false) fun proof_text ctxt isar_proofs isar_params num_chained (one_line_params as (preplay, _, _, _, _, _)) = diff -r a510fc40559c -r 4e58a38b330b src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Thu Dec 19 17:24:17 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Thu Dec 19 17:52:58 2013 +0100 @@ -13,14 +13,15 @@ Metis of string * string | SMT - datatype play = - Played of reconstructor * Time.time | - Not_Played of reconstructor | - Play_Timed_Out of reconstructor * Time.time | - Play_Failed of reconstructor + datatype play_outcome = + Played of Time.time | + Play_Timed_Out of Time.time | + Play_Failed | + Not_Played type minimize_command = string list -> string - type one_line_params = play * string * (string * stature) list * minimize_command * int * int + type one_line_params = + (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int val smtN : string end; @@ -34,14 +35,15 @@ Metis of string * string | SMT -datatype play = - Played of reconstructor * Time.time | - Not_Played of reconstructor | - Play_Timed_Out of reconstructor * Time.time | - Play_Failed of reconstructor +datatype play_outcome = + Played of Time.time | + Play_Timed_Out of Time.time | + Play_Failed | + Not_Played type minimize_command = string list -> string -type one_line_params = play * string * (string * stature) list * minimize_command * int * int +type one_line_params = + (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int val smtN = "smt"