--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 22 03:29:36 2014 +0200
@@ -289,7 +289,7 @@
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
val _ = fold_isar_steps (fn meth =>
- K (set_preplay_outcomes_of_isar_step ctxt debug preplay_timeout preplay_data meth []))
+ K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
(steps_of_isar_proof canonical_isar_proof) ()
fun str_of_preplay_outcome outcome =
@@ -316,11 +316,11 @@
val (play_outcome, isar_proof) =
canonical_isar_proof
|> tap (trace_isar_proof "Original")
- |> compress_isar_proof ctxt debug compress_isar preplay_timeout preplay_data
+ |> compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
|> tap (trace_isar_proof "Compressed")
|> postprocess_isar_proof_remove_unreferenced_steps
(keep_fastest_method_of_isar_step (!preplay_data)
- #> minimize ? minimize_isar_step_dependencies ctxt debug preplay_data)
+ #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
|> tap (trace_isar_proof "Minimized")
(* It's not clear whether this is worth the trouble (and if so, "isar_compress" has an
unnatural semantics): *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu May 22 03:29:36 2014 +0200
@@ -11,7 +11,7 @@
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
- val compress_isar_proof : Proof.context -> bool -> real -> Time.time ->
+ val compress_isar_proof : Proof.context -> real -> Time.time ->
isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof
end;
@@ -109,7 +109,7 @@
val compress_degree = 2
(* Precondition: The proof must be labeled canonically. *)
-fun compress_isar_proof ctxt debug compress_isar preplay_timeout preplay_data proof =
+fun compress_isar_proof ctxt compress_isar preplay_timeout preplay_data proof =
if compress_isar <= 1.0 then
proof
else
@@ -172,12 +172,11 @@
(* check if the modified step can be preplayed fast enough *)
val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l'))
in
- (case preplay_isar_step ctxt debug timeout hopeless step'' of
+ (case preplay_isar_step ctxt timeout hopeless step'' of
meths_outcomes as (_, Played time'') :: _ =>
(* l' successfully eliminated *)
(decrement_step_count ();
- set_preplay_outcomes_of_isar_step ctxt debug time'' preplay_data step''
- meths_outcomes;
+ set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes;
map (replace_successor l' [l]) lfs';
elim_one_subproof time'' step'' subs nontriv_subs)
| _ => elim_one_subproof time step subs (sub :: nontriv_subs))
@@ -217,15 +216,14 @@
val timeouts =
map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0
val meths_outcomess =
- map3 (preplay_isar_step ctxt debug) timeouts hopelesses succs'
+ map3 (preplay_isar_step ctxt) timeouts hopelesses succs'
in
(case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
NONE => steps
| SOME times =>
(* candidate successfully eliminated *)
(decrement_step_count ();
- map3 (fn time =>
- set_preplay_outcomes_of_isar_step ctxt debug time preplay_data)
+ map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data)
times succs' meths_outcomess;
map (replace_successor l labels) lfs;
steps_before @ update_steps succs' steps_after))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu May 22 03:29:36 2014 +0200
@@ -12,8 +12,8 @@
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step
- val minimize_isar_step_dependencies : Proof.context -> bool ->
- isar_preplay_data Unsynchronized.ref -> isar_step -> isar_step
+ val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref ->
+ isar_step -> isar_step
val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
isar_proof
end;
@@ -34,7 +34,7 @@
val slack = seconds 0.025
-fun minimize_isar_step_dependencies ctxt debug preplay_data
+fun minimize_isar_step_dependencies ctxt preplay_data
(step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
Played time =>
@@ -43,7 +43,7 @@
fun minimize_facts _ min_facts [] time = (min_facts, time)
| minimize_facts mk_step min_facts (fact :: facts) time =
- (case preplay_isar_step_for_method ctxt debug (Time.+ (time, slack)) meth
+ (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)
@@ -53,12 +53,11 @@
val step' = mk_step_lfs_gfs min_lfs min_gfs
in
- set_preplay_outcomes_of_isar_step ctxt debug time'' preplay_data step'
- [(meth, Played time'')];
+ set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step' [(meth, Played time'')];
step'
end
| _ => step (* don't touch steps that time out or fail *))
- | minimize_isar_step_dependencies _ _ _ step = step
+ | minimize_isar_step_dependencies _ _ step = step
fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu May 22 03:29:36 2014 +0200
@@ -18,11 +18,11 @@
type isar_preplay_data
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
- val preplay_isar_step_for_method : Proof.context -> bool -> Time.time -> proof_method ->
- isar_step -> play_outcome
- val preplay_isar_step : Proof.context -> bool -> Time.time -> proof_method list -> isar_step ->
+ val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step ->
+ play_outcome
+ val preplay_isar_step : Proof.context -> Time.time -> proof_method list -> isar_step ->
(proof_method * play_outcome) list
- val set_preplay_outcomes_of_isar_step : Proof.context -> bool -> Time.time ->
+ val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit
val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method ->
@@ -101,8 +101,7 @@
end
(* may throw exceptions *)
-fun raw_preplay_step_for_method ctxt debug timeout meth
- (Prove (_, xs, _, t, subproofs, facts, _, _)) =
+fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) =
let
val goal =
(case xs of
@@ -129,7 +128,7 @@
fun prove () =
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
- HEADGOAL (tac_of_proof_method ctxt debug assmsp meth))
+ HEADGOAL (tac_of_proof_method ctxt assmsp meth))
handle ERROR msg => error ("Preplay error: " ^ msg)
val play_outcome = take_time timeout prove ()
@@ -138,13 +137,13 @@
play_outcome
end
-fun preplay_isar_step_for_method ctxt debug timeout meth =
- try (raw_preplay_step_for_method ctxt debug timeout meth) #> the_default Play_Failed
+fun preplay_isar_step_for_method ctxt timeout meth =
+ try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed
-fun preplay_isar_step ctxt debug timeout hopeless step =
+fun preplay_isar_step ctxt timeout hopeless step =
let
fun try_method meth =
- (case preplay_isar_step_for_method ctxt debug timeout meth step of
+ (case preplay_isar_step_for_method ctxt timeout meth step of
outcome as Played _ => SOME (meth, outcome)
| _ => NONE)
@@ -164,11 +163,11 @@
| add_preplay_outcomes play1 play2 =
Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
-fun set_preplay_outcomes_of_isar_step ctxt debug timeout preplay_data
+fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
(step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
let
fun lazy_preplay meth =
- Lazy.lazy (fn () => preplay_isar_step_for_method ctxt debug timeout meth step)
+ Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
val meths_outcomes = meths_outcomes0
|> map (apsnd Lazy.value)
|> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
@@ -176,7 +175,7 @@
preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes [])
(!preplay_data)
end
- | set_preplay_outcomes_of_isar_step _ _ _ _ _ _ = ()
+ | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
fun peek_at_outcome outcome =
if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu May 22 03:29:36 2014 +0200
@@ -34,8 +34,7 @@
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
val string_of_proof_method : Proof.context -> string list -> proof_method -> string
- val tac_of_proof_method : Proof.context -> bool -> thm list * thm list -> proof_method -> int ->
- tactic
+ val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
val string_of_play_outcome : play_outcome -> string
val play_outcome_ord : play_outcome * play_outcome -> order
val one_line_proof_text : Proof.context -> int -> one_line_params -> string
@@ -97,7 +96,7 @@
maybe_paren (space_implode " " (meth_s :: ss))
end
-fun tac_of_proof_method ctxt debug (local_facts, global_facts) meth =
+fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
Method.insert_tac local_facts THEN'
(case meth of
Metis_Method (type_enc_opt, lam_trans_opt) =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu May 22 03:29:36 2014 +0200
@@ -79,7 +79,7 @@
val filter_used_facts :
bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
((''a * stature) * 'b) list
- val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
+ val play_one_line_proof : mode -> bool -> Time.time -> ((string * 'a) * thm) list ->
Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
val isar_supported_prover_of : theory -> string -> string
val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
@@ -214,15 +214,15 @@
TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
end
-fun timed_proof_method debug timeout ths meth =
- timed_apply timeout (fn ctxt => tac_of_proof_method ctxt debug ([], ths) meth)
+fun timed_proof_method timeout ths meth =
+ timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
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 debug verbose timeout pairs state i preferred (meths as meth :: _) =
+fun play_one_line_proof mode verbose timeout pairs state i preferred (meths as meth :: _) =
let
val ctxt = Proof.context_of state
@@ -246,7 +246,7 @@
()
val timer = Timer.startRealTimer ()
in
- (case timed_proof_method debug timeout ths meth state i of
+ (case timed_proof_method timeout ths meth state i of
SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
| _ => play timed_out meths)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu May 22 03:29:36 2014 +0200
@@ -353,8 +353,8 @@
(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 meths) meths
+ play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal (hd meths)
+ meths
end),
fn preplay =>
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu May 22 03:29:36 2014 +0200
@@ -51,7 +51,7 @@
open Sledgehammer_Prover_SMT
open Sledgehammer_Prover_SMT2
-fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
+fun run_proof_method mode name (params as {verbose, timeout, type_enc, lam_trans, ...})
minimize_command
({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
let
@@ -61,23 +61,22 @@
else raise Fail ("unknown proof_method: " ^ quote name)
val used_facts = facts |> map fst
in
- (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout
- facts state subgoal meth [meth] of
+ (case play_one_line_proof (if mode = Minimize then Normal else mode) verbose timeout facts state
+ subgoal meth [meth] of
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 ctxt = Proof.context_of state
- val (_, override_params) = extract_proof_method params meth
- val one_line_params =
- (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 ctxt num_chained one_line_params
- end,
+ message = fn play =>
+ let
+ val ctxt = Proof.context_of state
+ val (_, override_params) = extract_proof_method params meth
+ val one_line_params =
+ (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 ctxt num_chained one_line_params
+ end,
message_tail = ""}
| play =>
let
@@ -128,10 +127,7 @@
fun n_facts names =
let val n = length names in
string_of_int n ^ " fact" ^ plural_s n ^
- (if n > 0 then
- ": " ^ (names |> map fst |> sort string_ord |> space_implode " ")
- else
- "")
+ (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
end
fun print silent f = if silent then () else Output.urgent_message (f ())
@@ -141,10 +137,9 @@
smt_proofs, preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state goal facts =
let
- val _ =
- print silent (fn () =>
- "Testing " ^ n_facts (map fst facts) ^
- (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
+ val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
+ (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
+
val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
val params =
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true,
@@ -230,7 +225,7 @@
(case test timeout (sup @ r0) of
result as {outcome = NONE, used_facts, ...} =>
min depth result (filter_used_facts true used_facts sup)
- (filter_used_facts true used_facts r0)
+ (filter_used_facts true used_facts r0)
| _ =>
let
val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
@@ -259,8 +254,8 @@
val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
fun test timeout = test_facts params silent prover timeout i n state goal
val (chained, non_chained) = List.partition is_fact_chained facts
- (* Push chained facts to the back, so that they are less likely to be
- kicked out by the linear minimization algorithm. *)
+ (* Push chained facts to the back, so that they are less likely to be kicked out by the linear
+ minimization algorithm. *)
val facts = non_chained @ chained
in
(print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ ".");
@@ -378,8 +373,7 @@
| NONE => result)
end
-fun get_minimizing_prover ctxt mode do_learn name params minimize_command
- problem =
+fun get_minimizing_prover ctxt mode do_learn name params minimize_command problem =
get_prover ctxt mode name params minimize_command problem
|> maybe_minimize ctxt mode do_learn name params problem
@@ -393,14 +387,14 @@
in
(case subgoal_count state of
0 => Output.urgent_message "No subgoal!"
- | n => (case provers of
- [] => 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)) =>
- message (Lazy.force preplay) ^ message_tail
- |> Output.urgent_message))))
+ | n =>
+ (case provers of
+ [] => 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)))))
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu May 22 03:29:36 2014 +0200
@@ -212,7 +212,7 @@
do_slice timeout 1 NONE Time.zeroTime
end
-fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
+fun run_smt_solver mode name (params as {verbose, smt_proofs, preplay_timeout, ...})
minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val thy = Proof.theory_of state
@@ -233,7 +233,7 @@
(case outcome of
NONE =>
(Lazy.lazy (fn () =>
- play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+ play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal
SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 03:29:36 2014 +0200
@@ -238,7 +238,7 @@
(case outcome of
NONE =>
(Lazy.lazy (fn () =>
- play_one_line_proof mode debug verbose preplay_timeout used_named_facts state subgoal
+ play_one_line_proof mode verbose preplay_timeout used_named_facts state subgoal
SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let