# HG changeset patch
# User smolkas
# Date 1367830988 -7200
# Node ID ee9562d317780987b1abd87bb659d6ccf42e4615
# Parent  f11039b31bae22e905feb08e98f88487550e297a
added preplay tracing

diff -r f11039b31bae -r ee9562d31778 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- 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
diff -r f11039b31bae -r ee9562d31778 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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
diff -r f11039b31bae -r ee9562d31778 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- 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
diff -r f11039b31bae -r ee9562d31778 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- 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
diff -r f11039b31bae -r ee9562d31778 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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,
diff -r f11039b31bae -r ee9562d31778 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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 =