248 val dummy_phi = AAtom (ATerm (("", []), [])) |
248 val dummy_phi = AAtom (ATerm (("", []), [])) |
249 val dummy_inference = Inference_Source ("", []) |
249 val dummy_inference = Inference_Source ("", []) |
250 |
250 |
251 (* "skip_term" is there to cope with Waldmeister nonsense such as |
251 (* "skip_term" is there to cope with Waldmeister nonsense such as |
252 "theory(equality)". *) |
252 "theory(equality)". *) |
253 val parse_dependency = scan_general_id --| skip_term |
253 fun parse_dependency x = |
254 val parse_dependencies = |
254 (parse_inference_source >> snd |
255 parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency) |
255 || scan_general_id --| skip_term >> single) x |
256 |
256 and parse_dependencies x = |
257 fun parse_source x = |
257 (parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency) |
258 (Scan.this_string "file" |-- $$ "(" |-- scan_general_id -- |
258 >> flat) x |
259 Scan.option ($$ "," |-- scan_general_id) --| $$ ")" |
259 and parse_file_source x = |
260 >> File_Source |
260 (Scan.this_string "file" |-- $$ "(" |-- scan_general_id |
261 || Scan.this_string "inference" |-- $$ "(" |-- scan_general_id |
261 -- Scan.option ($$ "," |-- scan_general_id) --| $$ ")") x |
262 --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "[" |
262 and parse_inference_source x = |
263 -- parse_dependencies --| $$ "]" --| $$ ")" |
263 (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id |
264 >> Inference_Source |
264 --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "[" |
|
265 -- parse_dependencies --| $$ "]" --| $$ ")") x |
|
266 and parse_source x = |
|
267 (parse_file_source >> File_Source |
|
268 || parse_inference_source >> Inference_Source |
265 || skip_term >> K dummy_inference) x |
269 || skip_term >> K dummy_inference) x |
266 |
270 |
267 fun list_app (f, args) = |
271 fun list_app (f, args) = |
268 fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f |
272 fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f |
269 |
273 |