--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Sep 20 22:39:30 2013 +0200
@@ -17,12 +17,11 @@
PplFail of exn |
PplSucc of preplay_time
+ val trace : bool Config.T
val zero_preplay_time : preplay_time
val some_preplay_time : preplay_time
val add_preplay_time : preplay_time -> preplay_time -> preplay_time
val string_of_preplay_time : preplay_time -> string
- (*val preplay_raw : bool -> bool -> string -> string -> Proof.context ->
- Time.time -> isar_step -> preplay_time*)
type preplay_interface =
{ get_preplay_result : label -> preplay_result,
@@ -34,9 +33,8 @@
overall_preplay_stats : isar_proof -> preplay_time * bool }
val proof_preplay_interface :
- bool -> Proof.context -> string -> string -> bool -> Time.time -> bool
+ bool -> Proof.context -> string -> string -> bool -> Time.time
-> isar_proof -> preplay_interface
-
end
structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
@@ -45,6 +43,9 @@
open Sledgehammer_Util
open Sledgehammer_Proof
+val trace =
+ Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
+
(* The boolean flag encodes whether the time is exact (false) or an lower bound
(true):
(t, false) = "t ms"
@@ -77,7 +78,7 @@
|> nr_of_assms>0 ? cons (Pretty.str "\<Longrightarrow>")
|> cons assms
|> cons time
- val pretty_trace = Pretty.blk(2, Pretty.breaks trace_list)
+ val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
in tracing (Pretty.string_of pretty_trace) end
(* timing *)
@@ -132,8 +133,8 @@
(* main function for preplaying isar_steps; may throw exceptions *)
-fun preplay_raw _ _ _ _ _ _ (Let _) = zero_preplay_time
- | preplay_raw debug trace type_enc lam_trans ctxt timeout
+fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time
+ | preplay_raw debug type_enc lam_trans ctxt timeout
(Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) =
let
val (prop, obtain) =
@@ -171,12 +172,12 @@
val preplay_time = take_time timeout run_tac ()
in
(* tracing *)
- (if trace then preplay_trace ctxt facts prop preplay_time else () ;
+ (if Config.get ctxt trace then preplay_trace ctxt facts prop preplay_time
+ else ();
preplay_time)
end
-
(*** proof preplay interface ***)
type preplay_interface =
@@ -216,13 +217,12 @@
The preplay results are caluclated lazyly and cached to avoid repeated
calculation.
- PRE CONDITION: the proof must be labeled canocially, see
+ PRECONDITION: the proof must be labeled canocially, see
Slegehammer_Proof.relabel_proof_canonically
*)
-
fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
- preplay_timeout preplay_trace proof : preplay_interface =
+ preplay_timeout proof : preplay_interface =
if not do_preplay then
(* the dont_preplay option pretends that everything works just fine *)
{ get_preplay_result = K (PplSucc zero_preplay_time),
@@ -238,7 +238,7 @@
val ctxt = enrich_context proof ctxt
fun preplay quietly timeout step =
- preplay_raw debug preplay_trace type_enc lam_trans ctxt timeout step
+ preplay_raw debug type_enc lam_trans ctxt timeout step
|> PplSucc
handle exn =>
if Exn.is_interrupt exn then