# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID ade5c84f860f78c365d94307fdd3650e77ea37fa
# Parent  0ef380310863f5f667f406d0baab8f7c4dfbbe25
cleanup proof text generation code

diff -r 0ef380310863 -r ade5c84f860f src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:08 2011 +0200
@@ -24,10 +24,11 @@
 
   type minimize_command = string list -> string
   type one_line_params =
-    preplay * string * (string * locality) list * minimize_command * thm * int
+    preplay * string * (string * locality) list * minimize_command * int * int
   type isar_params =
     bool * bool * int * type_system * string Symtab.table * int list list
     * int * (string * locality) list vector * int Symtab.table * string proof
+    * thm
   val repair_conjecture_shape_and_fact_names :
     type_system -> string -> int list list -> int
     -> (string * locality) list vector -> int list
@@ -39,15 +40,6 @@
     Proof.context -> type_system -> int list list -> int
     -> (string * locality) list vector -> 'a proof -> string list option
   val uses_typed_helpers : int list -> 'a proof -> bool
-  val reconstructor_name : reconstructor -> string
-  val reconstructor_settings : reconstructor -> string
-  val apply_on_subgoal : string -> int -> int -> string
-  val command_call : string -> string list -> string
-  val try_command_line : string -> (bool * Time.time) option -> string -> string
-  val minimize_line : ('a list -> string) -> 'a list -> string
-  val split_used_facts :
-    (string * locality) list
-    -> (string * locality) list * (string * locality) list
   val one_line_proof_text : one_line_params -> string
   val isar_proof_text :
     Proof.context -> isar_params -> one_line_params -> string
@@ -77,10 +69,10 @@
 
 type minimize_command = string list -> string
 type one_line_params =
-  preplay * string * (string * locality) list * minimize_command * thm * int
+  preplay * string * (string * locality) list * minimize_command * int * int
 type isar_params =
   bool * bool * int * type_system * string Symtab.table * int list list * int
-  * (string * locality) list vector * int Symtab.table * string proof
+  * (string * locality) list vector * int Symtab.table * string proof * thm
 
 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
@@ -291,7 +283,7 @@
   #> pairself (sort_distinct (string_ord o pairself fst))
 
 fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
-                         goal, i) =
+                         subgoal, subgoal_count) =
   let
     val (chained, extra) = split_used_facts used_facts
     val (reconstructor, ext_time) =
@@ -305,10 +297,10 @@
          | SOME time =>
            if time = Time.zeroTime then NONE else SOME (true, time))
       | Failed_to_Preplay => (NONE, NONE)
-    val n = Logic.count_prems (prop_of goal)
     val try_line =
       case reconstructor of
-        SOME r => reconstructor_command r i n ([], map fst extra)
+        SOME r => ([], map fst extra)
+                  |> reconstructor_command r subgoal subgoal_count
                   |> try_command_line banner ext_time
       | NONE => "Proof reconstruction failed."
   in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
@@ -1054,13 +1046,12 @@
 
 fun isar_proof_text ctxt
         (debug, full_types, isar_shrink_factor, type_sys, pool,
-         conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof)
-        (one_line_params as (_, _, _, _, goal, i)) =
+         conjecture_shape, facts_offset, 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 i
+    val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
-    val n = Logic.count_prems (prop_of goal)
     val one_line_proof = one_line_proof_text one_line_params
     fun isar_proof_for () =
       case atp_proof
@@ -1072,7 +1063,7 @@
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof
-           |> string_for_proof ctxt full_types i n of
+           |> string_for_proof ctxt full_types subgoal subgoal_count of
         "" => "\nNo structured proof available (proof too short)."
       | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
     val isar_proof =
