# HG changeset patch # User desharna # Date 1623927442 -7200 # Node ID bc263f1f68cd9b22ec4478cdfd667e95da55e501 # Parent 4538d6ffafbd13f51a4140720f65b31c332a6ce6 added support for TFX's and THF's $ite to Sledgehammer diff -r 4538d6ffafbd -r bc263f1f68cd src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Jun 17 11:27:21 2021 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Jun 17 12:57:22 2021 +0200 @@ -1000,7 +1000,7 @@ \item[\labelitemi] \textbf{\textit{keep\_lams}:} Keep the $\lambda$-abstractions in the generated problems. This is available -only with provers that support the TH0 syntax. +only with provers that support $\lambda$s. \item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used depends on the ATP and should be the most efficient scheme for that ATP. diff -r 4538d6ffafbd -r bc263f1f68cd src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Jun 17 11:27:21 2021 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Jun 17 12:57:22 2021 +0200 @@ -88,6 +88,7 @@ val tptp_if : string val tptp_iff : string val tptp_not_iff : string + val tptp_ite : string val tptp_app : string val tptp_not_infix : string val tptp_equal : string @@ -247,6 +248,7 @@ val tptp_if = "<=" val tptp_iff = "<=>" val tptp_not_iff = "<~>" +val tptp_ite = "$ite" val tptp_app = "@" val tptp_hilbert_choice = "@+" val tptp_hilbert_the = "@-" diff -r 4538d6ffafbd -r bc263f1f68cd src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jun 17 11:27:21 2021 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jun 17 12:57:22 2021 +0200 @@ -1147,8 +1147,9 @@ IAbs ((`I x, T), IApp (tm, IConst (`I x, T, []))) end -fun introduce_proxies_in_iterm type_enc = +fun introduce_builtins_and_proxies_in_iterm type_enc = let + val is_fool = is_type_enc_fool type_enc fun tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) [] = (* 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 @@ -1188,57 +1189,61 @@ IApp (tm1', tm2'') end | intro top_level args (IConst (name as (s, _), T, T_args)) = - (case proxify_const s of - SOME proxy_base => - let - val argc = length args - fun plain_const () = IConst (name, T, []) - fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args) - fun handle_fool card x = if card = argc then x else proxy_const () - in - if top_level then - (case s of - "c_False" => IConst (`I tptp_false, T, []) - | "c_True" => IConst (`I tptp_true, T, []) - | _ => plain_const ()) - else if is_type_enc_full_higher_order type_enc then - (case s of - "c_False" => IConst (`I tptp_false, T, []) - | "c_True" => IConst (`I tptp_true, T, []) - | "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 - plain_const ()) - else if is_type_enc_fool type_enc then - (case s of - "c_False" => IConst (`I tptp_false, T, []) - | "c_True" => IConst (`I tptp_true, T, []) - | "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)) + if is_fool andalso s = "c_If" andalso + (length args = 3 orelse is_type_enc_higher_order type_enc) then + IConst (`I tptp_ite, T, []) + else + (case proxify_const s of + SOME proxy_base => + let + val argc = length args + fun plain_const () = IConst (name, T, []) + fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args) + fun handle_fool card x = if card = argc then x else proxy_const () + in + if top_level then + (case s of + "c_False" => IConst (`I tptp_false, T, []) + | "c_True" => IConst (`I tptp_true, T, []) + | _ => plain_const ()) + else if is_type_enc_full_higher_order type_enc then + (case s of + "c_False" => IConst (`I tptp_false, T, []) + | "c_True" => IConst (`I tptp_true, T, []) + | "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 + plain_const ()) + else if is_fool then + (case s of + "c_False" => IConst (`I tptp_false, T, []) + | "c_True" => IConst (`I tptp_true, T, []) + | "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)) | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm) | intro _ _ tm = tm in intro true [] end @@ -1283,7 +1288,7 @@ val thy = Proof_Context.theory_of ctxt fun do_term bs t atomic_Ts = iterm_of_term thy type_enc bs (Envir.eta_contract t) - |>> (introduce_proxies_in_iterm type_enc + |>> (introduce_builtins_and_proxies_in_iterm type_enc #> mangle_type_args_in_iterm type_enc #> AAtom) ||> union (op =) atomic_Ts fun do_quant bs q pos s T t' = diff -r 4538d6ffafbd -r bc263f1f68cd src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Jun 17 11:27:21 2021 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Jun 17 12:57:22 2021 +0200 @@ -552,7 +552,7 @@ val zipperposition_config : atp_config = let - val format = THF (Without_FOOL, Polymorphic, THF_Without_Choice) + val format = THF (With_FOOL, Polymorphic, THF_Without_Choice) in {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]), arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ => @@ -563,9 +563,9 @@ prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) - [(0.333, (((128, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)), - (0.333, (((32, "meshN"), format, "poly_native_higher", keep_lamsN, false), zipperposition_s6)), - (0.334, (((512, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_cdots))], + [(0.333, (((128, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false), zipperposition_blsimp)), + (0.333, (((32, "meshN"), format, "poly_native_higher_fool", keep_lamsN, false), zipperposition_s6)), + (0.334, (((512, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false), zipperposition_cdots))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} end