src/HOL/TPTP/MaSh_Export.thy

--- a/src/HOL/TPTP/MaSh_Export.thy	Fri May 30 08:23:08 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Fri May 30 12:27:51 2014 +0200
@@ -8,6 +8,7 @@
 imports Main
 begin
 
+ML_file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML" (*###*)
 ML_file "mash_export.ML"
 
 sledgehammer_params
@@ -27,11 +28,11 @@
 *}
 
 ML {*
-val do_it = false (* switch to "true" to generate the files *)
+val do_it = true (*###*) (* switch to "true" to generate the files *)
 val thys = [@{theory List}]
 val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
 val prover = hd provers
-val range = (1, NONE)
+val range = (1, (* ### NONE *) SOME 100)
 val step = 1
 val linearize = false
 val max_suggestions = 1024
@@ -46,10 +47,39 @@
   ()
 *}
 
+ML {* Options.put_default @{system_option MaSh} "sml_knn" *}
+
+ML {*
+if do_it then
+  generate_mash_suggestions @{context} params (range, step) thys linearize max_suggestions
+    (prefix ^ "mash_sml_knn_suggestions")
+else
+  ()
+*}
+
+ML {* Options.put_default @{system_option MaSh} "sml_nb" *}
+
 ML {*
 if do_it then
-  generate_accessibility @{context} thys linearize
-      (prefix ^ "mash_accessibility")
+  generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
+    (prefix ^ "mash_sml_nb_suggestions")
+else
+  ()
+*}
+
+ML {* Options.put_default @{system_option MaSh} "py" *}
+
+ML {*
+if do_it then
+  generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
+    (prefix ^ "mepo_suggestions")
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_accessibility @{context} thys linearize (prefix ^ "mash_accessibility")
 else
   ()
 *}
@@ -63,24 +93,23 @@
 
 ML {*
 if do_it then
-  generate_isar_dependencies @{context} range thys linearize
-      (prefix ^ "mash_dependencies")
+  generate_isar_dependencies @{context} range thys linearize (prefix ^ "mash_dependencies")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_isar_commands @{context} prover (range, step) thys linearize
-      max_suggestions (prefix ^ "mash_commands")
+  generate_isar_commands @{context} prover (range, step) thys linearize max_suggestions
+    (prefix ^ "mash_commands")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_mepo_suggestions @{context} params (range, step) thys linearize
-      max_suggestions (prefix ^ "mepo_suggestions")
+  generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
+    (prefix ^ "mepo_suggestions")
 else
   ()
 *}
@@ -88,7 +117,7 @@
 ML {*
 if do_it then
   generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions")
-      (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
+    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
 else
   ()
 *}
@@ -96,15 +125,15 @@
 ML {*
 if do_it then
   generate_prover_dependencies @{context} params range thys linearize
-      (prefix ^ "mash_prover_dependencies")
+    (prefix ^ "mash_prover_dependencies")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_prover_commands @{context} params (range, step) thys linearize
-      max_suggestions (prefix ^ "mash_prover_commands")
+  generate_prover_commands @{context} params (range, step) thys linearize max_suggestions
+    (prefix ^ "mash_prover_commands")
 else
   ()
 *}
@@ -112,7 +141,7 @@
 ML {*
 if do_it then
   generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions")
-      (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")
+    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")
 else
   ()
 *}