equal
deleted
inserted
replaced
53 val is_same_atp_step : step_name -> step_name -> bool |
53 val is_same_atp_step : step_name -> step_name -> bool |
54 val scan_general_id : string list -> string * string list |
54 val scan_general_id : string list -> string * string list |
55 val satallax_unsat_coreN : string |
55 val satallax_unsat_coreN : string |
56 val parse_formula : |
56 val parse_formula : |
57 string list -> (string, 'a, (string, 'a) ho_term) formula * string list |
57 string list -> (string, 'a, (string, 'a) ho_term) formula * string list |
58 val atp_proof_from_tstplike_proof : |
58 val atp_proof_from_tstplike_proof : string problem -> string -> string proof |
59 string problem -> string -> string -> string proof |
|
60 val clean_up_atp_proof_dependencies : string proof -> string proof |
59 val clean_up_atp_proof_dependencies : string proof -> string proof |
61 val map_term_names_in_atp_proof : |
60 val map_term_names_in_atp_proof : |
62 (string -> string) -> string proof -> string proof |
61 (string -> string) -> string proof -> string proof |
63 val nasty_atp_proof : string Symtab.table -> string proof -> string proof |
62 val nasty_atp_proof : string Symtab.table -> string proof -> string proof |
64 end; |
63 end; |
483 |> Scan.finite Symbol.stopper |
482 |> Scan.finite Symbol.stopper |
484 (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) |
483 (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) |
485 (Scan.repeat1 (parse_line problem)))) |
484 (Scan.repeat1 (parse_line problem)))) |
486 |> fst |
485 |> fst |
487 |
486 |
488 fun atp_proof_from_tstplike_proof _ _ "" = [] |
487 fun atp_proof_from_tstplike_proof _ "" = [] |
489 | atp_proof_from_tstplike_proof problem output tstp = |
488 | atp_proof_from_tstplike_proof problem tstp = |
490 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |
489 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |
491 |> parse_proof problem |
490 |> parse_proof problem |
492 |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *) |
491 |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *) |
493 |
492 |
494 fun clean_up_dependencies _ [] = [] |
493 fun clean_up_dependencies _ [] = [] |