# HG changeset patch
# User blanchet
# Date 1305888479 -7200
# Node ID 391e41ac038b6efa1632c7ecdd0b37eb61fbb676
# Parent  dbdfe2d5b6ab6c2c6c1d453fe994ddef96377eec
make sure the Vampire incomplete proof detection code kicks in

diff -r dbdfe2d5b6ab -r 391e41ac038b src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri May 20 12:47:59 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri May 20 12:47:59 2011 +0200
@@ -15,6 +15,7 @@
     Unprovable |
     IncompleteUnprovable |
     ProofMissing |
+    ProofIncomplete |
     UnsoundProof of bool * string list |
     CantConnect |
     TimedOut |
@@ -64,6 +65,7 @@
   Unprovable |
   IncompleteUnprovable |
   ProofMissing |
+  ProofIncomplete |
   UnsoundProof of bool * string list |
   CantConnect |
   TimedOut |
@@ -126,6 +128,9 @@
     "The prover gave up."
   | string_for_failure ProofMissing =
     "The prover claims the conjecture is a theorem but did not provide a proof."
+  | string_for_failure ProofIncomplete =
+    "The prover claims the conjecture is a theorem but provided an incomplete \
+    \proof."
   | string_for_failure (UnsoundProof (false, ss)) =
     "The prover found a type-unsound proof " ^ involving ss ^
     "(or, less likely, your axioms are inconsistent). Try passing the \
@@ -199,18 +204,16 @@
 
 fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims
                                        known_failures output =
-   case extract_tstplike_proof proof_delims output of
-     "" =>
-     ("", SOME (if res_code = 0 andalso output = "" then
-                  ProofMissing
-                else case extract_known_failure known_failures output of
-                  SOME failure =>
-                  if failure = IncompleteUnprovable andalso complete then
-                    Unprovable
-                  else
-                    failure
-                | NONE => UnknownError (short_output verbose output)))
-   | tstplike_proof => (tstplike_proof, NONE)
+  case (extract_tstplike_proof proof_delims output,
+        extract_known_failure known_failures output) of
+    (_, SOME ProofIncomplete) => ("", SOME ProofIncomplete)
+  | ("", SOME failure) =>
+    ("", SOME (if failure = IncompleteUnprovable andalso complete then Unprovable
+               else failure))
+  | ("", NONE) =>
+    ("", SOME (if res_code = 0 andalso output = "" then ProofMissing
+               else UnknownError (short_output verbose output)))
+  | (tstplike_proof, _) => (tstplike_proof, NONE)
 
 fun mk_anot (AConn (ANot, [phi])) = phi
   | mk_anot phi = AConn (ANot, [phi])
diff -r dbdfe2d5b6ab -r 391e41ac038b src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri May 20 12:47:59 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri May 20 12:47:59 2011 +0200
@@ -292,7 +292,7 @@
      [(Unprovable, "UNPROVABLE"),
       (IncompleteUnprovable, "CANNOT PROVE"),
       (IncompleteUnprovable, "SZS status GaveUp"),
-      (ProofMissing, "predicate_definition_introduction,[]"),
+      (ProofIncomplete, "predicate_definition_introduction,[]"),
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
diff -r dbdfe2d5b6ab -r 391e41ac038b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 20 12:47:59 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 20 12:47:59 2011 +0200
@@ -677,9 +677,11 @@
         NONE =>
         (NONE, proof_text isar_proof isar_params metis_params
                |>> append_to_message)
-      | SOME ProofMissing =>
-        (NONE, metis_proof_text metis_params |>> append_to_message)
-      | SOME failure => (outcome, (string_for_failure failure, []))
+      | SOME failure =>
+        if failure = ProofMissing orelse failure = ProofIncomplete then
+          (NONE, metis_proof_text metis_params |>> append_to_message)
+        else
+          (outcome, (string_for_failure failure, []))
   in
     {outcome = outcome, message = message, used_facts = used_facts,
      run_time_in_msecs = msecs}