--- 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
@@ -61,15 +61,16 @@
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)
+ (used_facts,
+ (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 fact_names = used_facts |> map fst |> sort string_ord
val {context = ctxt, facts = chained, goal} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
@@ -77,9 +78,9 @@
fun try_methss [] = dont_know ()
| try_methss (meths :: methss) =
- let val step = Prove ([], [], ("", 0), goal_t, [], ([], facts), meths, "") in
+ let val step = Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") in
(case preplay_isar_step ctxt timeout [] step of
- (res as (_, Played _)) :: _ => res
+ (res as (_, Played _)) :: _ => (used_facts, res)
| _ => try_methss methss)
end
in
@@ -157,12 +158,11 @@
print_used_facts used_facts used_from
| _ => ())
|> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
- |> (fn {outcome, used_facts, used_from, preferred_methss, message, ...} =>
+ |> (fn {outcome, used_facts, preferred_methss, message, ...} =>
(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
+ fn () => message (play_one_line_proof mode preplay_timeout used_facts state subgoal
preferred_methss)))
fun go () =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 14:43:57 2014 +0200
@@ -127,7 +127,7 @@
val skolem_methods = basic_systematic_methods
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
- (one_line_params as ((_, one_line_play), banner, used_facts, subgoal, subgoal_count)) =
+ (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
let
val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
@@ -351,7 +351,7 @@
(case isar_proof of
Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
let val used_facts' = filter (member (op =) gfs o fst) used_facts in
- ((meth, play_outcome), banner, used_facts', subgoal, subgoal_count)
+ ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
end)
else
one_line_params) ^
@@ -387,7 +387,7 @@
| Play_Failed => true)
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
- (one_line_params as (preplay, _, _, _, _)) =
+ (one_line_params as ((_, preplay), _, _, _)) =
(if isar_proofs = SOME true orelse
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Aug 01 14:43:57 2014 +0200
@@ -43,15 +43,15 @@
fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
- fun minimize_facts _ min_facts [] time = (min_facts, time)
- | minimize_facts mk_step min_facts (fact :: facts) time =
+ fun minimize_half _ min_facts [] time = (min_facts, time)
+ | minimize_half mk_step min_facts (fact :: facts) time =
(case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth
(mk_step (min_facts @ facts)) of
- Played time' => minimize_facts mk_step min_facts facts time'
- | _ => minimize_facts mk_step (fact :: min_facts) facts time)
+ Played time' => minimize_half mk_step min_facts facts time'
+ | _ => minimize_half mk_step (fact :: min_facts) facts time)
- val (min_lfs, time') = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time
- val (min_gfs, time'') = minimize_facts (mk_step_lfs_gfs min_lfs) [] gfs0 time'
+ val (min_lfs, time') = minimize_half (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time
+ val (min_gfs, time'') = minimize_half (mk_step_lfs_gfs min_lfs) [] gfs0 time'
in
(time'', mk_step_lfs_gfs min_lfs min_gfs)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Aug 01 14:43:57 2014 +0200
@@ -30,7 +30,7 @@
Play_Failed
type one_line_params =
- (proof_method * play_outcome) * string * (string * stature) list * int * int
+ ((string * stature) list * (proof_method * play_outcome)) * string * int * int
val is_proof_method_direct : proof_method -> bool
val string_of_proof_method : Proof.context -> string list -> proof_method -> string
@@ -68,7 +68,8 @@
Play_Timed_Out of Time.time |
Play_Failed
-type one_line_params = (proof_method * play_outcome) * string * (string * stature) list * int * int
+type one_line_params =
+ ((string * stature) list * (proof_method * play_outcome)) * string * int * int
fun is_proof_method_direct (Metis_Method _) = true
| is_proof_method_direct Meson_Method = true
@@ -182,7 +183,7 @@
|> pairself (sort_distinct (string_ord o pairself fst))
fun one_line_proof_text ctxt num_chained
- ((meth, play), banner, used_facts, subgoal, subgoal_count) =
+ ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
let val (chained, extra) = split_used_facts used_facts in
map fst extra
|> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
--- 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
@@ -58,7 +58,7 @@
used_from : fact list,
preferred_methss : proof_method * proof_method list list,
run_time : Time.time,
- message : proof_method * play_outcome -> string}
+ message : (string * stature) list * (proof_method * play_outcome) -> string}
type prover = params -> prover_problem -> prover_result
@@ -149,7 +149,7 @@
used_from : fact list,
preferred_methss : proof_method * proof_method list list,
run_time : Time.time,
- message : proof_method * play_outcome -> string}
+ message : (string * stature) list * (proof_method * play_outcome) -> string}
type prover = params -> prover_problem -> prover_result
--- 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
@@ -385,8 +385,7 @@
minimize, atp_proof, goal)
end
- val one_line_params =
- (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count)
+ val one_line_params = (preplay, proof_banner mode 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
--- 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
@@ -22,7 +22,8 @@
val binary_min_facts : int Config.T
val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
Proof.state -> thm -> ((string * stature) * thm list) list ->
- ((string * stature) * thm list) list option * ((proof_method * play_outcome) -> string)
+ ((string * stature) * thm list) list option
+ * (((string * stature) list * (proof_method * play_outcome)) -> string)
val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
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
@@ -208,8 +208,7 @@
(verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
goal)
- val one_line_params =
- (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count)
+ val one_line_params = (preplay, proof_banner mode 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