--- a/CONTRIBUTORS Tue Mar 29 13:31:45 2022 +0200
+++ b/CONTRIBUTORS Tue Mar 29 17:12:44 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 Tue Mar 29 13:31:45 2022 +0200
+++ b/NEWS Tue Mar 29 17:12:44 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 Tue Mar 29 13:31:45 2022 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 29 17:12:44 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 ^ " ")