1.1 --- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Jul 18 08:44:05 2012 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Jul 18 08:44:05 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* MaSh Evaluation Driver *}
     1.5  
     1.6  theory MaSh_Eval
     1.7 -imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
     1.8 +imports Complex_Main
     1.9  uses "mash_eval.ML"
    1.10  begin
    1.11  
    1.12 @@ -20,14 +20,14 @@
    1.13  *}
    1.14  
    1.15  ML {*
    1.16 -val do_it = false (* switch to "true" to generate the files *);
    1.17 -val thy = @{theory Nat};
    1.18 +val do_it = false (* switch to "true" to generate the files *)
    1.19 +val thy = @{theory Nat}
    1.20  val params = Sledgehammer_Isar.default_params @{context} []
    1.21  *}
    1.22  
    1.23  ML {*
    1.24  if do_it then
    1.25 -  evaluate_mash_suggestions @{context} params thy "/Users/blanchet/tum/mash/mash/results/natNB200ATP-15.pred"
    1.26 +  evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions"
    1.27  else
    1.28    ()
    1.29  *}

     2.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:05 2012 +0200
     2.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:05 2012 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* MaSh Exporter *}
     2.5  
     2.6  theory MaSh_Export
     2.7 -imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
     2.8 +imports Complex_Main
     2.9  uses "mash_export.ML"
    2.10  begin
    2.11  
    2.12 @@ -18,9 +18,10 @@
    2.13  *}
    2.14  
    2.15  ML {*
    2.16 -val do_it = false (* switch to "true" to generate the files *);
    2.17 -val thy = @{theory List};
    2.18 -val params = Sledgehammer_Isar.default_params @{context} []
    2.19 +val do_it = false (* switch to "true" to generate the files *)
    2.20 +val thy = @{theory List}
    2.21 +val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
    2.22 +val prover = hd provers
    2.23  *}
    2.24  
    2.25  ML {*
    2.26 @@ -32,14 +33,28 @@
    2.27  
    2.28  ML {*
    2.29  if do_it then
    2.30 -  generate_features @{context} thy false "/tmp/mash_features"
    2.31 +  generate_features @{context} prover thy false "/tmp/mash_features"
    2.32  else
    2.33    ()
    2.34  *}
    2.35  
    2.36  ML {*
    2.37  if do_it then
    2.38 -  generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
    2.39 +  generate_isar_dependencies thy false "/tmp/mash_dependencies"
    2.40 +else
    2.41 +  ()
    2.42 +*}
    2.43 +
    2.44 +ML {*
    2.45 +if do_it then
    2.46 +  generate_commands @{context} prover thy "/tmp/mash_commands"
    2.47 +else
    2.48 +  ()
    2.49 +*}
    2.50 +
    2.51 +ML {*
    2.52 +if do_it then
    2.53 +  generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
    2.54  else
    2.55    ()
    2.56  *}
    2.57 @@ -51,18 +66,5 @@
    2.58    ()
    2.59  *}
    2.60  
    2.61 -ML {*
    2.62 -if do_it then
    2.63 -  generate_commands @{context} thy "/tmp/mash_commands"
    2.64 -else
    2.65 -  ()
    2.66 -*}
    2.67 -
    2.68 -ML {*
    2.69 -if do_it then
    2.70 -  generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
    2.71 -else
    2.72 -  ()
    2.73 -*}
    2.74  
    2.75  end

     3.1 --- a/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:05 2012 +0200
     3.2 +++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:05 2012 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4  val max_facts_slack = 2
     3.5  
     3.6  val all_names =
     3.7 -  filter_out (is_likely_tautology_or_too_meta)
     3.8 +  filter_out is_likely_tautology_or_too_meta
     3.9    #> map (rpair () o Thm.get_name_hint) #> Symtab.make
    3.10  
    3.11  fun evaluate_mash_suggestions ctxt params thy file_name =

     4.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:05 2012 +0200
     4.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:05 2012 +0200
     4.3 @@ -12,9 +12,9 @@
     4.4    val generate_accessibility : theory -> bool -> string -> unit
     4.5    val generate_features :
     4.6      Proof.context -> string -> theory -> bool -> string -> unit
     4.7 -  val generate_isa_dependencies :
     4.8 +  val generate_isar_dependencies :
     4.9      theory -> bool -> string -> unit
    4.10 -  val generate_prover_dependencies :
    4.11 +  val generate_atp_dependencies :
    4.12      Proof.context -> params -> theory -> bool -> string -> unit
    4.13    val generate_commands : Proof.context -> string -> theory -> string -> unit
    4.14    val generate_iter_suggestions :
    4.15 @@ -50,7 +50,7 @@
    4.16  fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
    4.17  
    4.18  val all_names =
    4.19 -  filter_out (is_likely_tautology_or_too_meta)
    4.20 +  filter_out is_likely_tautology_or_too_meta
    4.21    #> map (rpair () o Thm.get_name_hint) #> Symtab.make
    4.22  
    4.23  fun generate_accessibility thy include_thy file_name =
    4.24 @@ -71,7 +71,7 @@
    4.25          val thy = thy_of_fact thy (hd facts)
    4.26          val parents = parent_facts thy thy_map
    4.27        in fold do_fact facts parents; () end
    4.28 -  in fold_rev (fn (_, facts) => K (do_thy facts)) thy_map () end
    4.29 +  in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
    4.30  
    4.31  fun generate_features ctxt prover thy include_thy file_name =
    4.32    let
    4.33 @@ -90,7 +90,7 @@
    4.34        in File.append path s end
    4.35    in List.app do_fact facts end
    4.36  
    4.37 -fun generate_isa_dependencies thy include_thy file_name =
    4.38 +fun generate_isar_dependencies thy include_thy file_name =
    4.39    let
    4.40      val path = file_name |> Path.explode
    4.41      val _ = File.write path ""
    4.42 @@ -107,8 +107,8 @@
    4.43        in File.append path s end
    4.44    in List.app do_thm ths end
    4.45  
    4.46 -fun generate_prover_dependencies ctxt (params as {provers, max_facts, ...}) thy
    4.47 -                                 include_thy file_name =
    4.48 +fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy
    4.49 +                              include_thy file_name =
    4.50    let
    4.51      val path = file_name |> Path.explode
    4.52      val _ = File.write path ""
    4.53 @@ -119,7 +119,7 @@
    4.54      val ths = facts |> map snd
    4.55      val all_names = all_names ths
    4.56      fun is_dep dep (_, th) = Thm.get_name_hint th = dep
    4.57 -    fun add_isa_dep facts dep accum =
    4.58 +    fun add_isar_dep facts dep accum =
    4.59        if exists (is_dep dep) accum then
    4.60          accum
    4.61        else case find_first (is_dep dep) facts of
    4.62 @@ -135,21 +135,21 @@
    4.63          val deps =
    4.64            case isabelle_dependencies_of all_names th of
    4.65              [] => []
    4.66 -          | isa_dep as [_] => isa_dep (* can hardly beat that *)
    4.67 -          | isa_deps =>
    4.68 +          | isar_dep as [_] => isar_dep (* can hardly beat that *)
    4.69 +          | isar_deps =>
    4.70              let
    4.71                val facts =
    4.72                  facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    4.73                val facts =
    4.74                  facts |> iterative_relevant_facts ctxt params prover
    4.75                               (the max_facts) NONE hyp_ts concl_t
    4.76 -                      |> fold (add_isa_dep facts) isa_deps
    4.77 +                      |> fold (add_isar_dep facts) isar_deps
    4.78                        |> map fix_name
    4.79              in
    4.80                case run_prover_for_mash ctxt params prover facts goal of
    4.81                  {outcome = NONE, used_facts, ...} =>
    4.82                  used_facts |> map fst |> sort string_ord
    4.83 -              | _ => isa_deps
    4.84 +              | _ => isar_deps
    4.85              end
    4.86          val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
    4.87        in File.append path s end