256 || scan_general_id >> (fn s => Inference_Source ("", [s])) (* for E *) |
256 || scan_general_id >> (fn s => Inference_Source ("", [s])) (* for E *) |
257 || skip_term >> K dummy_inference) x |
257 || skip_term >> K dummy_inference) x |
258 |
258 |
259 fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f |
259 fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f |
260 |
260 |
261 fun parse_sort x = scan_general_id x |
261 fun parse_class x = scan_general_id x |
262 and parse_sorts x = (parse_sort ::: Scan.repeat ($$ "&" |-- parse_sort)) x |
262 and parse_classes x = (parse_class ::: Scan.repeat ($$ "&" |-- parse_class)) x |
263 |
263 |
264 fun parse_type x = |
264 fun parse_type x = |
265 (scan_general_id --| Scan.option ($$ "{" |-- parse_sorts --| $$ "}") |
265 (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") [] |
266 -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") [] |
266 -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") [] |
267 >> AType) x |
267 >> AType) x |
268 and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x |
268 and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x |
269 |
269 |
270 (* We currently ignore TFF and THF types. *) |
270 (* We currently ignore TFF and THF types. *) |
528 |
528 |
529 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof |
529 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof |
530 |
530 |
531 fun map_term_names_in_atp_proof f = |
531 fun map_term_names_in_atp_proof f = |
532 let |
532 let |
533 fun map_type (AType (s, tys)) = AType (f s, map map_type tys) |
533 fun map_type (AType ((s, clss), tys)) = AType ((f s, map f clss), map map_type tys) |
534 | map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty') |
534 | map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty') |
535 | map_type (APi (ss, ty)) = APi (map f ss, map_type ty) |
535 | map_type (APi (ss, ty)) = APi (map f ss, map_type ty) |
536 |
536 |
537 fun map_term (ATerm ((s, tys), ts)) = ATerm ((f s, map map_type tys), map map_term ts) |
537 fun map_term (ATerm ((s, tys), ts)) = ATerm ((f s, map map_type tys), map map_term ts) |
538 | map_term (AAbs (((s, ty), tm), args)) = |
538 | map_term (AAbs (((s, ty), tm), args)) = |