# HG changeset patch
# User immler@in.tum.de
# Date 1246353662 -7200
# Node ID d262a0d4624653cc92a31b06e212ff9e95d5977c
# Parent  5e97c4abd18e82aae44f188c73c8b8772fd69d43
check for correct proof output

diff -r 5e97c4abd18e -r d262a0d46246 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Jun 30 11:21:02 2009 +0200
@@ -457,9 +457,28 @@
     in  trace msg; msg  end;
 
 
-    
-  (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
-  
+  (*=== EXTRACTING PROOF-TEXT === *)
+
+  val begin_proof_strings = ["# SZS output start CNFRefutation.",
+      "=========== Refutation ==========",
+  "Here is a proof"];
+  val end_proof_strings = ["# SZS output end CNFRefutation",
+      "======= End of refutation =======",
+  "Formulae used in the proof"];
+  fun get_proof_extract proof =
+    let
+    (*splits to_split by the first possible of a list of splitters*)
+    val (begin_string, end_string) =
+      (find_first (fn s => String.isSubstring s proof) begin_proof_strings,
+      find_first (fn s => String.isSubstring s proof) end_proof_strings)
+    in
+      if is_none begin_string orelse is_none end_string
+      then error "Could not extract proof (no substring indicating a proof)"
+      else proof |> first_field (the begin_string) |> the |> snd
+                 |> first_field (the end_string) |> the |> fst end;
+
+(* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
+
   val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
     "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
   val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
@@ -469,31 +488,15 @@
   fun find_failure proof =
     let val failures =
       map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
-         (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
-    in if null failures then NONE else SOME (hd failures) end;
-    
-  (*=== EXTRACTING PROOF-TEXT === *)
-  
-  val begin_proof_strings = ["# SZS output start CNFRefutation.",
-      "=========== Refutation ==========",
-  "Here is a proof"];
-  val end_proof_strings = ["# SZS output end CNFRefutation",
-      "======= End of refutation =======",
-  "Formulae used in the proof"];
-  fun get_proof_extract proof =
-    let
-    (*splits to_split by the first possible of a list of splitters*)
-    fun first_field_any [] to_split = NONE
-      | first_field_any (splitter::splitters) to_split =
-      let
-      val result = (first_field splitter to_split)
-      in
-        if isSome result then result else first_field_any splitters to_split
-      end
-    val (a:string, b:string) = valOf (first_field_any begin_proof_strings proof)
-    val (proofextract:string, c:string) = valOf (first_field_any end_proof_strings b)
-    in proofextract end;
-  
+        (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
+    val correct = null failures andalso
+      exists (fn s => String.isSubstring s proof) begin_proof_strings andalso
+      exists (fn s => String.isSubstring s proof) end_proof_strings
+    in
+      if correct then NONE
+      else if null failures then SOME "Output of ATP not in proper format"
+      else SOME (hd failures) end;
+
   (* === EXTRACTING LEMMAS === *)
   (* lines have the form "cnf(108, axiom, ...",
   the number (108) has to be extracted)*)