34 UnknownError of string |
34 UnknownError of string |
35 |
35 |
36 type step_name = string * string list |
36 type step_name = string * string list |
37 |
37 |
38 datatype 'a step = |
38 datatype 'a step = |
39 Definition of step_name * 'a * 'a | |
39 Definition_Step of step_name * 'a * 'a | |
40 Inference of step_name * 'a * string * step_name list |
40 Inference_Step of step_name * 'a * string * step_name list |
41 |
41 |
42 type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list |
42 type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list |
43 |
43 |
44 val short_output : bool -> string -> string |
44 val short_output : bool -> string -> string |
45 val string_for_failure : failure -> string |
45 val string_for_failure : failure -> string |
205 | (SOME _, NONE) => GREATER |
205 | (SOME _, NONE) => GREATER |
206 | (SOME i, SOME j) => int_ord (i, j) |
206 | (SOME i, SOME j) => int_ord (i, j) |
207 end |
207 end |
208 |
208 |
209 datatype 'a step = |
209 datatype 'a step = |
210 Definition of step_name * 'a * 'a | |
210 Definition_Step of step_name * 'a * 'a | |
211 Inference of step_name * 'a * string * step_name list |
211 Inference_Step of step_name * 'a * string * step_name list |
212 |
212 |
213 type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list |
213 type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list |
214 |
214 |
215 fun step_name (Definition (name, _, _)) = name |
215 fun step_name (Definition_Step (name, _, _)) = name |
216 | step_name (Inference (name, _, _, _)) = name |
216 | step_name (Inference_Step (name, _, _, _)) = name |
217 |
217 |
218 (**** PARSING OF TSTP FORMAT ****) |
218 (**** PARSING OF TSTP FORMAT ****) |
219 |
219 |
220 (* FIXME: temporary hack *) |
220 (* FIXME: temporary hack *) |
221 fun repair_waldmeister_step_name s = |
221 fun repair_waldmeister_step_name s = |
393 in |
393 in |
394 case role of |
394 case role of |
395 "definition" => |
395 "definition" => |
396 (case phi of |
396 (case phi of |
397 AConn (AIff, [phi1 as AAtom _, phi2]) => |
397 AConn (AIff, [phi1 as AAtom _, phi2]) => |
398 Definition (name, phi1, phi2) |
398 Definition_Step (name, phi1, phi2) |
399 | AAtom (ATerm ("equal", _)) => |
399 | AAtom (ATerm ("equal", _)) => |
400 (* Vampire's equality proxy axiom *) |
400 (* Vampire's equality proxy axiom *) |
401 Inference (name, phi, rule, map (rpair []) deps) |
401 Inference_Step (name, phi, rule, map (rpair []) deps) |
402 | _ => raise UNRECOGNIZED_ATP_PROOF ()) |
402 | _ => raise UNRECOGNIZED_ATP_PROOF ()) |
403 | _ => Inference (name, phi, rule, map (rpair []) deps) |
403 | _ => Inference_Step (name, phi, rule, map (rpair []) deps) |
404 end) |
404 end) |
405 |
405 |
406 (**** PARSING OF SPASS OUTPUT ****) |
406 (**** PARSING OF SPASS OUTPUT ****) |
407 |
407 |
408 (* SPASS returns clause references of the form "x.y". We ignore "y", whose role |
408 (* SPASS returns clause references of the form "x.y". We ignore "y", whose role |
451 -- Symbol.scan_id -- parse_spass_annotations --| $$ "]" |
451 -- Symbol.scan_id -- parse_spass_annotations --| $$ "]" |
452 -- parse_horn_clause --| $$ "." |
452 -- parse_horn_clause --| $$ "." |
453 -- Scan.option (Scan.this_string "derived from formulae " |
453 -- Scan.option (Scan.this_string "derived from formulae " |
454 |-- Scan.repeat (scan_general_id --| Scan.option ($$ " "))) |
454 |-- Scan.repeat (scan_general_id --| Scan.option ($$ " "))) |
455 >> (fn ((((num, rule), deps), u), names) => |
455 >> (fn ((((num, rule), deps), u), names) => |
456 Inference ((num, resolve_spass_num names spass_names num), u, rule, |
456 Inference_Step ((num, resolve_spass_num names spass_names num), u, |
457 map (swap o `(resolve_spass_num NONE spass_names)) deps)) |
457 rule, map (swap o `(resolve_spass_num NONE spass_names)) deps)) |
458 |
458 |
459 (* Syntax: <name> *) |
459 (* Syntax: <name> *) |
460 fun parse_satallax_line x = |
460 fun parse_satallax_line x = |
461 (scan_general_id --| Scan.option ($$ " ") |
461 (scan_general_id --| Scan.option ($$ " ") |
462 >> (fn s => Inference ((s, [s]), dummy_phi, "", []))) x |
462 >> (fn s => Inference_Step ((s, [s]), dummy_phi, "", []))) x |
463 |
463 |
464 fun parse_line problem spass_names = |
464 fun parse_line problem spass_names = |
465 parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line |
465 parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line |
466 fun parse_proof problem spass_names tstp = |
466 fun parse_proof problem spass_names tstp = |
467 tstp |> strip_spaces_except_between_idents |
467 tstp |> strip_spaces_except_between_idents |
518 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |
518 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |
519 |> parse_proof problem (extract_spass_name_vector output) |
519 |> parse_proof problem (extract_spass_name_vector output) |
520 |> sort (step_name_ord o pairself step_name) |
520 |> sort (step_name_ord o pairself step_name) |
521 |
521 |
522 fun clean_up_dependencies _ [] = [] |
522 fun clean_up_dependencies _ [] = [] |
523 | clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) = |
523 | clean_up_dependencies seen |
|
524 ((step as Definition_Step (name, _, _)) :: steps) = |
524 step :: clean_up_dependencies (name :: seen) steps |
525 step :: clean_up_dependencies (name :: seen) steps |
525 | clean_up_dependencies seen (Inference (name, u, rule, deps) :: steps) = |
526 | clean_up_dependencies seen (Inference_Step (name, u, rule, deps) :: steps) = |
526 Inference (name, u, rule, |
527 Inference_Step (name, u, rule, |
527 map_filter (fn dep => find_first (is_same_atp_step dep) seen) |
528 map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) :: |
528 deps) :: |
|
529 clean_up_dependencies (name :: seen) steps |
529 clean_up_dependencies (name :: seen) steps |
530 |
530 |
531 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof |
531 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof |
532 |
532 |
533 fun map_term_names_in_term f (ATerm (s, ts)) = |
533 fun map_term_names_in_term f (ATerm (s, ts)) = |
535 fun map_term_names_in_formula f (AQuant (q, xs, phi)) = |
535 fun map_term_names_in_formula f (AQuant (q, xs, phi)) = |
536 AQuant (q, xs, map_term_names_in_formula f phi) |
536 AQuant (q, xs, map_term_names_in_formula f phi) |
537 | map_term_names_in_formula f (AConn (c, phis)) = |
537 | map_term_names_in_formula f (AConn (c, phis)) = |
538 AConn (c, map (map_term_names_in_formula f) phis) |
538 AConn (c, map (map_term_names_in_formula f) phis) |
539 | map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t) |
539 | map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t) |
540 fun map_term_names_in_step f (Definition (name, phi1, phi2)) = |
540 fun map_term_names_in_step f (Definition_Step (name, phi1, phi2)) = |
541 Definition (name, map_term_names_in_formula f phi1, |
541 Definition_Step (name, map_term_names_in_formula f phi1, |
542 map_term_names_in_formula f phi2) |
542 map_term_names_in_formula f phi2) |
543 | map_term_names_in_step f (Inference (name, phi, rule, deps)) = |
543 | map_term_names_in_step f (Inference_Step (name, phi, rule, deps)) = |
544 Inference (name, map_term_names_in_formula f phi, rule, deps) |
544 Inference_Step (name, map_term_names_in_formula f phi, rule, deps) |
545 fun map_term_names_in_atp_proof f = map (map_term_names_in_step f) |
545 fun map_term_names_in_atp_proof f = map (map_term_names_in_step f) |
546 |
546 |
547 fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s |
547 fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s |
548 fun nasty_atp_proof pool = |
548 fun nasty_atp_proof pool = |
549 if Symtab.is_empty pool then I |
549 if Symtab.is_empty pool then I |