# HG changeset patch
# User desharna
# Date 1607016444 -3600
# Node ID 4bf5b4f8bd6f19568b197d0ab5fb8124baf11e97
# Parent  02b6ca455be481f55cf61da520b9f583b0a52656
proper eta-expansion to avoid lambdas in tptp fool

diff -r 02b6ca455be4 -r 4bf5b4f8bd6f src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Dec 03 17:40:31 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Dec 03 18:27:24 2020 +0100
@@ -1103,10 +1103,17 @@
 
 val unmangled_invert_const = invert_const o hd o unmangled_const_name
 
+fun eta_expand_iterm tm =
+  let
+    val T = domain_type (ityp_of tm)
+    val x = "CHANGEME"
+  in
+    IAbs ((`I x, T), IApp (tm, IConst (`I x, T, [])))
+  end
+
 fun introduce_proxies_in_iterm type_enc =
   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, _]), _])) _ =
+    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
            syntactic sugar "!" and "?" whenever possible. *)
@@ -1115,7 +1122,7 @@
                     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"
+      | tweak_ho_quant ho_quant T _ = IConst (`I ho_quant, T, [])
     fun tweak_ho_equal T argc =
       if argc = 2 then
         IConst (`I tptp_equal, T, [])
@@ -1130,7 +1137,20 @@
                             IConst (`I "Z", i_T, []))))
         end
     fun intro top_level args (IApp (tm1, tm2)) =
-        IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
+        let
+          val tm1' = intro top_level (tm2 :: args) tm1
+          val tm2' = intro false [] tm2
+          val tm2'' =
+            (case tm1' of
+              IConst ((s, _), _, _) =>
+              if s = tptp_ho_forall orelse s = tptp_ho_exists then
+                eta_expand_iterm tm2'
+              else
+                tm2'
+            | _ => tm2')
+        in
+          IApp (tm1', tm2'')
+        end
       | intro top_level args (IConst (name as (s, _), T, T_args)) =
         (case proxify_const s of
           SOME proxy_base =>