# HG changeset patch
# User desharna
# Date 1648798880 -7200
# Node ID ed0bc21cc60dc418f5cf585f8bd8384e57d43d78
# Parent  6e8ca49593346760fcb2c3fbf68099db54f410f0# Parent  bdab2daa2779679048e01282afc9b7e8b326d639
merged

diff -r 6e8ca4959334 -r ed0bc21cc60d CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Mar 31 18:12:38 2022 +0200
+++ b/CONTRIBUTORS	Fri Apr 01 09:41:20 2022 +0200
@@ -9,6 +9,9 @@
 * April - August 2021: Denis Paluca and Fabian Huch, TU München
   Various improvements to Isabelle/VSCode.
 
+* March 2021: Florian Haftmann, TU München
+  More ambitious minimazation of case expressions in generated code.
+
 
 Contributions to Isabelle2021-1
 -------------------------------
diff -r 6e8ca4959334 -r ed0bc21cc60d NEWS
--- a/NEWS	Thu Mar 31 18:12:38 2022 +0200
+++ b/NEWS	Fri Apr 01 09:41:20 2022 +0200
@@ -89,6 +89,8 @@
 * (Co)datatype package:
   - Lemma map_ident_strong is now generated for all BNFs.
 
+* More ambitious minimazation of case expressions in generated code.
+
 
 *** System ***
 
diff -r 6e8ca4959334 -r ed0bc21cc60d src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Mar 31 18:12:38 2022 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Apr 01 09:41:20 2022 +0200
@@ -253,7 +253,7 @@
 val tptp_hilbert_the = "@-"
 val tptp_not_infix = "!"
 val tptp_equal = "="
-val tptp_not_equal = "!="
+val tptp_not_equal = tptp_not_infix ^ tptp_equal
 val tptp_old_equal = "equal"
 val tptp_false = "$false"
 val tptp_true = "$true"
@@ -569,12 +569,14 @@
     |> parens
   | tptp_string_of_formula format
         (AConn (ANot, [AAtom (ATerm (("=" (* tptp_equal *), []), ts))])) =
-    space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
-                  (map (tptp_string_of_term format) ts)
+    space_implode (" " ^ tptp_not_equal ^ " ") (map (tptp_string_of_term format) ts)
+    |> is_format_higher_order format ? parens
+  | tptp_string_of_formula format
+        (AConn (ANot, [AAtom (ATerm (("equal" (* tptp_old_equal *), []), ts))])) =
+    space_implode (" " ^ tptp_not_equal ^ " ") (map (tptp_string_of_term format) ts)
     |> is_format_higher_order format ? parens
   | tptp_string_of_formula format (AConn (c, [phi])) =
-    tptp_string_of_connective c ^ " " ^
-    (tptp_string_of_formula format phi |> parens)
+    tptp_string_of_connective c ^ " " ^ (tptp_string_of_formula format phi |> parens)
     |> parens
   | tptp_string_of_formula format (AConn (c, phis)) =
     space_implode (" " ^ tptp_string_of_connective c ^ " ")
diff -r 6e8ca4959334 -r ed0bc21cc60d src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Mar 31 18:12:38 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Apr 01 09:41:20 2022 +0200
@@ -192,8 +192,8 @@
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN, "--auto-schedule")
      in
        (* FUDGE *)
-       K [((1000 (* infinity *), 1024, meshN), (format, type_enc, lam_trans, false, extra_options)),
-         ((1000 (* infinity *), 512, meshN), (format, type_enc, lam_trans, false, extra_options)),
+       K [((1000 (* infinity *), 512, meshN), (format, type_enc, lam_trans, false, extra_options)),
+         ((1000 (* infinity *), 1024, meshN), (format, type_enc, lam_trans, false, extra_options)),
          ((1000 (* infinity *), 128, mepoN), (format, type_enc, lam_trans, false, extra_options)),
          ((1000 (* infinity *), 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)),
          ((1000 (* infinity *), 256, mepoN), (format, type_enc, liftingN, false, extra_options)),