# HG changeset patch # User desharna # Date 1607013631 -3600 # Node ID 02b6ca455be481f55cf61da520b9f583b0a52656 # Parent 999b07bfd88653683f194b240d4b042bb4ba1b23 proper proxification for fool + refactoring diff -r 999b07bfd886 -r 02b6ca455be4 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Dec 03 11:08:54 2020 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Dec 03 17:40:31 2020 +0100 @@ -480,8 +480,8 @@ else if s = tptp_ho_forall orelse s = tptp_ho_exists then (case ts of [AAbs (((s', ty), tm), [])] => - (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever - possible, to work around LEO-II 1.2.8 parser limitation. *) + (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever possible, to work + around LEO-II, Leo-III, and Satallax parser limitation. *) tptp_string_of_formula format (AQuant (if s = tptp_ho_forall then AForall else AExists, [(s', SOME ty)], AAtom tm)) @@ -489,8 +489,8 @@ else if s = tptp_choice then (case ts of [AAbs (((s', ty), tm), args)] => - (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is - always applied to an abstraction. *) + (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an + abstraction. *) tptp_string_of_app format (tptp_choice ^ "[" ^ s' ^ " : " ^ of_type ty ^ "]: " ^ of_term tm ^ "" diff -r 999b07bfd886 -r 02b6ca455be4 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 03 11:08:54 2020 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 03 17:40:31 2020 +0100 @@ -1107,16 +1107,28 @@ let fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, []) | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) _ = - (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser - limitation. This works in conjuction with special code in - "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever - possible. *) + (* Eta-expand "!!" and "??", to work around LEO-II, Leo-III, and Satallax parser + limitations. This works in conjunction with special code in "ATP_Problem" that uses the + syntactic sugar "!" and "?" whenever possible. *) IAbs ((`I "P", p_T), IApp (IConst (`I ho_quant, T, []), IAbs ((`I "X", x_T), IApp (IConst (`I "P", p_T, []), IConst (`I "X", x_T, []))))) | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier" + fun tweak_ho_equal T argc = + if argc = 2 then + IConst (`I tptp_equal, T, []) + else + (* Eta-expand partially applied THF equality, because the LEO-II and Satallax parsers + complain about not being able to infer the type of "=". *) + let val i_T = domain_type T in + IAbs ((`I "Y", i_T), + IAbs ((`I "Z", i_T), + IApp (IApp (IConst (`I tptp_equal, T, []), + IConst (`I "Y", i_T, [])), + IConst (`I "Z", i_T, [])))) + end fun intro top_level args (IApp (tm1, tm2)) = IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2) | intro top_level args (IConst (name as (s, _), T, T_args)) = @@ -1124,46 +1136,50 @@ SOME proxy_base => let val argc = length args - val plain_const = IConst (name, T, []) + fun plain_const () = IConst (name, T, []) fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args) - val is_fool = is_type_enc_fool type_enc - fun if_card_matches card x = if not is_fool orelse card = argc then x else plain_const + fun handle_fool card x = if card = argc then x else proxy_const () in - if top_level orelse is_fool orelse is_type_enc_full_higher_order type_enc then - (case (top_level, s) of - (_, "c_False") => IConst (`I tptp_false, T, []) - | (_, "c_True") => IConst (`I tptp_true, T, []) - | (false, "c_Not") => if_card_matches 1 (IConst (`I tptp_not, T, [])) - | (false, "c_conj") => if_card_matches 2 (IConst (`I tptp_and, T, [])) - | (false, "c_disj") => if_card_matches 2 (IConst (`I tptp_or, T, [])) - | (false, "c_implies") => if_card_matches 2 (IConst (`I tptp_implies, T, [])) - | (false, "c_All") => if_card_matches 1 (tweak_ho_quant tptp_ho_forall T args) - | (false, "c_Ex") => if_card_matches 1 (tweak_ho_quant tptp_ho_exists T args) - | (false, s) => - if is_tptp_equal s then - if argc = 2 then - IConst (`I tptp_equal, T, []) - else if is_fool then - proxy_const () + (case s of + "c_False" => IConst (`I tptp_false, T, []) + | "c_True" => IConst (`I tptp_true, T, []) + | _ => + if top_level then + plain_const () + else if is_type_enc_full_higher_order type_enc then + (case s of + "c_Not" => IConst (`I tptp_not, T, []) + | "c_conj" => IConst (`I tptp_and, T, []) + | "c_disj" => IConst (`I tptp_or, T, []) + | "c_implies" => IConst (`I tptp_implies, T, []) + | "c_All" => tweak_ho_quant tptp_ho_forall T args + | "c_Ex" => tweak_ho_quant tptp_ho_exists T args + | s => + if is_tptp_equal s then + tweak_ho_equal T argc else - (* Eta-expand partially applied THF equality, because the - LEO-II and Satallax parsers complain about not being able to - infer the type of "=". *) - let val i_T = domain_type T in - IAbs ((`I "Y", i_T), - IAbs ((`I "Z", i_T), - IApp (IApp (IConst (`I tptp_equal, T, []), - IConst (`I "Y", i_T, [])), - IConst (`I "Z", i_T, [])))) - end - else - plain_const - | _ => plain_const) - else - IConst (proxy_base |>> prefix const_prefix, T, T_args) + plain_const ()) + else if is_type_enc_fool type_enc then + (case s of + "c_Not" => handle_fool 1 (IConst (`I tptp_not, T, [])) + | "c_conj" => handle_fool 2 (IConst (`I tptp_and, T, [])) + | "c_disj" => handle_fool 2 (IConst (`I tptp_or, T, [])) + | "c_implies" => handle_fool 2 (IConst (`I tptp_implies, T, [])) + | "c_All" => handle_fool 1 (tweak_ho_quant tptp_ho_forall T args) + | "c_Ex" => handle_fool 1 (tweak_ho_quant tptp_ho_exists T args) + | s => + if is_tptp_equal s then + handle_fool 2 (IConst (`I tptp_equal, T, [])) + else + plain_const ()) + else + proxy_const ()) end - | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args - else IConst (name, T, T_args)) + | NONE => + if s = tptp_choice then + tweak_ho_quant tptp_choice T args + else + IConst (name, T, T_args)) | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm) | intro _ _ tm = tm in intro true [] end