repair MaSh exporter
authorblanchet
Wed, 18 Jul 2012 08:44:05 +0200
changeset 48333 2250197977dc
parent 48332 271a4a6af734
child 48334 8dff9933e72a
repair MaSh exporter
src/HOL/TPTP/MaSh_Eval.thy
src/HOL/TPTP/MaSh_Export.thy
src/HOL/TPTP/mash_eval.ML
src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Jul 18 08:44:05 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Jul 18 08:44:05 2012 +0200
@@ -5,7 +5,7 @@
 header {* MaSh Evaluation Driver *}
 
 theory MaSh_Eval
-imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
+imports Complex_Main
 uses "mash_eval.ML"
 begin
 
@@ -20,14 +20,14 @@
 *}
 
 ML {*
-val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory Nat};
+val do_it = false (* switch to "true" to generate the files *)
+val thy = @{theory Nat}
 val params = Sledgehammer_Isar.default_params @{context} []
 *}
 
 ML {*
 if do_it then
-  evaluate_mash_suggestions @{context} params thy "/Users/blanchet/tum/mash/mash/results/natNB200ATP-15.pred"
+  evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions"
 else
   ()
 *}
--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:05 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:05 2012 +0200
@@ -5,7 +5,7 @@
 header {* MaSh Exporter *}
 
 theory MaSh_Export
-imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
+imports Complex_Main
 uses "mash_export.ML"
 begin
 
@@ -18,9 +18,10 @@
 *}
 
 ML {*
-val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory List};
-val params = Sledgehammer_Isar.default_params @{context} []
+val do_it = false (* switch to "true" to generate the files *)
+val thy = @{theory List}
+val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
+val prover = hd provers
 *}
 
 ML {*
@@ -32,14 +33,28 @@
 
 ML {*
 if do_it then
-  generate_features @{context} thy false "/tmp/mash_features"
+  generate_features @{context} prover thy false "/tmp/mash_features"
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
+  generate_isar_dependencies thy false "/tmp/mash_dependencies"
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_commands @{context} prover thy "/tmp/mash_commands"
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
 else
   ()
 *}
@@ -51,18 +66,5 @@
   ()
 *}
 
-ML {*
-if do_it then
-  generate_commands @{context} thy "/tmp/mash_commands"
-else
-  ()
-*}
-
-ML {*
-if do_it then
-  generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
-else
-  ()
-*}
 
 end
--- a/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:05 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:05 2012 +0200
@@ -27,7 +27,7 @@
 val max_facts_slack = 2
 
 val all_names =
-  filter_out (is_likely_tautology_or_too_meta)
+  filter_out is_likely_tautology_or_too_meta
   #> map (rpair () o Thm.get_name_hint) #> Symtab.make
 
 fun evaluate_mash_suggestions ctxt params thy file_name =
--- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:05 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:05 2012 +0200
@@ -12,9 +12,9 @@
   val generate_accessibility : theory -> bool -> string -> unit
   val generate_features :
     Proof.context -> string -> theory -> bool -> string -> unit
-  val generate_isa_dependencies :
+  val generate_isar_dependencies :
     theory -> bool -> string -> unit
-  val generate_prover_dependencies :
+  val generate_atp_dependencies :
     Proof.context -> params -> theory -> bool -> string -> unit
   val generate_commands : Proof.context -> string -> theory -> string -> unit
   val generate_iter_suggestions :
@@ -50,7 +50,7 @@
 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
 
 val all_names =
-  filter_out (is_likely_tautology_or_too_meta)
+  filter_out is_likely_tautology_or_too_meta
   #> map (rpair () o Thm.get_name_hint) #> Symtab.make
 
 fun generate_accessibility thy include_thy file_name =
@@ -71,7 +71,7 @@
         val thy = thy_of_fact thy (hd facts)
         val parents = parent_facts thy thy_map
       in fold do_fact facts parents; () end
-  in fold_rev (fn (_, facts) => K (do_thy facts)) thy_map () end
+  in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
 
 fun generate_features ctxt prover thy include_thy file_name =
   let
@@ -90,7 +90,7 @@
       in File.append path s end
   in List.app do_fact facts end
 
-fun generate_isa_dependencies thy include_thy file_name =
+fun generate_isar_dependencies thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -107,8 +107,8 @@
       in File.append path s end
   in List.app do_thm ths end
 
-fun generate_prover_dependencies ctxt (params as {provers, max_facts, ...}) thy
-                                 include_thy file_name =
+fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy
+                              include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -119,7 +119,7 @@
     val ths = facts |> map snd
     val all_names = all_names ths
     fun is_dep dep (_, th) = Thm.get_name_hint th = dep
-    fun add_isa_dep facts dep accum =
+    fun add_isar_dep facts dep accum =
       if exists (is_dep dep) accum then
         accum
       else case find_first (is_dep dep) facts of
@@ -135,21 +135,21 @@
         val deps =
           case isabelle_dependencies_of all_names th of
             [] => []
-          | isa_dep as [_] => isa_dep (* can hardly beat that *)
-          | isa_deps =>
+          | isar_dep as [_] => isar_dep (* can hardly beat that *)
+          | isar_deps =>
             let
               val facts =
                 facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
               val facts =
                 facts |> iterative_relevant_facts ctxt params prover
                              (the max_facts) NONE hyp_ts concl_t
-                      |> fold (add_isa_dep facts) isa_deps
+                      |> fold (add_isar_dep facts) isar_deps
                       |> map fix_name
             in
               case run_prover_for_mash ctxt params prover facts goal of
                 {outcome = NONE, used_facts, ...} =>
                 used_facts |> map fst |> sort string_ord
-              | _ => isa_deps
+              | _ => isar_deps
             end
         val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
       in File.append path s end