# HG changeset patch
# User blanchet
# Date 1360334313 -3600
# Node ID 177db6811f11b93a044b6ef7b7b0c31c3ad5b703
# Parent  69da236d78387766746b2510aa789b0d14338a1f
added markers in proofs identifying origin of proofs, in eval driver

diff -r 69da236d7838 -r 177db6811f11 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Feb 08 12:22:37 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Fri Feb 08 15:38:33 2013 +0100
@@ -83,15 +83,30 @@
       in File.append path s end
   in List.app do_fact facts end
 
-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
+val isar_marker = "$i"
+val omitted_marker = "$o"
+val prover_marker = "$a"
+val prover_failed_marker = "$x"
+
+fun smart_dependencies_of ctxt params_opt facts name_tabs th isar_deps_opt =
+  let
+    val (marker, deps) =
+      case params_opt of
+        SOME (params as {provers = prover :: _, ...}) =>
+        prover_dependencies_of ctxt params prover 0 facts name_tabs th
+        |>> (fn true => prover_marker | false => prover_failed_marker)
+      | NONE =>
+        let
+          val deps =
+            case isar_deps_opt of
+              SOME deps => deps
+            | NONE => isar_dependencies_of name_tabs th
+        in (isar_marker, deps) end
+  in
+    case trim_dependencies th deps of
+      SOME deps => (marker, deps)
+    | NONE => (omitted_marker, [])
+  end
 
 fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
                                          file_name =
@@ -105,10 +120,9 @@
         let
           val name = nickname_of_thm th
           val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
-          val deps =
-            isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
-                                           NONE
-        in encode_str name ^ ": " ^ encode_strs deps ^ "\n" end
+          val (marker, deps) =
+            smart_dependencies_of ctxt params_opt facts name_tabs th NONE
+        in encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" end
       else
         ""
     val lines = Par_List.map do_fact (tag_list 1 facts)
@@ -141,9 +155,9 @@
           val feats =
             features_of ctxt prover (theory_of_thm th) stature [prop_of th]
           val isar_deps = isar_dependencies_of name_tabs th
-          val deps =
-            isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
-                                           (SOME isar_deps)
+          val (marker, deps) =
+            smart_dependencies_of ctxt params_opt facts name_tabs th
+                                  (SOME isar_deps)
           val core =
             encode_str name ^ ": " ^ encode_strs prevs ^ "; " ^
             encode_features (sort_wrt fst feats)
@@ -151,8 +165,7 @@
             if is_bad_query ctxt ho_atp step j th isar_deps then ""
             else "? " ^ core ^ "\n"
           val update =
-            "! " ^ core ^ "; " ^
-            encode_strs (these (trim_dependencies th deps)) ^ "\n"
+            "! " ^ core ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n"
         in query ^ update end
       else
         ""