equal
deleted
inserted
replaced
208 fun step_name (Definition (name, _, _)) = name |
208 fun step_name (Definition (name, _, _)) = name |
209 | step_name (Inference (name, _, _)) = name |
209 | step_name (Inference (name, _, _)) = name |
210 |
210 |
211 (**** PARSING OF TSTP FORMAT ****) |
211 (**** PARSING OF TSTP FORMAT ****) |
212 |
212 |
213 (*Strings enclosed in single quotes, e.g. filenames*) |
213 (* Strings enclosed in single quotes (e.g., file names) *) |
214 val scan_general_id = |
214 val scan_general_id = |
215 $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode |
215 $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode |
216 || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig |
216 || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig |
217 >> (fn (ss1, ss2) => implode ss1 ^ implode ss2) |
217 >> (fn (ss1, ss2) => implode ss1 ^ implode ss2) |
218 |
218 |
275 val parse_tstp_extra_arguments = |
275 val parse_tstp_extra_arguments = |
276 Scan.optional ($$ "," |-- parse_annotation false |
276 Scan.optional ($$ "," |-- parse_annotation false |
277 --| Scan.option ($$ "," |-- parse_annotations false)) [] |
277 --| Scan.option ($$ "," |-- parse_annotations false)) [] |
278 |
278 |
279 val vampire_unknown_fact = "unknown" |
279 val vampire_unknown_fact = "unknown" |
|
280 val tofof_fact_prefix = "fof_" |
280 |
281 |
281 (* Syntax: (cnf|fof|tff)\(<num>, <formula_role>, <formula> <extra_arguments>\). |
282 (* Syntax: (cnf|fof|tff)\(<num>, <formula_role>, <formula> <extra_arguments>\). |
282 The <num> could be an identifier, but we assume integers. *) |
283 The <num> could be an identifier, but we assume integers. *) |
283 val parse_tstp_line = |
284 val parse_tstp_line = |
284 ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff") |
285 ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff") |
288 >> (fn (((num, role), phi), deps) => |
289 >> (fn (((num, role), phi), deps) => |
289 let |
290 let |
290 val (name, deps) = |
291 val (name, deps) = |
291 case deps of |
292 case deps of |
292 ["file", _, s] => |
293 ["file", _, s] => |
293 ((num, if s = vampire_unknown_fact then NONE else SOME s), []) |
294 ((num, |
|
295 if s = vampire_unknown_fact then NONE |
|
296 else SOME (s |> perhaps (try (unprefix tofof_fact_prefix)))), |
|
297 []) |
294 | _ => ((num, NONE), deps) |
298 | _ => ((num, NONE), deps) |
295 in |
299 in |
296 case role of |
300 case role of |
297 "definition" => |
301 "definition" => |
298 (case phi of |
302 (case phi of |