# HG changeset patch
# User blanchet
# Date 1343292483 -7200
# Node ID 716ec3458b1dedc28bb34de0e036556faba429bb
# Parent  af1dabad14c0c3c7f0434b15d683d7019bbf1a77
generate fact name in queries again + use ATP dependencies when possible

diff -r af1dabad14c0 -r 716ec3458b1d src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 25 23:02:50 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jul 26 10:48:03 2012 +0200
@@ -23,7 +23,6 @@
 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
 val prover = hd provers
 *}
-
 ML {*
 if do_it then
   generate_accessibility thy false "/tmp/mash_accessibility"
@@ -47,7 +46,7 @@
 
 ML {*
 if do_it then
-  generate_commands @{context} prover thy "/tmp/mash_commands"
+  generate_commands @{context} params thy "/tmp/mash_commands"
 else
   ()
 *}
diff -r af1dabad14c0 -r 716ec3458b1d src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Wed Jul 25 23:02:50 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Thu Jul 26 10:48:03 2012 +0200
@@ -16,7 +16,7 @@
     theory -> bool -> string -> unit
   val generate_atp_dependencies :
     Proof.context -> params -> theory -> bool -> string -> unit
-  val generate_commands : Proof.context -> string -> theory -> string -> unit
+  val generate_commands : Proof.context -> params -> theory -> string -> unit
   val generate_mepo_suggestions :
     Proof.context -> params -> theory -> int -> string -> unit
 end;
@@ -51,6 +51,11 @@
 
 val all_names = map (rpair () o nickname_of) #> Symtab.make
 
+fun smart_dependencies_of ctxt params prover facts all_names th =
+  case atp_dependencies_of ctxt params prover 0 facts all_names th of
+    SOME deps => deps
+  | NONE => isar_dependencies_of all_names th |> these
+
 fun generate_accessibility thy include_thy file_name =
   let
     val path = file_name |> Path.explode
@@ -119,18 +124,16 @@
     fun do_thm th =
       let
         val name = nickname_of th
-        val deps =
-          case atp_dependencies_of ctxt params prover 0 facts all_names th of
-            SOME deps => deps
-          | NONE => isar_dependencies_of all_names th |> these
+        val deps = smart_dependencies_of ctxt params prover facts all_names th
         val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
       in File.append path s end
   in List.app do_thm ths end
 
-fun generate_commands ctxt prover thy file_name =
+fun generate_commands ctxt (params as {provers, ...}) thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
+    val prover = hd provers
     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val facts = all_facts_of (Proof_Context.init_global thy) css_table
     val (new_facts, old_facts) =
@@ -142,13 +145,13 @@
       let
         val name = nickname_of th
         val feats = features_of ctxt prover thy stature [prop_of th]
-        val deps = isar_dependencies_of all_names th |> these
+        val deps = smart_dependencies_of ctxt params prover facts all_names th
         val kind = Thm.legacy_get_kind th
-        val core = escape_metas prevs ^ "; " ^ escape_metas feats
+        val core =
+          escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
+          escape_metas feats
         val query = if kind <> "" then "? " ^ core ^ "\n" else ""
-        val update =
-          "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^
-          escape_metas deps ^ "\n"
+        val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
         val _ = File.append path (query ^ update)
       in [name] end
     val thy_map = old_facts |> thy_map_from_facts