diff -r 0ef380310863 -r ade5c84f860f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
@@ -521,7 +521,8 @@
         ({debug, verbose, overlord, blocking, type_sys, max_relevant,
           max_mono_iters, max_new_mono_instances, explicit_apply, isar_proof,
           isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
-        minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
+        minimize_command
+        ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -743,18 +744,7 @@
         extract_important_message output
       else
         ""
-    fun complete_message message =
-      message ^
-      (if verbose then
-         "\nATP real CPU time: " ^
-         string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
-       else
-         "") ^
-      (if important_message <> "" then
-         "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
-       else
-         "")
-    val (outcome, (message, used_facts)) =
+    val (message, used_facts) =
       case outcome of
         NONE =>
         let
@@ -764,24 +754,36 @@
           val reconstructor =
             if uses_typed_helpers typed_helpers atp_proof then MetisFT
             else Metis
-          val ths = facts |> map untranslated_fact
-                          |> filter_used_facts used_facts
-                          |> map snd
+          val used_ths =
+            facts |> map untranslated_fact
+                  |> filter_used_facts used_facts
+                  |> map snd
           val preplay =
-            preplay_one_line_proof debug preplay_timeout ths state subgoal
+            preplay_one_line_proof debug preplay_timeout used_ths state subgoal
                                    reconstructor
           val full_types = uses_typed_helpers typed_helpers atp_proof
           val isar_params =
             (debug, full_types, isar_shrink_factor, type_sys, pool,
-             conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof)
+             conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof,
+             goal)
           val one_line_params =
             (preplay, proof_banner mode blocking name, used_facts,
-             minimize_command, goal, subgoal)
+             minimize_command, subgoal, subgoal_count)
         in
-          (NONE, (proof_text ctxt isar_proof isar_params one_line_params
-                  |> complete_message, used_facts))
+          (proof_text ctxt isar_proof isar_params one_line_params ^
+           (if verbose then
+              "\nATP real CPU time: " ^
+              string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
+            else
+              "") ^
+           (if important_message <> "" then
+              "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
+              important_message
+            else
+              ""),
+           used_facts)
         end
-      | SOME failure => (outcome, (string_for_failure failure, []))
+      | SOME failure => (string_for_failure failure, [])
   in
     {outcome = outcome, message = message, used_facts = used_facts,
      run_time_in_msecs = msecs}
@@ -937,26 +939,25 @@
                 |> map (smt_weighted_fact ctxt num_facts)
     val {outcome, used_facts, run_time_in_msecs} =
       smt_filter_loop ctxt name params state subgoal smt_filter facts
-    val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
+    val (used_facts, used_ths) = used_facts |> ListPair.unzip
     val outcome = outcome |> Option.map failure_from_smt_failure
     val message =
       case outcome of
         NONE =>
         let
-          val (settings, method, time) =
-            case preplay_one_line_proof debug preplay_timeout
-                    (map snd used_facts) state subgoal Metis of
-              Preplayed (method, time) =>
-              ("", reconstructor_name method, SOME (false, time))
-            | _ => (if name = SMT_Solver.solver_name_of ctxt then ""
-                    else "smt_solver = " ^ maybe_quote name,
-                    "smt", NONE)
+          fun smt_settings () =
+            if name = SMT_Solver.solver_name_of ctxt then ""
+            else "smt_solver = " ^ maybe_quote name
+          val preplay =
+            case preplay_one_line_proof debug preplay_timeout used_ths state
+                                        subgoal Metis of
+              p as Preplayed _ => p
+            | _ => Trust_Playable (SMT (smt_settings ()), NONE)
+          val one_line_params =
+            (preplay, proof_banner mode blocking name, used_facts,
+             minimize_command, subgoal, subgoal_count)
         in
-          try_command_line (proof_banner mode blocking name) time
-              (apply_on_subgoal settings subgoal subgoal_count ^
-               command_call method (map fst other_lemmas)) ^
-          minimize_line minimize_command
-                        (map fst (other_lemmas @ chained_lemmas)) ^
+          one_line_proof_text one_line_params ^
           (if verbose then
              "\nSMT solver real CPU time: " ^
              string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^
@@ -966,7 +967,7 @@
         end
       | SOME failure => string_for_failure failure
   in
-    {outcome = outcome, used_facts = map fst used_facts,
+    {outcome = outcome, used_facts = used_facts,
      run_time_in_msecs = run_time_in_msecs, message = message}
   end
 
diff -r 0ef380310863 -r ade5c84f860f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:08 2011 +0200
@@ -61,7 +61,7 @@
    (if blocking then
       "."
     else
-      ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
+      "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
 
 val auto_minimize_min_facts =
   Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}