# HG changeset patch
# User blanchet
# Date 1354808988 -3600
# Node ID c9023d78d1a6b3ca47161d696232978f063e027d
# Parent  923f1e199f4f6ac68075d1f2d08fe106ebfc3609
export ATP and Isar commands separately

diff -r 923f1e199f4f -r c9023d78d1a6 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Thu Dec 06 16:07:09 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Dec 06 16:49:48 2012 +0100
@@ -11,8 +11,8 @@
 ML_file "mash_export.ML"
 
 sledgehammer_params
-  [provers = spass, max_relevant = 40, strict, dont_slice, type_enc = mono_native,
-   lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize]
+  [provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native,
+   lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize]
 
 ML {*
 open MaSh_Export
@@ -57,7 +57,7 @@
 
 ML {*
 if do_it then
-  generate_commands @{context} params thys (prefix ^ "mash_commands")
+  generate_isar_commands @{context} prover thys (prefix ^ "mash_commands")
 else
   ()
 *}
@@ -76,4 +76,11 @@
   ()
 *}
 
+ML {*
+if do_it then
+  generate_atp_commands @{context} params thys (prefix ^ "mash_atp_commands")
+else
+  ()
+*}
+
 end
diff -r 923f1e199f4f -r c9023d78d1a6 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Thu Dec 06 16:07:09 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Thu Dec 06 16:49:48 2012 +0100
@@ -17,7 +17,9 @@
     Proof.context -> theory list -> bool -> string -> unit
   val generate_atp_dependencies :
     Proof.context -> params -> theory list -> bool -> string -> unit
-  val generate_commands :
+  val generate_isar_commands :
+    Proof.context -> string -> theory list -> string -> unit
+  val generate_atp_commands :
     Proof.context -> params -> theory list -> string -> unit
   val generate_mepo_suggestions :
     Proof.context -> params -> theory list -> int -> string -> unit
@@ -97,29 +99,18 @@
       in File.append path s end
   in List.app do_fact facts end
 
-fun generate_isar_dependencies ctxt thys include_thys file_name =
+fun isar_or_atp_dependencies_of ctxt params_opt facts all_names th =
+  (case params_opt of
+     SOME (params as {provers = prover :: _, ...}) =>
+     atp_dependencies_of ctxt params prover 0 facts all_names th |> snd
+   | NONE => isar_dependencies_of all_names th)
+  |> these
+
+fun generate_isar_or_atp_dependencies ctxt params_opt thys include_thys
+                                      file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val ths =
-      all_facts ctxt
-      |> not include_thys ? filter_out (has_thys thys o snd)
-      |> map snd
-    val all_names = all_names ths
-    fun do_thm th =
-      let
-        val name = nickname_of th
-        val deps = isar_dependencies_of all_names th |> these
-        val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
-      in File.append path s end
-  in List.app do_thm ths end
-
-fun generate_atp_dependencies ctxt (params as {provers, ...}) thys include_thys
-                              file_name =
-  let
-    val path = file_name |> Path.explode
-    val _ = File.write path ""
-    val prover = hd provers
     val facts =
       all_facts ctxt
       |> not include_thys ? filter_out (has_thys thys o snd)
@@ -129,17 +120,21 @@
       let
         val name = nickname_of th
         val deps =
-          atp_dependencies_of ctxt params prover 0 facts all_names th
-          |> snd |> these
+          isar_or_atp_dependencies_of ctxt params_opt facts all_names th
         val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
       in File.append path s end
   in List.app do_thm ths end
 
-fun generate_commands ctxt (params as {provers, ...}) thys file_name =
+fun generate_isar_dependencies ctxt =
+  generate_isar_or_atp_dependencies ctxt NONE
+
+fun generate_atp_dependencies ctxt params =
+  generate_isar_or_atp_dependencies ctxt (SOME params)
+
+fun generate_isar_or_atp_commands ctxt prover params_opt thys file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val prover = hd provers
     val facts = all_facts ctxt
     val (new_facts, old_facts) =
       facts |> List.partition (has_thys thys o snd)
@@ -151,8 +146,7 @@
         val feats =
           features_of ctxt prover (theory_of_thm th) stature [prop_of th]
         val deps =
-          atp_dependencies_of ctxt params prover 0 facts all_names th
-          |> snd |> these
+          isar_or_atp_dependencies_of ctxt params_opt facts all_names th
         val kind = Thm.legacy_get_kind th
         val core =
           escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
@@ -166,6 +160,12 @@
     val parents = fold (add_thy_parent_facts thy_map) thys []
   in fold do_fact new_facts parents; () end
 
+fun generate_isar_commands ctxt prover =
+  generate_isar_or_atp_commands ctxt prover NONE
+
+fun generate_atp_commands ctxt (params as {provers = prover :: _, ...}) =
+  generate_isar_or_atp_commands ctxt prover (SOME params)
+
 fun generate_mepo_suggestions ctxt (params as {provers, ...}) thys max_relevant
                               file_name =
   let