437 Vector.sub (spass_names, j - 1) |
437 Vector.sub (spass_names, j - 1) |
438 else |
438 else |
439 [] |
439 [] |
440 | NONE => [] |
440 | NONE => [] |
441 |
441 |
|
442 val parse_spass_debug = |
|
443 Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) |
|
444 --| $$ ")") |
|
445 |
442 (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>. *) |
446 (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>. *) |
443 fun parse_spass_line spass_names = |
447 fun parse_spass_line spass_names = |
444 scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" -- Symbol.scan_id |
448 parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" |
445 -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "." |
449 -- Symbol.scan_id -- parse_spass_annotations --| $$ "]" |
|
450 -- parse_horn_clause --| $$ "." |
446 >> (fn (((num, rule), deps), u) => |
451 >> (fn (((num, rule), deps), u) => |
447 Inference ((num, resolve_spass_num spass_names num), u, rule, |
452 Inference ((num, resolve_spass_num spass_names num), u, rule, |
448 map (swap o `(resolve_spass_num spass_names)) deps)) |
453 map (swap o `(resolve_spass_num spass_names)) deps)) |
449 |
454 |
450 (* Syntax: <name> *) |
455 (* Syntax: <name> *) |