--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Mon May 06 11:03:08 2013 +0200
@@ -11,7 +11,7 @@
type preplay_time = Sledgehammer_Preplay.preplay_time
val compress_and_preplay_proof :
bool -> Proof.context -> string -> string -> bool -> Time.time option
- -> real -> isar_proof -> isar_proof * (bool * preplay_time)
+ -> bool -> real -> isar_proof -> isar_proof * (bool * preplay_time)
end
structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS =
@@ -48,7 +48,7 @@
(* Main function for compresing proofs *)
fun compress_and_preplay_proof debug ctxt type_enc lam_trans preplay
- preplay_timeout isar_compress proof =
+ preplay_timeout preplay_trace isar_compress proof =
let
(* 60 seconds seems like a good interpreation of "no timeout" *)
val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
@@ -103,7 +103,7 @@
cons (Term.size_of_term t, i)
| (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) =>
cons (Term.size_of_term t, i)
- | _ => I)
+ | _ => I)
handle Option => raise Fail "sledgehammer_compress: add_if_cand")
| add_if_cand _ _ = I
val cand_tab =
@@ -116,7 +116,8 @@
(if not preplay then K (zero_preplay_time) #> Lazy.value
else
the
- #> try_metis debug type_enc lam_trans ctxt preplay_timeout
+ #> try_metis debug preplay_trace type_enc lam_trans ctxt
+ preplay_timeout
#> handle_metis_fail
#> Lazy.lazy)
step_vect
@@ -156,8 +157,8 @@
val s12 = merge s1 s2
val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
in
- case try_metis_quietly debug type_enc lam_trans
- ctxt timeout s12 () of
+ case try_metis_quietly debug preplay_trace type_enc
+ lam_trans ctxt timeout s12 () of
(true, _) => (NONE, metis_time)
| exact_time =>
(SOME s12, metis_time
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 06 11:03:08 2013 +0200
@@ -98,7 +98,8 @@
("isar_compress", "10"),
("slice", "true"),
("minimize", "smart"),
- ("preplay_timeout", "3")]
+ ("preplay_timeout", "3"),
+ ("preplay_trace", "false")] (* TODO: document *)
val alias_params =
[("prover", ("provers", [])), (* undocumented *)
@@ -114,12 +115,14 @@
("dont_learn", "learn"),
("no_isar_proofs", "isar_proofs"),
("dont_slice", "slice"),
- ("dont_minimize", "minimize")]
+ ("dont_minimize", "minimize"),
+ ("no_preplay_trace", "preplay_trace")] (* TODO: document *)
val params_for_minimize =
["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
"uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
"learn", "isar_proofs", "isar_compress", "timeout", "preplay_timeout"]
+(* TODO: add preplay_trace? *)
val property_dependent_params = ["provers", "timeout"]
@@ -308,6 +311,7 @@
val preplay_timeout =
if mode = Auto_Try then SOME Time.zeroTime
else lookup_time "preplay_timeout"
+ val preplay_trace = lookup_bool "preplay_trace"
val expect = lookup_string "expect"
in
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
@@ -317,7 +321,8 @@
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
isar_compress = isar_compress, slice = slice, minimize = minimize,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ timeout = timeout, preplay_timeout = preplay_timeout,
+ preplay_trace = preplay_trace, expect = expect}
end
fun get_params mode = extract_params mode o default_raw_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 06 11:03:08 2013 +0200
@@ -57,7 +57,7 @@
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
max_new_mono_instances, type_enc, strict, lam_trans,
uncurried_aliases, isar_proofs, isar_compress,
- preplay_timeout, ...} : params)
+ preplay_timeout, preplay_trace, ...} : params)
silent (prover : prover) timeout i n state facts =
let
val _ =
@@ -80,7 +80,8 @@
max_new_mono_instances = max_new_mono_instances,
isar_proofs = isar_proofs, isar_compress = isar_compress,
slice = false, minimize = SOME false, timeout = timeout,
- preplay_timeout = preplay_timeout, expect = ""}
+ preplay_timeout = preplay_timeout, preplay_trace = preplay_trace,
+ expect = ""}
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
factss = [("", facts)]}
@@ -250,8 +251,8 @@
({debug, verbose, overlord, blocking, provers, type_enc, strict,
lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
- isar_compress, slice, minimize, timeout, preplay_timeout, expect}
- : params) =
+ isar_compress, slice, minimize, timeout, preplay_timeout,
+ preplay_trace, expect} : params) =
let
fun lookup_override name default_value =
case AList.lookup (op =) override_params name of
@@ -269,7 +270,8 @@
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
isar_compress = isar_compress, slice = slice, minimize = minimize,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ timeout = timeout, preplay_timeout = preplay_timeout,
+ preplay_trace = preplay_trace, expect = expect}
end
fun maybe_minimize ctxt mode do_learn name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon May 06 11:03:08 2013 +0200
@@ -13,9 +13,9 @@
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 try_metis : bool -> string -> string -> Proof.context ->
+ val try_metis : bool -> bool -> string -> string -> Proof.context ->
Time.time -> isar_step -> unit -> preplay_time
- val try_metis_quietly : bool -> string -> string -> Proof.context ->
+ val try_metis_quietly : bool -> bool -> string -> string -> Proof.context ->
Time.time -> isar_step -> unit -> preplay_time
end
@@ -38,6 +38,24 @@
val string_of_preplay_time = ATP_Util.string_from_ext_time
+(* preplay tracing *)
+fun preplay_trace ctxt assms concl time =
+ let
+ val ctxt = ctxt |> Config.put show_markup true
+ val time = "[" ^ (string_of_preplay_time time) ^ "]" |> Pretty.str
+ val nr_of_assms = length assms
+ val assms = assms |> map (Display.pretty_thm ctxt)
+ |> (fn [] => Pretty.str ""
+ | [a] => a
+ | assms => Pretty.enum ";" "⟦" "⟧" assms)
+ val concl = concl |> Syntax.pretty_term ctxt
+ val trace_list = [] |> cons concl
+ |> nr_of_assms>0 ? cons (Pretty.str "⟹")
+ |> cons assms
+ |> cons time
+ val pretty_trace = Pretty.blk(2, Pretty.breaks trace_list)
+ in tracing (Pretty.string_of pretty_trace) end
+
(* timing *)
fun take_time timeout tac arg =
let
@@ -56,9 +74,9 @@
|> maps (thms_of_name ctxt))
handle ERROR msg => error ("preplay error: " ^ msg)
-(* *)
+(* turn terms/proofs into theorems *)
fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
-fun fact_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) =
+fun thm_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) =
let
val concl = (case try List.last steps of
SOME (Prove (_, _, t, _)) => t
@@ -74,9 +92,9 @@
end
exception ZEROTIME
-fun try_metis debug type_enc lam_trans ctxt timeout step =
+fun try_metis debug trace type_enc lam_trans ctxt timeout step =
let
- val (t, subproofs, fact_names, obtain) =
+ val (prop, subproofs, fact_names, obtain) =
(case step of
Prove (_, _, t, By_Metis (subproofs, fact_names)) =>
(t, subproofs, fact_names, false)
@@ -100,22 +118,30 @@
end
| _ => raise ZEROTIME)
val facts =
- map (fact_of_proof ctxt) subproofs @
- resolve_fact_names ctxt fact_names
+ map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
|> obtain ? Config.put Metis_Tactic.new_skolem true
val goal =
- Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
+ Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop
fun tac {context = ctxt, prems = _} =
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
+ fun run_tac () = goal tac
+ handle ERROR msg => error ("preplay error: " ^ msg)
in
- take_time timeout
- (fn () => goal tac handle ERROR msg => error ("preplay error: " ^ msg))
+ fn () =>
+ let
+ val preplay_time = take_time timeout run_tac ()
+ (* tracing *)
+ val _ = if trace then preplay_trace ctxt facts prop preplay_time else ()
+ in
+ preplay_time
+ end
end
handle ZEROTIME => K zero_preplay_time
(* this version treats exceptions like timeouts *)
-fun try_metis_quietly debug type_enc lam_trans ctxt timeout =
- the_default (true, timeout) oo try o try_metis debug type_enc lam_trans ctxt timeout
+fun try_metis_quietly debug trace type_enc lam_trans ctxt timeout =
+ the_default (true, timeout) oo try
+ o try_metis debug trace type_enc lam_trans ctxt timeout
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 06 11:03:08 2013 +0200
@@ -40,6 +40,7 @@
minimize : bool option,
timeout : Time.time option,
preplay_timeout : Time.time option,
+ preplay_trace : bool,
expect : string}
type relevance_fudge =
@@ -348,6 +349,7 @@
minimize : bool option,
timeout : Time.time option,
preplay_timeout : Time.time option,
+ preplay_trace : bool,
expect : string}
type relevance_fudge =
@@ -668,7 +670,7 @@
(params as {debug, verbose, overlord, type_enc, strict, lam_trans,
uncurried_aliases, fact_filter, max_facts, max_mono_iters,
max_new_mono_instances, isar_proofs, isar_compress,
- slice, timeout, preplay_timeout, ...})
+ slice, timeout, preplay_timeout, preplay_trace, ...})
minimize_command
({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
@@ -940,7 +942,7 @@
else
()
val isar_params =
- (debug, verbose, preplay_timeout, isar_compress,
+ (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
pool, fact_names, sym_tab, atp_proof, goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon May 06 11:03:08 2013 +0200
@@ -23,7 +23,7 @@
type one_line_params =
play * string * (string * stature) list * minimize_command * int * int
type isar_params =
- bool * bool * Time.time option * real * string Symtab.table
+ bool * bool * Time.time option * bool * real * string Symtab.table
* (string * stature) list vector * int Symtab.table * string proof * thm
val smtN : string
@@ -631,12 +631,12 @@
in chain_proof end
type isar_params =
- bool * bool * Time.time option * real * string Symtab.table
+ bool * bool * Time.time option * bool * real * string Symtab.table
* (string * stature) list vector * int Symtab.table * string proof * thm
fun isar_proof_text ctxt isar_proofs
- (debug, verbose, preplay_timeout, isar_compress, pool, fact_names, sym_tab,
- atp_proof, goal)
+ (debug, verbose, preplay_timeout, preplay_trace, isar_compress, pool,
+ fact_names, sym_tab, atp_proof, goal)
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
@@ -792,7 +792,7 @@
rpair (false, (true, seconds 0.0))
else
compress_and_preplay_proof debug ctxt type_enc lam_trans preplay
- preplay_timeout
+ preplay_timeout preplay_trace
(if isar_proofs = SOME true then isar_compress else 1000.0))
|>> clean_up_labels_in_proof
val isar_text =