1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 18:53:13 2013 +0100
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 19:20:56 2013 +0100
     1.3 @@ -29,6 +29,8 @@
     1.4  val thys = [@{theory List}]
     1.5  val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
     1.6  val prover = hd provers
     1.7 +val range = (1, NONE)
     1.8 +val step = 1
     1.9  val max_suggestions = 1536
    1.10  val dir = "List"
    1.11  val prefix = "/tmp/" ^ dir ^ "/"
    1.12 @@ -65,15 +67,16 @@
    1.13  
    1.14  ML {*
    1.15  if do_it then
    1.16 -  generate_isar_commands @{context} prover thys (prefix ^ "mash_commands")
    1.17 +  generate_isar_commands @{context} prover (range, step) thys
    1.18 +      (prefix ^ "mash_commands")
    1.19  else
    1.20    ()
    1.21  *}
    1.22  
    1.23  ML {*
    1.24  if do_it then
    1.25 -  generate_mepo_suggestions @{context} params (1, NONE) thys max_suggestions
    1.26 -      (prefix ^ "mepo_suggestions")
    1.27 +  generate_mepo_suggestions @{context} params (range, step) thys
    1.28 +      max_suggestions (prefix ^ "mepo_suggestions")
    1.29  else
    1.30    ()
    1.31  *}
    1.32 @@ -88,7 +91,7 @@
    1.33  
    1.34  ML {*
    1.35  if do_it then
    1.36 -  generate_prover_dependencies @{context} params (1, NONE) thys false
    1.37 +  generate_prover_dependencies @{context} params range thys false
    1.38        (prefix ^ "mash_prover_dependencies")
    1.39  else
    1.40    ()
    1.41 @@ -96,7 +99,7 @@
    1.42  
    1.43  ML {*
    1.44  if do_it then
    1.45 -  generate_prover_commands @{context} params (1, NONE) thys
    1.46 +  generate_prover_commands @{context} params (range, step) thys
    1.47        (prefix ^ "mash_prover_commands")
    1.48  else
    1.49    ()

     2.1 --- a/src/HOL/TPTP/mash_export.ML	Thu Jan 17 18:53:13 2013 +0100
     2.2 +++ b/src/HOL/TPTP/mash_export.ML	Thu Jan 17 19:20:56 2013 +0100
     2.3 @@ -19,12 +19,14 @@
     2.4      Proof.context -> params -> int * int option -> theory list -> bool -> string
     2.5      -> unit
     2.6    val generate_isar_commands :
     2.7 -    Proof.context -> string -> theory list -> string -> unit
     2.8 +    Proof.context -> string -> (int * int option) * int -> theory list -> string
     2.9 +    -> unit
    2.10    val generate_prover_commands :
    2.11 -    Proof.context -> params -> int * int option -> theory list -> string -> unit
    2.12 +    Proof.context -> params -> (int * int option) * int -> theory list -> string
    2.13 +    -> unit
    2.14    val generate_mepo_suggestions :
    2.15 -    Proof.context -> params -> int * int option -> theory list -> int -> string
    2.16 -    -> unit
    2.17 +    Proof.context -> params -> (int * int option) * int -> theory list -> int
    2.18 +    -> string -> unit
    2.19    val generate_mesh_suggestions : int -> string -> string -> string -> unit
    2.20  end;
    2.21  
    2.22 @@ -118,12 +120,13 @@
    2.23  fun generate_prover_dependencies ctxt params =
    2.24    generate_isar_or_prover_dependencies ctxt (SOME params)
    2.25  
    2.26 -fun is_bad_query ctxt ho_atp th isar_deps =
    2.27 +fun is_bad_query ctxt ho_atp step j th isar_deps =
    2.28 +  j mod step <> 0 orelse
    2.29    Thm.legacy_get_kind th = "" orelse
    2.30    null (these (trim_dependencies th isar_deps)) orelse
    2.31    is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
    2.32  
    2.33 -fun generate_isar_or_prover_commands ctxt prover params_opt range thys
    2.34 +fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
    2.35                                       file_name =
    2.36    let
    2.37      val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
    2.38 @@ -145,7 +148,7 @@
    2.39              encode_str name ^ ": " ^ encode_strs prevs ^ "; " ^
    2.40              encode_features (sort_wrt fst feats)
    2.41            val query =
    2.42 -            if is_bad_query ctxt ho_atp th isar_deps then ""
    2.43 +            if is_bad_query ctxt ho_atp step j th isar_deps then ""
    2.44              else "? " ^ core ^ "\n"
    2.45            val update =
    2.46              "! " ^ core ^ "; " ^
    2.47 @@ -161,13 +164,13 @@
    2.48    in File.write_list path lines end
    2.49  
    2.50  fun generate_isar_commands ctxt prover =
    2.51 -  generate_isar_or_prover_commands ctxt prover NONE (1, NONE)
    2.52 +  generate_isar_or_prover_commands ctxt prover NONE
    2.53  
    2.54  fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) =
    2.55    generate_isar_or_prover_commands ctxt prover (SOME params)
    2.56  
    2.57  fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...})
    2.58 -                              range thys max_suggs file_name =
    2.59 +                              (range, step) thys max_suggs file_name =
    2.60    let
    2.61      val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
    2.62      val path = file_name |> Path.explode
    2.63 @@ -183,7 +186,7 @@
    2.64            val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    2.65            val isar_deps = isar_dependencies_of name_tabs th
    2.66          in
    2.67 -          if is_bad_query ctxt ho_atp th isar_deps then
    2.68 +          if is_bad_query ctxt ho_atp step j th isar_deps then
    2.69              ""
    2.70            else
    2.71              let