generate ATP dependencies

--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 13:59:39 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 21:43:19 2012 +0200
@@ -9,40 +9,66 @@
 uses "mash_export.ML"
 begin
 
-sledgehammer_params [provers = e, max_relevant = 500]
+sledgehammer_params
+  [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
+   lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
 
 ML {*
 open MaSh_Export
 *}
 
 ML {*
-val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory List}
+if do_it then
+  generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
+else
+  ()
+*}
+
+ML {*
+val do_it = true (* switch to "true" to generate the files *);
+val thy = @{theory Nat}
 *}
 
 ML {*
-if do_it then generate_meng_paulson_suggestions @{context} thy "/tmp/mash_meng_paulson_suggestions"
-else ()
+if do_it then
+  generate_features thy false "/tmp/mash_features"
+else
+  ()
 *}
 
 ML {*
-if do_it then generate_mash_commands thy "/tmp/mash_commands"
-else ()
+if do_it then
+  generate_accessibility thy false "/tmp/mash_accessibility"
+else
+  ()
 *}
 
 ML {*
-if do_it then generate_mash_features thy false "/tmp/mash_features"
-else ()
+if do_it then
+  generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
+else
+  ()
 *}
 
 ML {*
-if do_it then generate_mash_accessibility thy false "/tmp/mash_accessibility"
-else ()
+if do_it then
+  generate_commands thy "/tmp/mash_commands"
+else
+  ()
 *}
 
 ML {*
-if do_it then generate_mash_dependencies thy false "/tmp/mash_dependencies"
-else ()
+if do_it then
+  generate_meng_paulson_suggestions @{context} thy 500 "/tmp/mash_meng_paulson_suggestions"
+else
+  ()
 *}
 
 end

--- a/src/HOL/TPTP/MaSh_Import.thy	Wed Jul 11 13:59:39 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Import.thy	Wed Jul 11 21:43:19 2012 +0200
@@ -21,11 +21,11 @@
 
 ML {*
 val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory Nat}
+val thy = @{theory List}
 *}
 
 ML {*
-if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions"
+if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
 else ()
 *}
 

--- a/src/HOL/TPTP/mash_export.ML	Wed Jul 11 13:59:39 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 11 21:43:19 2012 +0200
@@ -8,6 +8,7 @@
 signature MASH_EXPORT =
 sig
   type stature = ATP_Problem_Generate.stature
+  type prover_result = Sledgehammer_Provers.prover_result
 
   val non_tautological_facts_of :
     theory -> (((unit -> string) * stature) * thm) list
@@ -16,15 +17,18 @@
   val dependencies_of : string list -> thm -> string list
   val goal_of_thm : thm -> thm
   val meng_paulson_facts :
-    Proof.context -> string -> int -> real * real -> thm -> int
-    -> (((unit -> string) * stature) * thm) list
+    Proof.context -> int -> thm -> (((unit -> string) * stature) * thm) list
     -> ((string * stature) * thm) list
-  val generate_mash_accessibility : theory -> bool -> string -> unit
-  val generate_mash_features : theory -> bool -> string -> unit
-  val generate_mash_dependencies : theory -> bool -> string -> unit
-  val generate_mash_commands : theory -> string -> unit
+  val run_sledgehammer :
+    Proof.context -> ((string * stature) * thm) list -> thm -> prover_result
+  val generate_accessibility : theory -> bool -> string -> unit
+  val generate_features : theory -> bool -> string -> unit
+  val generate_isa_dependencies : theory -> bool -> string -> unit
+  val generate_atp_dependencies :
+    Proof.context -> theory -> bool -> string -> unit
+  val generate_commands : theory -> string -> unit
   val generate_meng_paulson_suggestions :
-    Proof.context -> theory -> string -> unit
+    Proof.context -> theory -> int -> string -> unit
 end;
 
 structure MaSh_Export : MASH_EXPORT =
@@ -33,6 +37,8 @@
 open ATP_Problem_Generate
 open ATP_Util
 
+type prover_result = Sledgehammer_Provers.prover_result
+
 fun stringN_of_int 0 _ = ""
   | stringN_of_int k n =
     stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
