# HG changeset patch
# User blanchet
# Date 1357490309 -3600
# Node ID 74a6adcb96ac52739d677157b8c96369249e1412
# Parent  1253fd12ca8a616a0d1f195e1509320d8f9d25f8
also generate queries for goals with too many Isar dependencies

diff -r 1253fd12ca8a -r 74a6adcb96ac src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Sun Jan 06 12:44:45 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Sun Jan 06 17:38:29 2013 +0100
@@ -79,7 +79,7 @@
             | NONE => error ("No fact called \"" ^ name ^ "\".")
           val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
-          val isar_deps = isar_dependencies_of name_tabs th |> these
+          val isar_deps = isar_dependencies_of name_tabs th
           val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
           val mepo_facts =
             mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts
diff -r 1253fd12ca8a -r 74a6adcb96ac src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Sun Jan 06 12:44:45 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Sun Jan 06 17:38:29 2013 +0100
@@ -81,14 +81,13 @@
 
 fun isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
                                    isar_deps_opt =
-  (case params_opt of
-     SOME (params as {provers = prover :: _, ...}) =>
-     prover_dependencies_of ctxt params prover 0 facts name_tabs th |> snd
-   | NONE =>
-     case isar_deps_opt of
-       SOME deps => deps
-     | NONE => isar_dependencies_of name_tabs th)
-  |> these
+  case params_opt of
+    SOME (params as {provers = prover :: _, ...}) =>
+    prover_dependencies_of ctxt params prover 0 facts name_tabs th |> snd
+  | NONE =>
+    case isar_deps_opt of
+      SOME deps => deps
+    | NONE => isar_dependencies_of name_tabs th
 
 fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
                                          file_name =
@@ -143,9 +142,11 @@
             escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
             encode_features (sort_wrt fst feats)
           val query =
-            if is_bad_query ctxt ho_atp th (these isar_deps) then ""
+            if is_bad_query ctxt ho_atp th isar_deps then ""
             else "? " ^ core ^ "\n"
-          val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
+          val update =
+            "! " ^ core ^ "; " ^
+            escape_metas (these (trim_dependencies th deps)) ^ "\n"
         in query ^ update end
       else
         ""
@@ -177,7 +178,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 (these isar_deps) then
+        if is_bad_query ctxt ho_atp th isar_deps then
           ""
         else
           let
diff -r 1253fd12ca8a -r 74a6adcb96ac src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Jan 06 12:44:45 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Jan 06 17:38:29 2013 +0100
@@ -59,12 +59,13 @@
   val features_of :
     Proof.context -> string -> theory -> stature -> term list
     -> (string * real) list
+  val trim_dependencies : thm -> string list -> string list option
   val isar_dependencies_of :
-    string Symtab.table * string Symtab.table -> thm -> string list option
+    string Symtab.table * string Symtab.table -> thm -> string list
   val prover_dependencies_of :
     Proof.context -> params -> string -> int -> fact list
     -> string Symtab.table * string Symtab.table -> thm
-    -> bool * string list option
+    -> bool * string list
   val weight_mash_facts : 'a list -> ('a * real) list
   val find_mash_suggestions :
     int -> (Symtab.key * 'a) list -> ('b * thm) list -> ('b * thm) list
@@ -645,13 +646,12 @@
           else
             deps)
 
-fun isar_dependencies_of name_tabs th =
-  th |> thms_in_proof (SOME name_tabs) |> trim_dependencies th
+val isar_dependencies_of = thms_in_proof o SOME
 
 fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
                            auto_level facts name_tabs th =
   case isar_dependencies_of name_tabs th of
-    SOME [] => (false, SOME [])
+    [] => (false, [])
   | isar_deps =>
     let
       val thy = Proof_Context.theory_of ctxt
@@ -672,7 +672,7 @@
         |> mepo_suggested_facts ctxt params prover
                (max_facts |> the_default prover_dependency_default_max_facts)
                NONE hyp_ts concl_t
-        |> fold (add_isar_dep facts) (these isar_deps)
+        |> fold (add_isar_dep facts) isar_deps
         |> map nickify
     in
       if verbose andalso auto_level = 0 then
@@ -694,9 +694,7 @@
            end
          else
            ();
-         case used_facts |> map fst |> trim_dependencies th of
-           NONE => (false, isar_deps)
-         | prover_deps => (true, prover_deps))
+         (true, map fst used_facts))
       | _ => (false, isar_deps)
     end
 
@@ -880,9 +878,11 @@
           else if run_prover then
             prover_dependencies_of ctxt params prover auto_level facts name_tabs
                                    th
-            |> (fn (false, _) => NONE | (true, deps) => deps)
+            |> (fn (false, _) => NONE
+                 | (true, deps) => trim_dependencies th deps)
           else
             isar_dependencies_of name_tabs th
+            |> trim_dependencies th
         fun do_commit [] [] [] state = state
           | do_commit learns relearns flops {access_G, dirty} =
             let
@@ -987,9 +987,7 @@
                      Isar_Proof => 0
                    | Automatic_Proof => 2 * max_isar
                    | Isar_Proof_wegen_Prover_Flop => max_isar)
-                - 500 * (th |> isar_dependencies_of name_tabs
-                            |> Option.map length
-                            |> the_default max_dependencies)
+                - 500 * length (isar_dependencies_of name_tabs th)
               val old_facts =
                 old_facts |> map (`priority_of)
                           |> sort (int_ord o pairself fst)