--- 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.
--- 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 = "@-"
--- 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' =
--- 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