@@ -105,13 +111,11 @@
   let
     val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
     val bad_consts = atp_widely_irrelevant_consts
-    val add_classes =
-      subtract (op =) @{sort type} #> map class_name_of #> union (op =)
     fun do_add_type (Type (s, Ts)) =
         (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
         #> fold do_add_type Ts
-      | do_add_type (TFree (_, S)) = add_classes S
-      | do_add_type (TVar (_, S)) = add_classes S
+      | do_add_type (TFree (_, S)) = union (op =) (map class_name_of S)
+      | do_add_type (TVar (_, S)) = union (op =) (map class_name_of S)
     fun add_type T = type_max_depth >= 0 ? do_add_type T
     fun mk_app s args =
       if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
@@ -211,10 +215,12 @@
 
 val goal_of_thm = prop_of #> freeze #> cterm_of thy #> Goal.init
 
-fun meng_paulson_facts ctxt prover_name max_relevant relevance_thresholds
-                       goal i =
+fun meng_paulson_facts ctxt max_relevant goal =
   let
-    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
+    val {provers, relevance_thresholds, ...} =
+      Sledgehammer_Isar.default_params ctxt []
+    val prover_name = hd provers
+    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
     val is_built_in_const =
       Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
     val relevance_fudge =
@@ -226,7 +232,18 @@
         hyp_ts concl_t
   end
 
-fun generate_mash_accessibility thy include_thy file_name =
+fun run_sledgehammer ctxt facts goal =
+  let
+    val params as {provers, ...} = Sledgehammer_Isar.default_params ctxt []
+    val problem =
+      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
+       facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
+    val prover =
+      Sledgehammer_Run.get_minimizing_prover ctxt
+          Sledgehammer_Provers.Normal (hd provers)
+  in prover params (K (K (K ""))) problem end
+
+fun generate_accessibility thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -247,7 +264,7 @@
       in fold do_thm ths parents; () end
   in List.app (do_thy o snd) thy_ths end
 
-fun generate_mash_features thy include_thy file_name =
+fun generate_features thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -262,7 +279,7 @@
       in File.append path s end
   in List.app do_fact facts end
 
-fun generate_mash_dependencies thy include_thy file_name =
+fun generate_isa_dependencies thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -279,7 +296,35 @@
       in File.append path s end
   in List.app do_thm ths end
 
-fun generate_mash_commands thy file_name =
+fun generate_atp_dependencies ctxt thy include_thy file_name =
+  let
+    val {max_relevant, ...} = Sledgehammer_Isar.default_params ctxt []
+    val path = file_name |> Path.explode
+    val _ = File.write path ""
+    val facts =
+      non_tautological_facts_of thy
+      |> not include_thy ? filter_out (has_thy thy o snd)
+    val ths = facts |> map snd
+    val all_names = ths |> map Thm.get_name_hint
+    fun do_thm th =
+      let
+        val name = Thm.get_name_hint th
+        val goal = goal_of_thm th
+        val facts =
+          facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
+                |> meng_paulson_facts ctxt (the max_relevant) goal
+                |> map (fn ((_, stature), th) =>
+                           ((th |> Thm.get_name_hint |> fact_name_of, stature),
+                            th))
+        val deps =
+          case run_sledgehammer ctxt facts goal of
+            {outcome = NONE, used_facts, ...} => used_facts |> map fst
+          | _ => dependencies_of all_names th
+        val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
+      in File.append path s end
+  in List.app do_thm ths end
+
+fun generate_commands thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -306,18 +351,14 @@
     val parents = parent_thms thy_ths thy
   in fold do_fact new_facts parents; () end
 
-fun generate_meng_paulson_suggestions ctxt thy file_name =
+fun generate_meng_paulson_suggestions ctxt thy max_relevant file_name =
   let
-    val {provers, max_relevant, relevance_thresholds, ...} =
-      Sledgehammer_Isar.default_params ctxt []
-    val prover_name = hd provers
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val facts = non_tautological_facts_of thy
     val (new_facts, old_facts) =
       facts |> List.partition (has_thy thy o snd)
             |>> sort (thm_ord o pairself snd)
-    val i = 1
     fun do_fact (fact as (_, th)) old_facts =
       let
         val name = Thm.get_name_hint th
@@ -327,10 +368,8 @@
           if kind <> "" then
             let
               val suggs =
-                old_facts
-                |> meng_paulson_facts ctxt prover_name (the max_relevant)
-                                      relevance_thresholds goal i
-                |> map (fact_name_of o Thm.get_name_hint o snd)
+                old_facts |> meng_paulson_facts ctxt max_relevant goal
+                          |> map (fact_name_of o fst o fst)
               val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
             in File.append path s end
           else

--- a/src/HOL/TPTP/mash_import.ML	Wed Jul 11 13:59:39 2012 +0200
+++ b/src/HOL/TPTP/mash_import.ML	Wed Jul 11 21:43:19 2012 +0200
@@ -39,15 +39,13 @@
 
 fun import_and_evaluate_mash_suggestions ctxt thy file_name =
   let
-    val params as {provers, max_relevant, relevance_thresholds,
-                   slice, type_enc, lam_trans, timeout, ...} =
+    val {provers, max_relevant, slice, type_enc, lam_trans, timeout, ...} =
       Sledgehammer_Isar.default_params ctxt []
     val prover_name = hd provers
     val path = file_name |> Path.explode
     val lines = path |> File.read_lines
     val facts = non_tautological_facts_of thy
     val all_names = facts |> map (Thm.get_name_hint o snd)
-    val i = 1
     val meng_ok = Unsynchronized.ref 0
     val mash_ok = Unsynchronized.ref 0
     val meng_mash_ok = Unsynchronized.ref 0
@@ -90,19 +88,14 @@
        else
          "Failure: " ^
          (facts |> map (fst o fst)
+                |> take (the max_relevant)
                 |> tag_list 1
                 |> map index_string
                 |> space_implode " "))
     fun run_sh ok heading facts goal =
       let
