# HG changeset patch
# User blanchet
# Date 1304330973 -7200
# Node ID 8734eb0033b35c5c1a8e68a1d4e5972ad6f46c28
# Parent  aed17803922e71ac50dc09456b1e717023ebcede
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses -- parse these correctly

diff -r aed17803922e -r 8734eb0033b3 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 02 12:09:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 02 12:09:33 2011 +0200
@@ -288,25 +288,29 @@
 
 (* TPTP formulas are fully parenthesized, so we don't need to worry about
    operator precedence. *)
-fun parse_formula x =
-  (($$ "(" |-- parse_formula --| $$ ")"
-    || ($$ "!" >> K AForall || $$ "?" >> K AExists)
-       --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_formula
-       >> (fn ((q, ts), phi) =>
-              (* FIXME: TFF *)
-              AQuant (q, map (rpair NONE o fo_term_head) ts, phi))
-    || (Scan.repeat ($$ "~") >> length)
-       -- ($$ "(" |-- parse_formula --| $$ ")" || parse_atom)
-       >> (fn (n, phi) => phi |> n div 2 = 1 ? mk_anot)
-    || parse_atom)
+fun parse_literal x =
+  ((Scan.repeat ($$ "~") >> length)
+      -- ($$ "(" |-- parse_formula --| $$ ")"
+          || parse_quantified_formula
+          || parse_atom)
+      >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x
+and parse_formula x =
+  (parse_literal
    -- Scan.option ((Scan.this_string "=>" >> K AImplies
                     || Scan.this_string "<=>" >> K AIff
                     || Scan.this_string "<~>" >> K ANotIff
                     || Scan.this_string "<=" >> K AIf
-                    || $$ "|" >> K AOr || $$ "&" >> K AAnd)
+                    || $$ "|" >> K AOr
+                    || $$ "&" >> K AAnd)
                    -- parse_formula)
    >> (fn (phi1, NONE) => phi1
         | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
+and parse_quantified_formula x =
+  (($$ "!" >> K AForall || $$ "?" >> K AExists)
+   --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
+   >> (fn ((q, ts), phi) =>
+          (* FIXME: TFF *)
+          AQuant (q, map (rpair NONE o fo_term_head) ts, phi))) x
 
 val parse_tstp_extra_arguments =
   Scan.optional ($$ "," |-- parse_annotation