added support for TFX's and THF's $ite to Sledgehammer
authordesharna
Thu, 17 Jun 2021 12:57:22 +0200
changeset 74115 bc263f1f68cd
parent 74114 4538d6ffafbd
child 74116 dfac078e5444
added support for TFX's and THF's $ite to Sledgehammer
src/Doc/Sledgehammer/document/root.tex
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- 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