# HG changeset patch
# User blanchet
# Date 1341991949 -7200
# Node ID 6a8d1879816167d944be6a471be7d0e8f9411acf
# Parent  0016290f904c3222502403aa1fe906ed6fe3deb9
rationalized output

diff -r 0016290f904c -r 6a8d18798161 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 11 09:32:29 2012 +0200
@@ -14,6 +14,7 @@
   val theory_ord : theory * theory -> order
   val thm_ord : thm * thm -> order
   val dependencies_of : string list -> thm -> string list
+  val goal_of_thm : thm -> thm
   val meng_paulson_facts :
     Proof.context -> string -> int -> real * real -> thm -> int
     -> (((unit -> string) * stature) * thm) list
diff -r 0016290f904c -r 6a8d18798161 src/HOL/TPTP/mash_import.ML
--- a/src/HOL/TPTP/mash_import.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/mash_import.ML	Wed Jul 11 09:32:29 2012 +0200
@@ -15,6 +15,8 @@
 structure MaSh_Import : MASH_IMPORT =
 struct
 
+open MaSh_Export
+
 val unescape_meta =
   let
     fun un accum [] = String.implode (rev accum)
@@ -63,16 +65,15 @@
     fun with_index facts s =
       (find_index (fn ((s', _), _) => s = s') facts + 1, s)
     fun index_string (j, s) = s ^ "@" ^ string_of_int j
-    fun print_result label facts {outcome, run_time, used_facts, ...} =
-      tracing ("  " ^ label ^ ": " ^
-               (if is_none outcome then
-                  "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
-                  space_implode " "
-                      (used_facts |> map (with_index facts o fst)
-                                  |> sort (int_ord o pairself fst)
-                                  |> map index_string)
-                else
-                  "Failure: " ^ space_implode " " (map (fst o fst) facts) ))
+    fun str_of_res label facts {outcome, run_time, used_facts, ...} =
+      "  " ^ label ^ ": " ^
+      (if is_none outcome then
+         "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
+         space_implode " " (used_facts |> map (with_index facts o fst)
+                                       |> sort (int_ord o pairself fst)
+                                       |> map index_string)
+       else
+         "Failure: " ^ space_implode " " (map (fst o fst) facts))
     fun run_sh heading facts goal =
       let
         val problem =
@@ -81,14 +82,11 @@
         val prover =
           Sledgehammer_Run.get_minimizing_prover ctxt
               Sledgehammer_Provers.Normal prover_name
-      in
-        prover params (K (K (K ""))) problem
-        |> tap (print_result heading facts)
-      end
+        val res as {outcome, ...} = prover params (K (K (K ""))) problem
+      in (str_of_res heading facts res, is_none outcome) end
     fun solve_goal name suggs =
       let
         val name = of_fact_name name
-        val _ = tracing ("Goal: " ^ name)
         val th =
           case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of
             SOME (_, th) => th
@@ -104,12 +102,12 @@
               i facts
         val mash_facts = sugg_facts hyp_ts concl_t facts suggs
         val hybrid_facts = hybrid_facts meng_facts mash_facts
+        val (dep_s, dep_ok) = run_sh "Dependencies" deps_facts goal
+        val (meng_s, meng_ok) = run_sh "Meng & Paulson" meng_facts goal
+        val (mash_s, mash_ok) = run_sh "MaSh" mash_facts goal
+        val (hybrid_s, hybrid_ok) = run_sh "Hybrid" hybrid_facts goal
       in
-        run_sh "Dependencies" deps_facts goal;
-        run_sh "Meng & Paulson" meng_facts goal;
-        run_sh "MaSh" mash_facts goal;
-        run_sh "Hybrid" hybrid_facts goal;
-        ()
+        tracing (cat_lines ["Goal: ", name, dep_s, meng_s, mash_s, hybrid_s])
       end
     val explode_suggs = space_explode " " #> filter_out (curry (op =) "")
     fun do_line line =