274 Scan.optional ($$ "," |-- parse_annotation false |
274 Scan.optional ($$ "," |-- parse_annotation false |
275 --| Scan.option ($$ "," |-- parse_annotations false)) [] |
275 --| Scan.option ($$ "," |-- parse_annotations false)) [] |
276 |
276 |
277 val vampire_unknown_fact = "unknown" |
277 val vampire_unknown_fact = "unknown" |
278 |
278 |
279 (* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\). |
279 (* Syntax: (cnf|fof|tff)\(<num>, <formula_role>, <formula> <extra_arguments>\). |
280 The <num> could be an identifier, but we assume integers. *) |
280 The <num> could be an identifier, but we assume integers. *) |
281 val parse_tstp_line = |
281 val parse_tstp_line = |
282 ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(") |
282 ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff") |
|
283 -- $$ "(") |
283 |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ "," |
284 |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ "," |
284 -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." |
285 -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." |
285 >> (fn (((num, role), phi), deps) => |
286 >> (fn (((num, role), phi), deps) => |
286 let |
287 let |
287 val (name, deps) = |
288 val (name, deps) = |