-        val problem =
-          {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = 1,
-           facts = facts |> take (the max_relevant)
-                         |> map Sledgehammer_Provers.Untranslated_Fact}
-        val prover =
-          Sledgehammer_Run.get_minimizing_prover ctxt
-              Sledgehammer_Provers.Normal prover_name
-        val res as {outcome, ...} = prover params (K (K (K ""))) problem
+        val facts = facts |> take (the max_relevant)
+        val res as {outcome, ...} = run_sledgehammer ctxt facts goal
         val _ = if is_none outcome then ok := !ok + 1 else ()
       in str_of_res heading facts res end
     fun solve_goal j name suggs =
@@ -114,13 +107,12 @@
           | NONE => error ("No fact called \"" ^ name ^ "\"")
         val deps = dependencies_of all_names th
         val goal = goal_of_thm th
-        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
+        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
         val deps_facts = sugg_facts hyp_ts concl_t facts deps
         val meng_facts =
-          meng_paulson_facts ctxt prover_name
-              (max_relevant_slack * the max_relevant) relevance_thresholds goal
-              i facts
+          meng_paulson_facts ctxt (max_relevant_slack * the max_relevant) goal
+                             facts
         val mash_facts = sugg_facts hyp_ts concl_t facts suggs
         val meng_mash_facts = meng_mash_facts meng_facts mash_facts
         val meng_s = run_sh meng_ok mengN meng_facts goal
@@ -142,7 +134,7 @@
       Real.fmt (StringCvt.FIX (SOME 1))
                (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
     val inst_inducts = Config.get ctxt Sledgehammer_Filter.instantiate_inducts
-    val params =
+    val options =
       [prover_name, string_of_int (the max_relevant) ^ " facts",
        "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
        the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
@@ -150,7 +142,7 @@
     val n = length lines
   in
     tracing " * * *";
-    tracing ("Options: " ^ commas params);
+    tracing ("Options: " ^ commas options);
     List.app do_line (tag_list 1 lines);
     ["Successes (of " ^ string_of_int n ^ " goals)",
      total_of mengN meng_ok n,