--- 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
--- 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
--- 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 =
--- 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;
--- 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;
--- 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;