--- 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
-------------------------------
--- 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 ***
--- 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 ^ " ")
--- 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)),