450 (Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|" |
450 (Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|" |
451 -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">" |
451 -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">" |
452 -- Scan.repeat parse_decorated_atom |
452 -- Scan.repeat parse_decorated_atom |
453 >> (mk_horn o apfst (op @))) x |
453 >> (mk_horn o apfst (op @))) x |
454 |
454 |
455 fun resolve_spass_num (SOME names) _ _ = names |
|
456 | resolve_spass_num NONE spass_names num = |
|
457 case Int.fromString num of |
|
458 SOME j => if j > 0 andalso j <= Vector.length spass_names then |
|
459 Vector.sub (spass_names, j - 1) |
|
460 else |
|
461 [] |
|
462 | NONE => [] |
|
463 |
|
464 val parse_spass_debug = |
455 val parse_spass_debug = |
465 Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) |
456 Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) |
466 --| $$ ")") |
457 --| $$ ")") |
467 |
458 |
468 (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>. |
459 (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>. |
469 derived from formulae <ident>* *) |
460 derived from formulae <ident>* *) |
470 fun parse_spass_line spass_names = |
461 fun parse_spass_line x = |
471 parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" |
462 (parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" |
472 -- Symbol.scan_id -- parse_spass_annotations --| $$ "]" |
463 -- Symbol.scan_id -- parse_spass_annotations --| $$ "]" |
473 -- parse_horn_clause --| $$ "." |
464 -- parse_horn_clause --| $$ "." |
474 -- Scan.option (Scan.this_string "derived from formulae " |
465 -- Scan.option (Scan.this_string "derived from formulae " |
475 |-- Scan.repeat (scan_general_id --| Scan.option ($$ " "))) |
466 |-- Scan.repeat (scan_general_id --| Scan.option ($$ " "))) |
476 >> (fn ((((num, rule), deps), u), names) => |
467 >> (fn ((((num, rule), deps), u), names) => |
477 Inference_Step ((num, resolve_spass_num names spass_names num), u, |
468 Inference_Step ((num, these names), u, rule, map (rpair []) deps))) x |
478 rule, map (swap o `(resolve_spass_num NONE spass_names)) deps)) |
|
479 |
469 |
480 val satallax_unsat_coreN = "__satallax_unsat_core" (* arbitrary *) |
470 val satallax_unsat_coreN = "__satallax_unsat_core" (* arbitrary *) |
481 |
471 |
482 (* Syntax: <name> *) |
472 (* Syntax: <name> *) |
483 fun parse_satallax_line x = |
473 fun parse_satallax_line x = |
484 (scan_general_id --| Scan.option ($$ " ") |
474 (scan_general_id --| Scan.option ($$ " ") |
485 >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_unsat_coreN, []))) |
475 >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_unsat_coreN, []))) |
486 x |
476 x |
487 |
477 |
488 fun parse_line problem spass_names = |
478 fun parse_line problem = |
489 parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line |
479 parse_tstp_line problem || parse_spass_line || parse_satallax_line |
490 fun parse_proof problem spass_names tstp = |
480 fun parse_proof problem tstp = |
491 tstp |> strip_spaces_except_between_idents |
481 tstp |> strip_spaces_except_between_idents |
492 |> raw_explode |
482 |> raw_explode |
493 |> Scan.finite Symbol.stopper |
483 |> Scan.finite Symbol.stopper |
494 (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) |
484 (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) |
495 (Scan.repeat1 (parse_line problem spass_names)))) |
485 (Scan.repeat1 (parse_line problem)))) |
496 |> fst |
486 |> fst |
497 |
|
498 (** SPASS's FLOTTER hack **) |
|
499 |
|
500 (* This is a hack required for keeping track of facts after they have been |
|
501 clausified by SPASS's FLOTTER preprocessor. The "ATP/scripts/spass" script is |
|
502 also part of this hack. *) |
|
503 |
|
504 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" |
|
505 |
|
506 fun extract_clause_sequence output = |
|
507 let |
|
508 val tokens_of = String.tokens (not o Char.isAlphaNum) |
|
509 fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss) |
|
510 | extract_num _ = NONE |
|
511 in output |> split_lines |> map_filter (extract_num o tokens_of) end |
|
512 |
|
513 fun is_head_digit s = Char.isDigit (String.sub (s, 0)) |
|
514 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) |
|
515 |
|
516 val parse_clause_formula_pair = |
|
517 $$ "(" |-- scan_integer --| $$ "," |
|
518 -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")" |
|
519 --| Scan.option ($$ ",") |
|
520 val parse_clause_formula_relation = |
|
521 Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" |
|
522 |-- Scan.repeat parse_clause_formula_pair |
|
523 val extract_clause_formula_relation = |
|
524 Substring.full #> Substring.position set_ClauseFormulaRelationN |
|
525 #> snd #> Substring.position "." #> fst #> Substring.string |
|
526 #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation |
|
527 #> fst |
|
528 |
|
529 fun extract_spass_name_vector output = |
|
530 (if String.isSubstring set_ClauseFormulaRelationN output then |
|
531 let |
|
532 val num_seq = extract_clause_sequence output |
|
533 val name_map = extract_clause_formula_relation output |
|
534 val name_seq = num_seq |> map (these o AList.lookup (op =) name_map) |
|
535 in name_seq end |
|
536 else |
|
537 []) |
|
538 |> Vector.fromList |
|
539 |
487 |
540 fun atp_proof_from_tstplike_proof _ _ "" = [] |
488 fun atp_proof_from_tstplike_proof _ _ "" = [] |
541 | atp_proof_from_tstplike_proof problem output tstp = |
489 | atp_proof_from_tstplike_proof problem output tstp = |
542 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |
490 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |
543 |> parse_proof problem (extract_spass_name_vector output) |
491 |> parse_proof problem |
544 |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *) |
492 |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *) |
545 |
493 |
546 fun clean_up_dependencies _ [] = [] |
494 fun clean_up_dependencies _ [] = [] |
547 | clean_up_dependencies seen |
495 | clean_up_dependencies seen |
548 ((step as Definition_Step (name, _, _)) :: steps) = |
496 ((step as Definition_Step (name, _, _)) :: steps) = |