equal
deleted
inserted
replaced
258 (Scan.this_string "introduced" |-- $$ "(" |-- skip_term --| $$ ")") x |
258 (Scan.this_string "introduced" |-- $$ "(" |-- skip_term --| $$ ")") x |
259 and parse_source x = |
259 and parse_source x = |
260 (parse_file_source >> File_Source |
260 (parse_file_source >> File_Source |
261 || parse_inference_source >> Inference_Source |
261 || parse_inference_source >> Inference_Source |
262 || skip_introduced >> K dummy_inference (* for Vampire *) |
262 || skip_introduced >> K dummy_inference (* for Vampire *) |
263 || scan_nat >> (fn s => Inference_Source ("", [s])) (* for E *) |
263 || scan_general_id >> (fn s => Inference_Source ("", [s])) (* for E *) |
264 || skip_term >> K dummy_inference) x |
264 || skip_term >> K dummy_inference) x |
265 |
265 |
266 fun list_app (f, args) = |
266 fun list_app (f, args) = |
267 fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f |
267 fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f |
268 |
268 |
504 fun atp_proof_of_tstplike_proof _ "" = [] |
504 fun atp_proof_of_tstplike_proof _ "" = [] |
505 | atp_proof_of_tstplike_proof problem tstp = |
505 | atp_proof_of_tstplike_proof problem tstp = |
506 case core_of_agsyhol_proof tstp of |
506 case core_of_agsyhol_proof tstp of |
507 SOME facts => facts |> map (core_inference agsyhol_coreN) |
507 SOME facts => facts |> map (core_inference agsyhol_coreN) |
508 | NONE => |
508 | NONE => |
509 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |
509 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |
510 |> parse_proof problem |
510 |> parse_proof problem |
511 |> perhaps (try (sort (vampire_step_name_ord o pairself #1))) |
511 |> perhaps (try (sort (vampire_step_name_ord o pairself #1))) |
512 |
512 |
513 fun clean_up_dependencies _ [] = [] |
513 fun clean_up_dependencies _ [] = [] |
514 | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) = |
514 | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) = |