--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 16:26:43 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 16:41:54 2014 +0100
@@ -342,39 +342,49 @@
and isar_proof outer fix assms lems infs =
Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
- val (preplay_data as {overall_preplay_outcome, ...}, isar_proof) =
+ val string_of_isar_proof =
+ string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count
+
+ val trace = false
+
+ val isar_proof =
refute_graph
-(*
- |> tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
-*)
+ |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
|> redirect_graph axioms tainted bot
-(*
- |> tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
-*)
+ |> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
|> isar_proof true params assms lems
|> postprocess_isar_proof_remove_unreferenced_steps I
|> relabel_isar_proof_canonically
- |> `(preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
- preplay_timeout)
+
+ val preplay_data as {overall_preplay_outcome, ...} =
+ preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
+ preplay_timeout isar_proof
+
+ fun trace_isar_proof label proof =
+ if trace then
+ tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof proof ^ "\n")
+ else
+ ()
val (play_outcome, isar_proof) =
isar_proof
+ |> tap (trace_isar_proof "Original")
|> compress_isar_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
preplay_data
+ |> tap (trace_isar_proof "Compressed")
|> try0_isar ? try0_isar_proof preplay_timeout preplay_data
+ |> tap (trace_isar_proof "Tried0")
|> postprocess_isar_proof_remove_unreferenced_steps
(try0_isar ? minimize_isar_step_dependencies preplay_data)
+ |> tap (trace_isar_proof "Minimized")
|> `overall_preplay_outcome
||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
-
- val isar_text =
- string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
in
- (case isar_text of
+ (case string_of_isar_proof isar_proof of
"" =>
if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
else ""
- | _ =>
+ | isar_text =>
let
val msg =
(if verbose then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 16:26:43 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 16:41:54 2014 +0100
@@ -204,7 +204,7 @@
| with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
val using_facts = with_facts "" (enclose "using " " ")
- fun by_facts meth ls ss = "by " ^ with_facts meth (enclose ("by (" ^ meth) ")") ls ss
+ fun by_facts meth ls ss = "by " ^ with_facts meth (enclose ("(" ^ meth ^ " ") ")") ls ss
(* Local facts are always passed via "using", which affects "meson" and "metis". This is
arguably stylistically superior, because it emphasises the structure of the proof. It is also