diff -r 287e569eebb2 -r 565f9af86d67 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Dec 18 16:50:14 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Dec 18 16:50:14 2013 +0100 @@ -220,15 +220,18 @@ val skip_term = let fun skip _ accum [] = (accum, []) - | skip 0 accum (ss as "," :: _) = (accum, ss) - | skip 0 accum (ss as ")" :: _) = (accum, ss) - | skip 0 accum (ss as "]" :: _) = (accum, ss) - | skip n accum ((s as "(") :: ss) = skip (n + 1) (s :: accum) ss - | skip n accum ((s as "[") :: ss) = skip (n + 1) (s :: accum) ss - | skip n accum ((s as "]") :: ss) = skip (n - 1) (s :: accum) ss - | skip n accum ((s as ")") :: ss) = skip (n - 1) (s :: accum) ss - | skip n accum (s :: ss) = skip n (s :: accum) ss - in skip 0 [] #>> (rev #> implode) end + | skip n accum (s :: ss) = + if s = "," andalso n = 0 then + (accum, ss) + else if member (op =) [")", "]", ">", "}"] s then + if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss + else if member (op =) ["(", "[", "<", "{"] s then + skip (n + 1) (s :: accum) ss + else + skip n (s :: accum) ss + in + skip 0 [] #>> (rev #> implode) + end datatype source = File_Source of string * string option | @@ -261,21 +264,17 @@ || scan_general_id >> (fn s => Inference_Source ("", [s])) (* for E *) || skip_term >> K dummy_inference) x -fun list_app (f, args) = - fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f +fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f (* We currently ignore TFF and THF types. *) -fun parse_type_stuff x = - Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x +fun parse_type_stuff x = Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x and parse_arg x = ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff || scan_general_id --| parse_type_stuff -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> (ATerm o apfst (rpair []))) x -and parse_term x = - (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x -and parse_terms x = - (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x +and parse_term x = (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x +and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x fun parse_atom x = (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal @@ -311,9 +310,7 @@ and parse_quantified_formula x = (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal - >> (fn ((q, ts), phi) => - (* We ignore TFF and THF types for now. *) - AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x + >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x val parse_tstp_extra_arguments = Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) @@ -351,9 +348,9 @@ c1 = c2 andalso length phis1 = length phis2 andalso forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2) | is_same_formula comm subst - (AAtom (tm1 as ATerm (("equal", []), [tm11, tm12]))) (AAtom tm2) = + (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) = is_same_term subst tm1 tm2 orelse - (comm andalso is_same_term subst (ATerm (("equal", []), [tm12, tm11])) tm2) + (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2) | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 | is_same_formula _ _ _ _ = false @@ -361,11 +358,13 @@ if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE | matching_formula_line_identifier _ _ = NONE -fun find_formula_in_problem problem phi = - problem |> maps snd |> map_filter (matching_formula_line_identifier phi) - |> try (single o hd) |> the_default [] +fun find_formula_in_problem phi = + maps snd + #> map_filter (matching_formula_line_identifier phi) + #> try (single o hd) + #> the_default [] -fun commute_eq (AAtom (ATerm ((s, []), tms))) = AAtom (ATerm ((s, []), rev tms)) +fun commute_eq (AAtom (ATerm ((s, tys), tms))) = AAtom (ATerm ((s, tys), rev tms)) | commute_eq _ = raise Fail "expected equation" fun role_of_tptp_string "axiom" = Axiom @@ -392,7 +391,7 @@ (case deps of File_Source (_, SOME s) => (if s = waldmeister_conjecture_name then - (case find_formula_in_problem problem (mk_anot phi) of + (case find_formula_in_problem (mk_anot phi) problem of (* Waldmeister hack: Get the original orientation of the equation to avoid confusing Isar. *) [(s, phi')] => @@ -404,16 +403,14 @@ phi), "", []) | File_Source _ => - (((num, phi |> find_formula_in_problem problem |> map fst), - phi), "", []) + (((num, map fst (find_formula_in_problem phi problem)), phi), "", []) | Inference_Source (rule, deps) => (((num, []), phi), rule, deps)) - fun mk_step () = - (name, role_of_tptp_string role, phi, rule, map (rpair []) deps) + fun mk_step () = (name, role_of_tptp_string role, phi, rule, map (rpair []) deps) in (case role_of_tptp_string role of Definition => (case phi of - AAtom (ATerm (("equal", []), _)) => + AAtom (ATerm (("equal", _), _)) => (* Vampire's equality proxy axiom *) (name, Definition, phi, rule, map (rpair []) deps) | _ => mk_step ())