# HG changeset patch
# User blanchet
# Date 1358446856 -3600
# Node ID 7bc58677860ed6d94b6c1bbf3c94210ca9146702
# Parent  c4c746bbf8368b5e8821b664a500b89907b53b50
added step to skip some queries

diff -r c4c746bbf836 -r 7bc58677860e src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 18:53:13 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 19:20:56 2013 +0100
@@ -29,6 +29,8 @@
 val thys = [@{theory List}]
 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
 val prover = hd provers
+val range = (1, NONE)
+val step = 1
 val max_suggestions = 1536
 val dir = "List"
 val prefix = "/tmp/" ^ dir ^ "/"
@@ -65,15 +67,16 @@
 
 ML {*
 if do_it then
-  generate_isar_commands @{context} prover thys (prefix ^ "mash_commands")
+  generate_isar_commands @{context} prover (range, step) thys
+      (prefix ^ "mash_commands")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_mepo_suggestions @{context} params (1, NONE) thys max_suggestions
-      (prefix ^ "mepo_suggestions")
+  generate_mepo_suggestions @{context} params (range, step) thys
+      max_suggestions (prefix ^ "mepo_suggestions")
 else
   ()
 *}
@@ -88,7 +91,7 @@
 
 ML {*
 if do_it then
-  generate_prover_dependencies @{context} params (1, NONE) thys false
+  generate_prover_dependencies @{context} params range thys false
       (prefix ^ "mash_prover_dependencies")
 else
   ()
@@ -96,7 +99,7 @@
 
 ML {*
 if do_it then
-  generate_prover_commands @{context} params (1, NONE) thys
+  generate_prover_commands @{context} params (range, step) thys
       (prefix ^ "mash_prover_commands")
 else
   ()
diff -r c4c746bbf836 -r 7bc58677860e src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Thu Jan 17 18:53:13 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Thu Jan 17 19:20:56 2013 +0100
@@ -19,12 +19,14 @@
     Proof.context -> params -> int * int option -> theory list -> bool -> string
     -> unit
   val generate_isar_commands :
-    Proof.context -> string -> theory list -> string -> unit
+    Proof.context -> string -> (int * int option) * int -> theory list -> string
+    -> unit
   val generate_prover_commands :
-    Proof.context -> params -> int * int option -> theory list -> string -> unit
+    Proof.context -> params -> (int * int option) * int -> theory list -> string
+    -> unit
   val generate_mepo_suggestions :
-    Proof.context -> params -> int * int option -> theory list -> int -> string
-    -> unit
+    Proof.context -> params -> (int * int option) * int -> theory list -> int
+    -> string -> unit
   val generate_mesh_suggestions : int -> string -> string -> string -> unit
 end;
 
@@ -118,12 +120,13 @@
 fun generate_prover_dependencies ctxt params =
   generate_isar_or_prover_dependencies ctxt (SOME params)
 
-fun is_bad_query ctxt ho_atp th isar_deps =
+fun is_bad_query ctxt ho_atp step j th isar_deps =
+  j mod step <> 0 orelse
   Thm.legacy_get_kind th = "" orelse
   null (these (trim_dependencies th isar_deps)) orelse
   is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
 
-fun generate_isar_or_prover_commands ctxt prover params_opt range thys
+fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
                                      file_name =
   let
     val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
@@ -145,7 +148,7 @@
             encode_str name ^ ": " ^ encode_strs prevs ^ "; " ^
             encode_features (sort_wrt fst feats)
           val query =
-            if is_bad_query ctxt ho_atp th isar_deps then ""
+            if is_bad_query ctxt ho_atp step j th isar_deps then ""
             else "? " ^ core ^ "\n"
           val update =
             "! " ^ core ^ "; " ^
@@ -161,13 +164,13 @@
   in File.write_list path lines end
 
 fun generate_isar_commands ctxt prover =
-  generate_isar_or_prover_commands ctxt prover NONE (1, NONE)
+  generate_isar_or_prover_commands ctxt prover NONE
 
 fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) =
   generate_isar_or_prover_commands ctxt prover (SOME params)
 
 fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...})
-                              range thys max_suggs file_name =
+                              (range, step) thys max_suggs file_name =
   let
     val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     val path = file_name |> Path.explode
@@ -183,7 +186,7 @@
           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
           val isar_deps = isar_dependencies_of name_tabs th
         in
-          if is_bad_query ctxt ho_atp th isar_deps then
+          if is_bad_query ctxt ho_atp step j th isar_deps then
             ""
           else
             let