# HG changeset patch
# User desharna
# Date 1601626730 -7200
# Node ID 1f959abe99d5f1dc02ed7217357f0cf4bcd2753f
# Parent  2d36c214f7fd23d22a4c5b227013ad09db662740
Add more tacing to sledgehammer_isar_trace

diff -r 2d36c214f7fd -r 1f959abe99d5 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Oct 01 17:21:47 2020 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Oct 02 10:18:50 2020 +0200
@@ -139,6 +139,7 @@
   val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type)
   val is_format_higher_order : atp_format -> bool
   val tptp_string_of_format : atp_format -> string
+  val tptp_string_of_role : atp_formula_role -> string
   val tptp_string_of_line : atp_format -> string atp_problem_line -> string
   val lines_of_atp_problem :
     atp_format -> term_order -> (unit -> (string * int) list)
diff -r 2d36c214f7fd -r 1f959abe99d5 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Oct 01 17:21:47 2020 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Oct 02 10:18:50 2020 +0200
@@ -98,6 +98,7 @@
     ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
   val vampire_step_name_ord : (string * 'a) ord
   val core_of_agsyhol_proof :  string -> string list option
+  val string_of_atp_step : ('a -> string) -> ('b -> string) -> ('a, 'b) atp_step -> string
 end;
 
 structure ATP_Proof : ATP_PROOF =
@@ -722,4 +723,19 @@
 fun nasty_atp_proof pool =
   not (Symtab.is_empty pool) ? map_term_names_in_atp_proof (nasty_name pool)
 
+fun string_of_list f xs = enclose "[" "]" (commas (map f xs))
+
+fun string_of_atp_step_name (s, ss) = "(" ^ s ^ ", " ^ string_of_list I ss ^ ")"
+
+fun string_of_atp_step f g (name, role, x, y, names) =
+  let
+    val name' = string_of_atp_step_name name
+    val role' = ATP_Problem.tptp_string_of_role role
+    val x' = f x
+    val y' = g y
+    val names' = string_of_list string_of_atp_step_name names
+  in
+    "(" ^ name' ^ ", " ^ role' ^ ", " ^ x' ^ ", " ^ y' ^ ", " ^ names' ^ ")"
+  end
+
 end;
diff -r 2d36c214f7fd -r 1f959abe99d5 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Oct 01 17:21:47 2020 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Oct 02 10:18:50 2020 +0200
@@ -254,7 +254,7 @@
   in replay ctxt replay_data output end
 
 
-(* filter *)
+(* filter (for Sledgehammer) *)
 
 fun smt_filter ctxt0 goal xfacts i time_limit =
   let
diff -r 2d36c214f7fd -r 1f959abe99d5 src/HOL/Tools/SMT/z3_isar.ML
--- a/src/HOL/Tools/SMT/z3_isar.ML	Thu Oct 01 17:21:47 2020 +0200
+++ b/src/HOL/Tools/SMT/z3_isar.ML	Fri Oct 02 10:18:50 2020 +0200
@@ -76,7 +76,7 @@
 fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
     conjecture_id fact_helper_ids proof =
   let
-    fun steps_of (Z3_Proof.Z3_Step {id, rule, prems, concl, ...}) =
+    fun steps_of (Z3_Proof.Z3_Step {id, rule, prems, concl, ...}) : (term, string) ATP_Proof.atp_step list =
       let
         val sid = string_of_int id
 
@@ -92,7 +92,7 @@
           let val ss = the_list (AList.lookup (op =) fact_helper_ids id) in
             (case distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts
                 hyp_ts concl_t of
-              NONE => []
+              NONE => [] (* useless nontheory tautology *)
             | SOME (role0, concl00) =>
               let
                 val name0 = (sid ^ "a", ss)
diff -r 2d36c214f7fd -r 1f959abe99d5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Oct 01 17:21:47 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 02 10:18:50 2020 +0200
@@ -183,9 +183,18 @@
             fun get_role keep_role ((num, _), role, t, rule, _) =
               if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
 
-            val atp_proof =
-              fold_rev add_line_pass1 atp_proof0 []
+            val trace = Config.get ctxt trace
+
+            val string_of_atp_steps =
+              let val to_string = ATP_Proof.string_of_atp_step (Syntax.string_of_term ctxt) I in
+                enclose "[\n" "\n]" o cat_lines o map (enclose "  " "," o to_string)
+              end
+
+            val atp_proof = atp_proof0
+              |> trace ? tap (tracing o prefix "atp_proof0 = " o string_of_atp_steps)
+              |> (fn x => fold_rev add_line_pass1 x [])
               |> add_lines_pass2 []
+              |> trace ? tap (tracing o prefix "atp_proof = " o string_of_atp_steps)
 
             val conjs =
               map_filter (fn (name, role, _, _, _) =>
@@ -358,8 +367,6 @@
               Proof (fix, assms,
                 fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs))
 
-            val trace = Config.get ctxt trace
-
             val canonical_isar_proof =
               refute_graph
               |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph)
@@ -461,7 +468,7 @@
         (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else ""))
   end
 
-fun isar_proof_would_be_a_good_idea (meth, play) =
+fun isar_proof_would_be_a_good_idea (_, play) =
   (case play of
     Played _ => false
   | Play_Timed_Out time => time > Time.zeroTime