# HG changeset patch # User blanchet # Date 1406897037 -7200 # Node ID 18bb3e1ff6f6a7758db11644adcaa5c77c44dba6 # Parent bcb84750eca593808f09040b1e4fdbbe025766f8 rationalized preplaying by eliminating (now superfluous) laziness diff -r bcb84750eca5 -r 18bb3e1ff6f6 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 01 14:43:57 2014 +0200 @@ -34,6 +34,8 @@ open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Proof_Methods +open Sledgehammer_Isar_Proof +open Sledgehammer_Isar_Preplay open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize @@ -49,17 +51,46 @@ fun max_outcome_code codes = NONE |> fold (fn candidate => - fn accum as SOME _ => accum - | NONE => if member (op =) codes candidate then SOME candidate else NONE) - ordered_outcome_codes + fn accum as SOME _ => accum + | NONE => if member (op =) codes candidate then SOME candidate else NONE) + ordered_outcome_codes |> the_default unknownN fun prover_description verbose name num_facts = (quote name, if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "") -fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode - output_result minimize_command only learn +fun play_one_line_proof mode timeout used_facts state i (preferred, methss as (meth :: _) :: _) = + let + fun dont_know () = + (if exists (fn meths => member (op =) meths preferred) methss then preferred else meth, + Play_Timed_Out Time.zeroTime) + in + if timeout = Time.zeroTime then + dont_know () + else + let + val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else () + val facts = used_facts |> map (fst o fst) |> sort string_ord + + val {context = ctxt, facts = chained, goal} = Proof.goal state + val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt + val goal_t = Logic.list_implies (map prop_of chained @ hyp_ts, concl_t) + + fun try_methss [] = dont_know () + | try_methss (meths :: methss) = + let val step = Prove ([], [], ("", 0), goal_t, [], ([], facts), meths, "") in + (case preplay_isar_step ctxt timeout [] step of + (res as (_, Played _)) :: _ => res + | _ => try_methss methss) + end + in + try_methss methss + end + end + +fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, preplay_timeout, + expect, ...}) mode output_result minimize_command only learn {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = let val ctxt = Proof.context_of state @@ -75,10 +106,9 @@ {comment = comment, state = state, goal = goal, subgoal = subgoal, subgoal_count = subgoal_count, factss = factss - |> map (apsnd ((not (is_ho_atp ctxt name) - ? filter_out (fn ((_, (_, Induction)), _) => true - | _ => false)) - #> take num_facts))} + |> map (apsnd ((not (is_ho_atp ctxt name) + ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false)) + #> take num_facts))} fun print_used_facts used_facts used_from = tag_list 1 used_from @@ -115,8 +145,8 @@ |> AList.group (op =) |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) in - "Success: Found proof with " ^ string_of_int num_used_facts ^ - " of " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ + "Success: Found proof with " ^ string_of_int num_used_facts ^ " of " ^ + string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ (if num_used_facts = 0 then "" else ": " ^ commas filter_infos) end | spying_str_of_res {outcome = SOME failure, ...} = @@ -125,15 +155,17 @@ fun really_go () = problem |> get_minimizing_prover ctxt mode learn name params minimize_command - |> verbose - ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => - print_used_facts used_facts used_from - | _ => ()) + |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => + print_used_facts used_facts used_from + | _ => ()) |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) - |> (fn {outcome, preplay, message, message_tail, ...} => - (if outcome = SOME ATP_Proof.TimedOut then timeoutN - else if is_some outcome then noneN - else someN, fn () => message (Lazy.force preplay) ^ message_tail)) + |> (fn {outcome, used_facts, used_from, preferred_methss, message, message_tail, ...} => + (if outcome = SOME ATP_Proof.TimedOut then timeoutN + else if is_some outcome then noneN + else someN, + fn () => message (play_one_line_proof mode preplay_timeout + (filter_used_facts false used_facts used_from) state subgoal + preferred_methss) ^ message_tail)) fun go () = let diff -r bcb84750eca5 -r 18bb3e1ff6f6 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Aug 01 14:43:57 2014 +0200 @@ -41,25 +41,26 @@ val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) -fun par_list_map_filter_with_timeout get_time timeout0 f xs = - let - val next_timeout = Unsynchronized.ref timeout0 +fun par_list_map_filter_with_timeout _ _ _ [] = [] + | par_list_map_filter_with_timeout get_time timeout0 f xs = + let + val next_timeout = Unsynchronized.ref timeout0 - fun apply_f x = - let val timeout = !next_timeout in - if timeout = Time.zeroTime then - NONE - else - let val y = f timeout x in - (case get_time y of - SOME time => next_timeout := time - | _ => ()); - SOME y - end - end - in - map_filter I (Par_List.map apply_f xs) - end + fun apply_f x = + let val timeout = !next_timeout in + if timeout = Time.zeroTime then + NONE + else + let val y = f timeout x in + (case get_time y of + SOME time => next_timeout := time + | _ => ()); + SOME y + end + end + in + map_filter I (Par_List.map apply_f xs) + end fun enrich_context_with_local_facts proof ctxt = let diff -r bcb84750eca5 -r 18bb3e1ff6f6 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200 @@ -57,8 +57,8 @@ {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, + preferred_methss : proof_method * proof_method list list, run_time : Time.time, - preplay : (proof_method * play_outcome) Lazy.lazy, message : proof_method * play_outcome -> string, message_tail : string} @@ -71,12 +71,10 @@ val overlord_file_location_of_prover : string -> string * string val proof_banner : mode -> string -> string val is_atp : theory -> string -> bool - val bunch_of_proof_methods : bool -> bool -> string -> proof_method list + val bunches_of_proof_methods : bool -> bool -> string -> proof_method list list val is_fact_chained : (('a * stature) * 'b) -> bool val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> ((''a * stature) * 'b) list - val play_one_line_proof : mode -> Time.time -> ((string * 'a) * thm) list -> Proof.state -> int -> - proof_method -> proof_method list -> proof_method * play_outcome val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> Proof.context @@ -98,8 +96,6 @@ open Metis_Tactic open Sledgehammer_Fact open Sledgehammer_Proof_Methods -open Sledgehammer_Isar_Proof -open Sledgehammer_Isar_Preplay (* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *) @@ -155,8 +151,8 @@ {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, + preferred_methss : proof_method * proof_method list list, run_time : Time.time, - preplay : (proof_method * play_outcome) Lazy.lazy, message : proof_method * play_outcome -> string, message_tail : string} @@ -172,54 +168,27 @@ | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" | _ => "Try this") -fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans = - [Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Meson_Method, - Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE), - Force_Method, Linarith_Method, Presburger_Method] @ - (if needs_full_types then - [Metis_Method (SOME really_full_type_enc, NONE), - Metis_Method (SOME full_typesN, SOME desperate_lam_trans), - Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] - else - [Metis_Method (SOME full_typesN, NONE), - Metis_Method (SOME no_typesN, SOME desperate_lam_trans), - Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @ - (if smt_proofs then [SMT2_Method] else []) - -fun preplay_methods timeout facts meths state i = - let - val {context = ctxt, facts = chained, goal} = Proof.goal state - val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt - val step = - Prove ([], [], ("", 0), Logic.list_implies (map prop_of chained @ hyp_ts, concl_t), [], - ([], facts), meths, "") - in - preplay_isar_step ctxt timeout [] step - end +fun bunches_of_proof_methods smt_proofs needs_full_types desperate_lam_trans = + [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method], + [Fastforce_Method, Meson_Method, + Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE), + Force_Method, Presburger_Method], + (if needs_full_types then + [Metis_Method (NONE, NONE), + Metis_Method (SOME really_full_type_enc, NONE), + Metis_Method (SOME full_typesN, SOME desperate_lam_trans), + Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] + else + [Metis_Method (SOME full_typesN, NONE), + Metis_Method (SOME no_typesN, SOME desperate_lam_trans), + Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)])] @ + (if smt_proofs then [[SMT2_Method]] else []) fun is_fact_chained ((_, (sc, _)), _) = sc = Chained fun filter_used_facts keep_chained used = filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false)) -fun play_one_line_proof mode timeout used_facts state i preferred (meths as meth :: _) = - let - fun dont_know () = - (if member (op =) meths preferred then preferred else meth, Play_Timed_Out Time.zeroTime) - in - if timeout = Time.zeroTime then - dont_know () - else - let - val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else () - val gfs = used_facts |> map (fst o fst) |> sort string_ord - in - (case preplay_methods timeout gfs meths state i of - res :: _ => res - | [] => dont_know ()) - end - end - val max_fact_instances = 10 (* FUDGE *) fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances = diff -r bcb84750eca5 -r 18bb3e1ff6f6 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200 @@ -355,21 +355,18 @@ else "" - val (used_facts, preplay, message, message_tail) = + val (used_facts, preferred_methss, message, message_tail) = (case outcome of NONE => let val used_facts = used_facts_in_atp_proof ctxt (map fst used_from) atp_proof val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof - val meths = - bunch_of_proof_methods (smt_proofs <> SOME false) needs_full_types + val preferred_methss = + bunches_of_proof_methods (smt_proofs <> SOME false) needs_full_types (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN) + |> `(hd o hd) in - (used_facts, - Lazy.lazy (fn () => - let val used_pairs = used_from |> filter_used_facts false used_facts in - play_one_line_proof mode preplay_timeout used_pairs state subgoal (hd meths) meths - end), + (used_facts, preferred_methss, fn preplay => let val _ = if verbose then Output.urgent_message "Generating proof text..." else () @@ -404,11 +401,11 @@ "")) end | SOME failure => - ([], Lazy.value (Metis_Method (NONE, NONE), Play_Failed), - fn _ => string_of_atp_failure failure, "")) + ([], (Auto_Method (* dummy *), []), 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, + preferred_methss = preferred_methss, run_time = run_time, message = message, + message_tail = message_tail} end end; diff -r bcb84750eca5 -r 18bb3e1ff6f6 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Aug 01 14:43:57 2014 +0200 @@ -21,11 +21,9 @@ val binary_min_facts : int Config.T val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int -> - Proof.state -> thm -> (proof_method * play_outcome) Lazy.lazy option -> - ((string * stature) * thm list) list -> + Proof.state -> thm -> ((string * stature) * thm list) list -> ((string * stature) * thm list) list option - * ((proof_method * play_outcome) Lazy.lazy * ((proof_method * play_outcome) -> string) - * string) + * (((proof_method * 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 -> @@ -104,8 +102,7 @@ val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)]} - val result as {outcome, used_facts, run_time, ...} = - prover params (K (K (K ""))) problem + val result as {outcome, used_facts, run_time, ...} = prover params (K (K (K ""))) problem in print silent (fn () => (case outcome of @@ -194,7 +191,7 @@ end fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal - preplay0 facts = + facts = let val ctxt = Proof.context_of state val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name @@ -212,7 +209,7 @@ val min = if length facts >= Config.get ctxt binary_min_facts then binary_minimize else linear_minimize - val (min_facts, {preplay, message, message_tail, ...}) = + val (min_facts, {message, message_tail, ...}) = min test (new_timeout timeout run_time) result facts in print silent (fn () => cat_lines @@ -221,41 +218,38 @@ 0 => "" | n => "\n(including " ^ string_of_int n ^ " chained)") ^ "."); (if learn then do_learn (maps snd min_facts) else ()); - (SOME min_facts, - (if is_some preplay0 andalso length min_facts = length facts then the preplay0 - else preplay, - message, message_tail)) + (SOME min_facts, (message, message_tail)) end - | {outcome = SOME TimedOut, preplay, ...} => - (NONE, (preplay, fn _ => + | {outcome = SOME TimedOut, ...} => + (NONE, (fn _ => "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 (Metis_Method (NONE, NONE), Play_Failed), fn _ => "Error: " ^ msg, "")) + | {message, ...} => (NONE, (prefix "Prover error: " o message, "")))) + handle ERROR msg => (NONE, (fn _ => "Error: " ^ msg, "")) end fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...}) ({state, goal, subgoal, subgoal_count, ...} : prover_problem) - (result as {outcome, used_facts, used_from, run_time, preplay, message, message_tail} : - prover_result) = + (result as {outcome, used_facts, used_from, preferred_methss, run_time, message, message_tail} + : prover_result) = if is_some outcome orelse null used_facts then result else let - val (used_facts, (preplay, message, _)) = + val (used_facts, (message, _)) = if minimize then minimize_facts do_learn 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)) + goal (filter_used_facts true used_facts (map (apsnd single) used_from)) |>> Option.map (map fst) else - (SOME used_facts, (preplay, message, "")) + (SOME used_facts, (message, "")) in (case used_facts of SOME used_facts => - {outcome = NONE, used_facts = used_facts, used_from = used_from, run_time = run_time, - preplay = preplay, message = message, message_tail = message_tail} + {outcome = NONE, used_facts = used_facts, used_from = used_from, + preferred_methss = preferred_methss, run_time = run_time, message = message, + message_tail = message_tail} | NONE => result) end @@ -278,9 +272,10 @@ [] => error "No prover is set." | prover :: _ => (kill_provers (); - minimize_facts do_learn prover params false i n state goal NONE facts - |> (fn (_, (preplay, message, message_tail)) => - Output.urgent_message (message (Lazy.force preplay) ^ message_tail))))) + minimize_facts do_learn prover params false i n state goal facts + |> (fn (_, (message, message_tail)) => + Output.urgent_message (message (Metis_Method (NONE, NONE), + Play_Timed_Out Time.zeroTime) ^ message_tail))))) end end; diff -r bcb84750eca5 -r 18bb3e1ff6f6 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200 @@ -192,34 +192,36 @@ val used_facts = map fst used_named_facts val outcome = Option.map failure_of_smt2_failure outcome - val (preplay, message, message_tail) = + val (preferred_methss, message, message_tail) = (case outcome of NONE => - (Lazy.lazy (fn () => - play_one_line_proof mode preplay_timeout used_named_facts state subgoal SMT2_Method - (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)), - fn preplay => - let - val _ = if verbose then Output.urgent_message "Generating proof text..." else () + let + val preferred_methss = + (SMT2_Method, bunches_of_proof_methods (smt_proofs <> SOME false) false liftingN) + in + (preferred_methss, + fn preplay => + let + val _ = if verbose then Output.urgent_message "Generating proof text..." else () - fun isar_params () = - (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (), - goal) + fun isar_params () = + (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (), + goal) - val one_line_params = - (preplay, proof_banner mode name, used_facts, minimize_command [] name, subgoal, - subgoal_count) - val num_chained = length (#facts (Proof.goal state)) - in - proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params - end, - if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "") - | SOME failure => - (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), - fn _ => string_of_atp_failure failure, "")) + val one_line_params = + (preplay, proof_banner mode name, used_facts, minimize_command [] name, subgoal, + subgoal_count) + val num_chained = length (#facts (Proof.goal state)) + in + proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params + end, + if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "") + end + | SOME failure => ((Auto_Method (* dummy *), []), 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, + preferred_methss = preferred_methss, run_time = run_time, message = message, + message_tail = message_tail} end end;