--- a/src/HOL/Code_Numeral.thy Fri Jan 03 22:35:28 2025 +0100
+++ b/src/HOL/Code_Numeral.thy Sat Jan 04 14:25:56 2025 +0100
@@ -873,6 +873,26 @@
and (Haskell) "Prelude.abs"
and (Scala) "_.abs"
and (Eval) "abs"
+| constant "Bit_Operations.and :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
+ (SML) "IntInf.andb ((_),/ (_))"
+ and (OCaml) "Z.logand"
+ and (Haskell) infixl 7 ".&."
+ and (Scala) infixl 3 "&"
+| constant "Bit_Operations.or :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
+ (SML) "IntInf.orb ((_),/ (_))"
+ and (OCaml) "Z.logor"
+ and (Haskell) infixl 5 ".|."
+ and (Scala) infixl 1 "|"
+| constant "Bit_Operations.xor :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
+ (SML) "IntInf.xorb ((_),/ (_))"
+ and (OCaml) "Z.logxor"
+ and (Haskell) infixl 6 ".^."
+ and (Scala) infixl 2 "^"
+| constant "Bit_Operations.not :: integer \<Rightarrow> integer" \<rightharpoonup>
+ (SML) "IntInf.notb"
+ and (OCaml) "Z.lognot"
+ and (Haskell) "Data.Bits.complement"
+ and (Scala) "_.unary'_~"
code_identifier
code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
--- a/src/Tools/Code/code_haskell.ML Fri Jan 03 22:35:28 2025 +0100
+++ b/src/Tools/Code/code_haskell.ML Sat Jan 04 14:25:56 2025 +0100
@@ -330,6 +330,10 @@
("Maybe", ["Nothing", "Just"])
];
+val data_bits_import_operators = [
+ ".&.", ".|.", ".^."
+];
+
fun serialize_haskell module_prefix string_classes ctxt { module_name,
reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports =
let
@@ -379,7 +383,10 @@
enclose "import Prelude (" ");" (commas (map str
(map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
@ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr))
+ :: enclose "import Data.Bits (" ");" (commas
+ (map (str o Library.enclose "(" ")") data_bits_import_operators))
:: print_qualified_import "Prelude"
+ :: print_qualified_import "Data.Bits"
:: map (print_qualified_import o fst) includes;
fun print_module module_name (gr, imports) =
let