refactored $ite and $let configuration and added dummy_thf_reduced prover

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Nov 17 21:36:13 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Nov 19 10:53:22 2021 +0100
@@ -685,26 +685,11 @@
           (case try (unsuffix "_arith") s of
             SOME s => (true, s)
           | NONE => (false, s))
-        val (with_let, s) =
-          (case try (unsuffix "_let") s of
-            SOME s => (true, s)
-          | NONE => (false, s))
-        val (with_ite, s) =
-          (case try (unsuffix "_ite") s of
-            SOME s => (true, s)
-          | NONE => (false, s))
-        val syntax = {with_ite = with_ite, with_let = with_let}
+        val syntax = {with_ite = true, with_let = true}
         val (fool, core) =
           (case try (unsuffix "_fool") s of
             SOME s => (With_FOOL syntax, s)
           | NONE => (Without_FOOL, s))
-
-        fun validate_syntax (type_enc as Native (_, Without_FOOL, _, _)) =
-            if with_ite orelse with_let then
-              error "\"ite\" and \"let\" options require \"native_fool\" or \"native_higher\"."
-            else
-              type_enc
-          | validate_syntax type_enc = type_enc
       in
         (case (core, poly) of
           ("native", SOME poly) =>
@@ -728,7 +713,6 @@
            | (poly as Raw_Polymorphic _, All_Types) =>
              Native (Higher_Order THF_With_Choice, With_FOOL syntax, poly, All_Types)
            | _ => raise Same.SAME))
-        |> validate_syntax
       end
 
     fun nonnative_of_string core =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Nov 17 21:36:13 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Nov 19 10:53:22 2021 +0100
@@ -300,7 +300,7 @@
        val heuristic = Config.get ctxt e_selection_heuristic
        val (format, enc, main_lam_trans) =
          if string_ord (getenv "E_VERSION", "2.7") <> LESS then
-           (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher_ite", keep_lamsN)
+           (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
          else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
            (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
          else
@@ -384,7 +384,7 @@
    prem_role = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (((150, ""), THF (Polymorphic, {with_ite = true, with_let = true}, THF_Without_Choice), "mono_native_higher_ite_let", keep_lamsN, false), ""))],
+     K [(1.0, (((150, ""), THF (Polymorphic, {with_ite = true, with_let = true}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    best_max_new_mono_instances = default_max_new_mono_instances}
 
@@ -490,9 +490,9 @@
    prem_role = Hypothesis,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (((500, meshN), TX1, "mono_native_fool_ite_let", combs_or_liftingN, false), sosN)),
-      (0.333, (((150, meshN), TX1, "poly_native_fool_ite_let", combs_or_liftingN, false), sosN)),
-      (0.334, (((50, meshN), TX1, "mono_native_fool_ite_let", combs_or_liftingN, false), no_sosN))]
+     [(0.333, (((500, meshN), TX1, "mono_native_fool", combs_or_liftingN, false), sosN)),
+      (0.333, (((150, meshN), TX1, "poly_native_fool", combs_or_liftingN, false), sosN)),
+      (0.334, (((50, meshN), TX1, "mono_native_fool", combs_or_liftingN, false), no_sosN))]
      |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single),
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
@@ -527,7 +527,7 @@
   let
     val format =
       THF (Polymorphic, {with_ite = true, with_let = false}, THF_Without_Choice)
-    val enc = ((512, "meshN"), format, "mono_native_higher_fool_ite", keep_lamsN, false)
+    val enc = ((512, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false)
   in
     {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
      arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ =>
@@ -663,18 +663,26 @@
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
+val dummy_fof =
+  let
+    val config = dummy_config Hypothesis FOF "mono_guards??" false
+  in (dummy_fofN, fn () => config) end
 
-val dummy_fof_format = FOF
-val dummy_fof_config = dummy_config Hypothesis dummy_fof_format "mono_guards??" false
-val dummy_fof = (dummy_fofN, fn () => dummy_fof_config)
+val dummy_tfx =
+  let
+    val config = dummy_config Hypothesis TX1 "poly_native_fool" false
+  in (dummy_tfxN, fn () => config) end
 
-val dummy_tfx_config = dummy_config Hypothesis TX1 "mono_native_fool_ite_let" false
-val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config)
+val dummy_thf =
+  let
+    val config = dummy_config Hypothesis TH1 "poly_native_higher" false
+  in (dummy_thfN, fn () => config) end
 
-val dummy_thf_config =
-  dummy_config Hypothesis TH1 "mono_native_higher_ite_let" false
-val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
-
+val dummy_thf_reduced =
+  let
+    val format = THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice)
+    val config = dummy_config Hypothesis format "poly_native_higher" false
+  in (dummy_thfN ^ "_reduced", fn () => config) end
 
 (* Setup *)
 
@@ -711,7 +719,7 @@
 val atps =
   [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
    remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
-   remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf]
+   remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced]
 
 val _ = Theory.setup (fold add_atp atps)