305 || parse_quantified_formula |
305 || parse_quantified_formula |
306 || parse_atom) |
306 || parse_atom) |
307 >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x |
307 >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x |
308 and parse_formula x = |
308 and parse_formula x = |
309 (parse_literal |
309 (parse_literal |
310 -- Scan.option ((Scan.this_string tptp_implies >> K AImplies |
310 -- Scan.option ((Scan.this_string tptp_implies |
311 || Scan.this_string tptp_iff >> K AIff |
311 || Scan.this_string tptp_iff |
312 || Scan.this_string tptp_not_iff >> K ANotIff |
312 || Scan.this_string tptp_not_iff |
313 || Scan.this_string tptp_if >> K AIf |
313 || Scan.this_string tptp_if |
314 || $$ tptp_or >> K AOr |
314 || $$ tptp_or |
315 || $$ tptp_and >> K AAnd) |
315 || $$ tptp_and) -- parse_formula) |
316 -- parse_formula) |
|
317 >> (fn (phi1, NONE) => phi1 |
316 >> (fn (phi1, NONE) => phi1 |
318 | (phi1, SOME (c, phi2)) => mk_aconn c phi1 phi2)) x |
317 | (phi1, SOME (c, phi2)) => |
|
318 if c = tptp_implies then mk_aconn AImplies phi1 phi2 |
|
319 else if c = tptp_iff then mk_aconn AIff phi1 phi2 |
|
320 else if c = tptp_not_iff then mk_anot (mk_aconn AIff phi1 phi2) |
|
321 else if c = tptp_if then mk_aconn AImplies phi2 phi1 |
|
322 else if c = tptp_or then mk_aconn AOr phi1 phi2 |
|
323 else if c = tptp_and then mk_aconn AAnd phi1 phi2 |
|
324 else raise Fail ("impossible connective " ^ quote c))) x |
319 and parse_quantified_formula x = |
325 and parse_quantified_formula x = |
320 (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) |
326 (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) |
321 --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal |
327 --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal |
322 >> (fn ((q, ts), phi) => |
328 >> (fn ((q, ts), phi) => |
323 (* We ignore TFF and THF types for now. *) |
329 (* We ignore TFF and THF types for now. *) |