avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Feb 13 13:16:17 2014 +0100
@@ -231,7 +231,6 @@
val _ = Proof.assert_backward state
val print =
if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
- val state = state |> Proof.map_context (silence_proof_methods debug)
val ctxt = Proof.context_of state
val {facts = chained, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 13 13:16:17 2014 +0100
@@ -290,7 +290,7 @@
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
val _ = fold_isar_steps (fn meth =>
- K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
+ K (set_preplay_outcomes_of_isar_step ctxt debug 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 compress_isar preplay_timeout preplay_data
+ |> compress_isar_proof ctxt debug 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 preplay_data)
+ #> minimize ? minimize_isar_step_dependencies ctxt debug 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 Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu Feb 13 13:16:17 2014 +0100
@@ -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 -> real -> Time.time ->
+ val compress_isar_proof : Proof.context -> bool -> 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 compress_isar preplay_timeout preplay_data proof =
+fun compress_isar_proof ctxt debug compress_isar preplay_timeout preplay_data proof =
if compress_isar <= 1.0 then
proof
else
@@ -172,11 +172,12 @@
(* 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 timeout hopeless step'' of
+ (case preplay_isar_step ctxt debug timeout hopeless step'' of
meths_outcomes as (_, Played time'') :: _ =>
(* l' successfully eliminated *)
(decrement_step_count ();
- set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes;
+ set_preplay_outcomes_of_isar_step ctxt debug 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))
@@ -215,14 +216,16 @@
val time_slice = time_mult (1.0 / Real.fromInt (length labels)) (reference_time l)
val timeouts =
map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0
- val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs'
+ val meths_outcomess =
+ map3 (preplay_isar_step ctxt debug) 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 time preplay_data)
+ map3 (fn time =>
+ set_preplay_outcomes_of_isar_step ctxt debug 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 Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu Feb 13 13:16:17 2014 +0100
@@ -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 -> isar_preplay_data Unsynchronized.ref ->
- isar_step -> isar_step
+ val minimize_isar_step_dependencies : Proof.context -> bool ->
+ 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 preplay_data
+fun minimize_isar_step_dependencies ctxt debug 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 (Time.+ (time, slack)) meth
+ (case preplay_isar_step_for_method ctxt debug (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,11 +53,12 @@
val step' = mk_step_lfs_gfs min_lfs min_gfs
in
- set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step' [(meth, Played time'')];
+ set_preplay_outcomes_of_isar_step ctxt debug 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 Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Feb 13 13:16:17 2014 +0100
@@ -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 -> Time.time -> proof_method -> isar_step ->
- play_outcome
- val preplay_isar_step : Proof.context -> Time.time -> proof_method list -> isar_step ->
+ 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 ->
(proof_method * play_outcome) list
- val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
+ val set_preplay_outcomes_of_isar_step : Proof.context -> bool -> 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,7 +101,8 @@
end
(* may throw exceptions *)
-fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) =
+fun raw_preplay_step_for_method ctxt debug timeout meth
+ (Prove (_, xs, _, t, subproofs, facts, _, _)) =
let
val goal =
(case xs of
@@ -128,7 +129,7 @@
fun prove () =
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
- HEADGOAL (tac_of_proof_method ctxt assmsp meth))
+ HEADGOAL (tac_of_proof_method ctxt debug assmsp meth))
handle ERROR msg => error ("Preplay error: " ^ msg)
val play_outcome = take_time timeout prove ()
@@ -137,13 +138,13 @@
play_outcome
end
-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_for_method ctxt debug timeout meth =
+ try (raw_preplay_step_for_method ctxt debug timeout meth) #> the_default Play_Failed
-fun preplay_isar_step ctxt timeout hopeless step =
+fun preplay_isar_step ctxt debug timeout hopeless step =
let
fun try_method meth =
- (case preplay_isar_step_for_method ctxt timeout meth step of
+ (case preplay_isar_step_for_method ctxt debug timeout meth step of
outcome as Played _ => SOME (meth, outcome)
| _ => NONE)
@@ -163,11 +164,11 @@
| add_preplay_outcomes play1 play2 =
Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
-fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
+fun set_preplay_outcomes_of_isar_step ctxt debug timeout preplay_data
(step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
let
fun lazy_preplay meth =
- Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
+ Lazy.lazy (fn () => preplay_isar_step_for_method ctxt debug timeout meth step)
val meths_outcomes = meths_outcomes0
|> map (apsnd Lazy.value)
|> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
@@ -175,7 +176,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 Not_Played
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Feb 13 13:16:17 2014 +0100
@@ -34,11 +34,11 @@
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
val string_of_proof_method : proof_method -> string
- val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
+ val tac_of_proof_method : Proof.context -> bool -> 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 : int -> one_line_params -> string
- val silence_proof_methods : bool -> Proof.context -> Proof.context
end;
structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
@@ -89,27 +89,36 @@
| Presburger_Method => "presburger"
| Algebra_Method => "algebra")
-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) =>
- Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
- (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
- | Meson_Method => Meson.meson_tac ctxt global_facts
- | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
- | _ =>
- Method.insert_tac global_facts THEN'
+(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
+ exceeded" warnings and the like. *)
+fun silence_proof_methods debug =
+ Try0.silence_methods debug
+ #> Config.put SMT_Config.verbose debug
+
+fun tac_of_proof_method ctxt0 debug (local_facts, global_facts) meth =
+ let val ctxt = silence_proof_methods debug ctxt0 in
+ Method.insert_tac local_facts THEN'
(case meth of
- Blast_Method => blast_tac ctxt
- | Simp_Method => Simplifier.asm_full_simp_tac ctxt
- | Simp_Size_Method =>
- Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
- | Auto_Method => K (Clasimp.auto_tac ctxt)
- | Fastforce_Method => Clasimp.fast_force_tac ctxt
- | Force_Method => Clasimp.force_tac ctxt
- | Linarith_Method => Lin_Arith.tac ctxt
- | Presburger_Method => Cooper.tac true [] [] ctxt
- | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
+ Metis_Method (type_enc_opt, lam_trans_opt) =>
+ Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
+ (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
+ | Meson_Method => Meson.meson_tac ctxt global_facts
+
+ | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
+ | _ =>
+ Method.insert_tac global_facts THEN'
+ (case meth of
+ Blast_Method => blast_tac ctxt
+ | Simp_Method => Simplifier.asm_full_simp_tac ctxt
+ | Simp_Size_Method =>
+ Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
+ | Auto_Method => K (Clasimp.auto_tac ctxt)
+ | Fastforce_Method => Clasimp.fast_force_tac ctxt
+ | Force_Method => Clasimp.force_tac ctxt
+ | Linarith_Method => Lin_Arith.tac ctxt
+ | Presburger_Method => Cooper.tac true [] [] ctxt
+ | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
+ end
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
| string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
@@ -189,10 +198,4 @@
try_line ^ minimize_line minimize_command (map fst (extra @ chained))
end
-(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
- exceeded" warnings and the like. *)
-fun silence_proof_methods debug =
- Try0.silence_methods debug
- #> Config.put SMT_Config.verbose debug
-
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Feb 13 13:16:17 2014 +0100
@@ -78,7 +78,7 @@
val filter_used_facts :
bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
((''a * stature) * 'b) list
- val play_one_line_proof : mode -> bool -> Time.time -> ((string * 'a) * thm) list ->
+ val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
val remotify_atp_if_not_installed : theory -> string -> string option
val isar_supported_prover_of : theory -> string -> string
@@ -219,15 +219,15 @@
TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
end
-fun timed_proof_method meth timeout ths =
- timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
+fun timed_proof_method debug timeout ths meth =
+ timed_apply timeout (fn ctxt => tac_of_proof_method ctxt debug ([], 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 verbose timeout pairs state i preferred (meths as meth :: _) =
+fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
let
fun get_preferred meths = if member (op =) meths preferred then preferred else meth
in
@@ -249,7 +249,7 @@
()
val timer = Timer.startRealTimer ()
in
- (case timed_proof_method meth timeout ths state i of
+ (case timed_proof_method debug 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 Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Feb 13 13:16:17 2014 +0100
@@ -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 verbose preplay_timeout used_pairs state subgoal (hd meths)
- meths
+ play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+ (hd meths) meths
end),
fn preplay =>
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu Feb 13 13:16:17 2014 +0100
@@ -50,7 +50,7 @@
open Sledgehammer_Prover_ATP
open Sledgehammer_Prover_SMT
-fun run_proof_method mode name (params as {verbose, timeout, type_enc, lam_trans, ...})
+fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
minimize_command
({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
let
@@ -60,8 +60,8 @@
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) verbose timeout facts state
- subgoal meth [meth] of
+ (case play_one_line_proof (if mode = Minimize then Normal else mode) debug 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,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Feb 13 13:16:17 2014 +0100
@@ -71,7 +71,7 @@
fun weight_smt_fact ctxt num_facts ((info, th), j) =
let val thy = Proof_Context.theory_of ctxt in
- (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
+ (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
end
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
@@ -212,7 +212,7 @@
do_slice timeout 1 NONE Time.zeroTime
end
-fun run_smt_solver mode name (params as {verbose, smt_proofs, preplay_timeout, ...})
+fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val thy = Proof.theory_of state
@@ -233,8 +233,8 @@
(case outcome of
NONE =>
(Lazy.lazy (fn () =>
- play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal SMT_Method
- (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
+ play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+ SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
val one_line_params =