# HG changeset patch # User desharna # Date 1602166030 -7200 # Node ID 5d1a7b688f6d1b349b95159a9f525e1c0997f8a7 # Parent 48013583e8e60757ccb0c0d9d26047a73b97b627 recognize THF proofs properly diff -r 48013583e8e6 -r 5d1a7b688f6d src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Oct 08 07:30:02 2020 +0000 +++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Oct 08 16:07:10 2020 +0200 @@ -77,14 +77,14 @@ -> string * atp_failure option val is_same_atp_step : atp_step_name -> atp_step_name -> bool val scan_general_id : string list -> string * string list - val parse_formula : string list -> + val parse_fol_formula : string list -> (string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof val skip_term: string list -> string * string list - val parse_thf_formula :string list -> + val parse_hol_formula :string list -> ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula * string list val dummy_atype : string ATP_Problem.atp_type @@ -354,46 +354,47 @@ (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x (* We currently half ignore types. *) -fun parse_optional_type_signature x = +fun parse_fol_optional_type_signature x = (Scan.option ($$ tptp_has_type |-- parse_type) >> (fn some as SOME (AType ((s, []), [])) => if s = dfg_individual_type then NONE else some | res => res)) x -and parse_arg x = - ($$ "(" |-- parse_term --| $$ ")" --| parse_optional_type_signature - || scan_general_id -- parse_optional_type_signature +and parse_fol_arg x = + ($$ "(" |-- parse_fol_term --| $$ ")" --| parse_fol_optional_type_signature + || scan_general_id -- parse_fol_optional_type_signature -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") [] - -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] + -- Scan.optional ($$ "(" |-- parse_fol_terms --| $$ ")") [] >> (fn (((s, ty_opt), tyargs), args) => if is_tptp_variable s andalso null tyargs andalso null args andalso is_some ty_opt then ATerm ((s, the_list ty_opt), []) else ATerm ((s, tyargs), args))) x -and parse_term x = - (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) - --| parse_optional_type_signature >> list_app) x -and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x +and parse_fol_term x = + (parse_fol_arg -- Scan.repeat ($$ tptp_app |-- parse_fol_arg) + --| parse_fol_optional_type_signature >> list_app) x +and parse_fol_terms x = (parse_fol_term ::: Scan.repeat ($$ "," |-- parse_fol_term)) x -fun parse_atom x = - (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal -- parse_term) +fun parse_fol_atom x = + (parse_fol_term -- + Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal -- parse_fol_term) >> (fn (u1, NONE) => AAtom u1 | (u1, SOME (neg, u2)) => AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x (* TPTP formulas are fully parenthesized, so we don't need to worry about operator precedence. *) -fun parse_literal x = +fun parse_fol_literal x = ((Scan.repeat ($$ tptp_not) >> length) - -- ($$ "(" |-- parse_formula --| $$ ")" - || parse_quantified_formula - || parse_atom) + -- ($$ "(" |-- parse_fol_formula --| $$ ")" + || parse_fol_quantified_formula + || parse_fol_atom) >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x -and parse_formula x = - (parse_literal +and parse_fol_formula x = + (parse_fol_literal -- Scan.option ((Scan.this_string tptp_implies || Scan.this_string tptp_iff || Scan.this_string tptp_not_iff || Scan.this_string tptp_if || $$ tptp_or - || $$ tptp_and) -- parse_formula) + || $$ tptp_and) -- parse_fol_formula) >> (fn (phi1, NONE) => phi1 | (phi1, SOME (c, phi2)) => if c = tptp_implies then mk_aconn AImplies phi1 phi2 @@ -403,9 +404,9 @@ else if c = tptp_or then mk_aconn AOr phi1 phi2 else if c = tptp_and then mk_aconn AAnd phi1 phi2 else raise Fail ("impossible connective " ^ quote c))) x -and parse_quantified_formula x = +and parse_fol_quantified_formula x = (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) - --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal + --| $$ "[" -- parse_fol_terms --| $$ "]" --| $$ ":" -- parse_fol_literal >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, _), _) => (s, NONE)) ts, phi))) x val parse_tstp_extra_arguments = @@ -495,10 +496,10 @@ (parse_one_in_list tptp_binary_ops >> (fn c => if c = tptp_equal then "equal" else c)) x -val parse_fo_quantifier = +val parse_fol_quantifier = parse_one_in_list [tptp_forall, tptp_exists, tptp_lambda, tptp_hilbert_choice, tptp_hilbert_the] -val parse_ho_quantifier = +val parse_hol_quantifier = parse_one_in_list [tptp_ho_forall, tptp_ho_exists, tptp_hilbert_choice, tptp_hilbert_the] fun mk_ho_of_fo_quant q = @@ -508,23 +509,23 @@ else if q = tptp_hilbert_the then tptp_hilbert_the else raise Fail ("unrecognized quantification: " ^ q) -fun remove_thf_app (ATerm ((x, ty), arg)) = +fun remove_hol_app (ATerm ((x, ty), arg)) = if x = tptp_app then (case arg of - ATerm ((x, ty), arg) :: t => remove_thf_app (ATerm ((x, ty), map remove_thf_app arg @ t)) + ATerm ((x, ty), arg) :: t => remove_hol_app (ATerm ((x, ty), map remove_hol_app arg @ t)) | [AAbs ((var, tvar), phi), t] => - remove_thf_app (AAbs ((var, tvar), map remove_thf_app phi @ [t]))) + remove_hol_app (AAbs ((var, tvar), map remove_hol_app phi @ [t]))) else - ATerm ((x, ty), map remove_thf_app arg) - | remove_thf_app (AAbs (((x, ty), arg), t)) = AAbs (((x, ty), remove_thf_app arg), t) + ATerm ((x, ty), map remove_hol_app arg) + | remove_hol_app (AAbs (((x, ty), arg), t)) = AAbs (((x, ty), remove_hol_app arg), t) -fun parse_typed_var x = +fun parse_hol_typed_var x = (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type) --| Scan.option (Scan.this_string ",")) - || $$ "(" |-- parse_typed_var --| $$ ")") x + || $$ "(" |-- parse_hol_typed_var --| $$ ")") x -fun parse_simple_thf_term x = - (parse_fo_quantifier -- ($$ "[" |-- parse_typed_var --| $$ "]" --| $$ ":") -- parse_thf_term +fun parse_simple_hol_term x = + (parse_fol_quantifier -- ($$ "[" |-- parse_hol_typed_var --| $$ "]" --| $$ ":") -- parse_hol_term >> (fn ((q, ys), t) => fold_rev (fn (var, ty) => fn r => @@ -534,23 +535,23 @@ |> mk_simple_aterm) else I)) ys t) - || Scan.this_string tptp_not |-- parse_thf_term >> mk_app (mk_simple_aterm tptp_not) + || Scan.this_string tptp_not |-- parse_hol_term >> mk_app (mk_simple_aterm tptp_not) || scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type) >> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), [])) - || parse_ho_quantifier >> mk_simple_aterm - || $$ "(" |-- parse_thf_term --| $$ ")" + || parse_hol_quantifier >> mk_simple_aterm + || $$ "(" |-- parse_hol_term --| $$ ")" || parse_binary_op >> mk_simple_aterm) x -and parse_thf_term x = - (parse_simple_thf_term -- Scan.option (parse_binary_op -- parse_thf_term) +and parse_hol_term x = + (parse_simple_hol_term -- Scan.option (parse_binary_op -- parse_hol_term) >> (fn (t1, SOME (c, t2)) => if c = tptp_app then mk_app t1 t2 else mk_apps (mk_simple_aterm c) [t1, t2] | (t, NONE) => t)) x -fun parse_thf_formula x = (parse_thf_term #>> remove_thf_app #>> AAtom) x +fun parse_hol_formula x = (parse_hol_term #>> remove_hol_app #>> AAtom) x -fun parse_tstp_thf_line problem = +fun parse_tstp_hol_line problem = (Scan.this_string tptp_thf -- $$ "(") |-- scan_general_id --| $$ "," - -- Symbol.scan_ascii_id --| $$ "," -- (parse_thf_formula || skip_term >> K dummy_phi) + -- Symbol.scan_ascii_id --| $$ "," -- (parse_hol_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." >> (fn (((num, role), phi), deps) => @@ -568,13 +569,10 @@ [(name, role', phi, rule, map (rpair []) deps)] end) -(* Syntax: (cnf|fof|tff|thf)\(, , \). - The could be an identifier, but we assume integers. *) -fun parse_tstp_line problem = - ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof - || Scan.this_string tptp_tff || Scan.this_string tptp_thf) -- $$ "(") +fun parse_tstp_fol_line problem = + ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tff) -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," - -- (parse_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments + -- (parse_fol_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." >> (fn (((num, role0), phi), src) => let @@ -611,6 +609,8 @@ | _ => mk_step ())] end) +fun parse_tstp_line problem = parse_tstp_fol_line problem || parse_tstp_hol_line problem + (**** PARSING OF SPASS OUTPUT ****) (* SPASS returns clause references of the form "x.y". We ignore "y". *) @@ -621,7 +621,7 @@ (* We ignore the stars and the pluses that follow literals. *) fun parse_decorated_atom x = - (parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x + (parse_fol_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), [])) | mk_horn (neg_lits, pos_lits) = foldr1 (uncurry (mk_aconn AOr)) (map mk_anot neg_lits @ pos_lits) @@ -680,8 +680,7 @@ fun parse_line local_name problem = (* Satallax is handled separately, in "atp_satallax.ML". *) - if local_name = leo2N orelse local_name = leo3N then parse_tstp_thf_line problem - else if local_name = spassN then parse_spass_line + if local_name = spassN then parse_spass_line else if local_name = pirateN then parse_pirate_line else if local_name = z3_tptpN then parse_z3_tptp_core_line else parse_tstp_line problem diff -r 48013583e8e6 -r 5d1a7b688f6d src/HOL/Tools/ATP/atp_satallax.ML --- a/src/HOL/Tools/ATP/atp_satallax.ML Thu Oct 08 07:30:02 2020 +0000 +++ b/src/HOL/Tools/ATP/atp_satallax.ML Thu Oct 08 16:07:10 2020 +0200 @@ -56,7 +56,7 @@ fun parse_tstp_thf0_satallax_line x = (((Scan.this_string tptp_thf -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," - -- parse_thf_formula -- Scan.option parse_tstp_satallax_extra_arguments --| $$ ")" --| $$ ".") + -- parse_hol_formula -- Scan.option parse_tstp_satallax_extra_arguments --| $$ ")" --| $$ ".") || (Scan.this_string "tab_inh" |-- skip_term --| $$ ".") >> K dummy_satallax_step) x