# HG changeset patch # User blanchet # Date 1304291114 -7200 # Node ID 62398fdbb5287f2cc4525ea4dca43404f5655ea2 # Parent f9d7f1331a00f48a6901fce9666713d12adf5b5a fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs diff -r f9d7f1331a00 -r 62398fdbb528 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Sun May 01 22:36:58 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Mon May 02 01:05:14 2011 +0200 @@ -250,15 +250,15 @@ >> (fn (ss1, ss2) => implode ss1 ^ implode ss2) (* Generalized first-order terms, which include file names, numbers, etc. *) -fun parse_annotation strict x = +fun parse_annotation x = ((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id) - >> (strict ? filter (is_some o Int.fromString))) - -- Scan.optional (parse_annotation strict) [] >> op @ - || $$ "(" |-- parse_annotations strict --| $$ ")" - || $$ "[" |-- parse_annotations strict --| $$ "]") x -and parse_annotations strict x = - (Scan.optional (parse_annotation strict - ::: Scan.repeat ($$ "," |-- parse_annotation strict)) [] + >> filter (is_some o Int.fromString)) + -- Scan.optional parse_annotation [] >> op @ + || $$ "(" |-- parse_annotations --| $$ ")" + || $$ "[" |-- parse_annotations --| $$ "]") x +and parse_annotations x = + (Scan.optional (parse_annotation + ::: Scan.repeat ($$ "," |-- parse_annotation)) [] >> flat) x (* Vampire proof lines sometimes contain needless information such as "(0:3)", @@ -295,7 +295,9 @@ >> (fn ((q, ts), phi) => (* FIXME: TFF *) AQuant (q, map (rpair NONE o fo_term_head) ts, phi)) - || $$ "~" |-- ($$ "(" |-- parse_formula --| $$ ")" || parse_atom) >> mk_anot + || (Scan.repeat ($$ "~") >> length) + -- ($$ "(" |-- parse_formula --| $$ ")" || parse_atom) + >> (fn (n, phi) => phi |> n div 2 = 1 ? mk_anot) || parse_atom) -- Scan.option ((Scan.this_string "=>" >> K AImplies || Scan.this_string "<=>" >> K AIff @@ -307,8 +309,8 @@ | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x val parse_tstp_extra_arguments = - Scan.optional ($$ "," |-- parse_annotation false - --| Scan.option ($$ "," |-- parse_annotations false)) [] + Scan.optional ($$ "," |-- parse_annotation + --| Scan.option ($$ "," |-- parse_annotations)) [] val vampire_unknown_fact = "unknown" val tofof_fact_prefix = "fof_" @@ -355,7 +357,7 @@ scan_general_id --| $$ "." -- parse_formula --| Scan.option parse_vampire_braced_stuff --| Scan.option parse_vampire_parenthesized_detritus - -- parse_annotation true + -- parse_annotation >> (fn ((num, phi), deps) => Inference ((num, NONE), phi, map (rpair NONE) deps))