# HG changeset patch
# User haftmann
# Date 1736008725 -3600
# Node ID 5e3dd01a9eb27d67a8c3e09eb2b7474d32550d84
# Parent  378b9d6c52b2c17e2df942fd0ee95cc9e9d57848
separate theory for tests checking bit operations

diff -r 378b9d6c52b2 -r 5e3dd01a9eb2 src/HOL/Codegenerator_Test/Code_Test_GHC.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sat Jan 04 14:41:30 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sat Jan 04 17:38:45 2025 +0100
@@ -1,11 +1,9 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_GHC.thy
     Author:     Andreas Lochbihler, ETH Zurich
-    Author:     Florian Haftmann, TU Muenchen
 *)
 
 theory Code_Test_GHC
 imports
-  "HOL-Library.Code_Target_Bit_Shifts"
   "HOL-Library.Code_Test"
   Code_Lazy_Test
 begin
diff -r 378b9d6c52b2 -r 5e3dd01a9eb2 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Sat Jan 04 14:41:30 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Sat Jan 04 17:38:45 2025 +0100
@@ -1,11 +1,9 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_OCaml.thy
     Author:     Andreas Lochbihler, ETH Zurich
-    Author:     Florian Haftmann, TU Muenchen
 *)
 
 theory Code_Test_OCaml
 imports
-  "HOL-Library.Code_Target_Bit_Shifts"
   "HOL-Library.Code_Test"
   Code_Lazy_Test
 begin
diff -r 378b9d6c52b2 -r 5e3dd01a9eb2 src/HOL/Codegenerator_Test/Code_Test_PolyML.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Sat Jan 04 14:41:30 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Sat Jan 04 17:38:45 2025 +0100
@@ -1,11 +1,9 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_PolyML.thy
     Author:     Andreas Lochbihler, ETH Zurich
-    Author:     Florian Haftmann, TU Muenchen
 *)
 
 theory Code_Test_PolyML
 imports 
-  "HOL-Library.Code_Target_Bit_Shifts"
   "HOL-Library.Code_Test"
   Code_Lazy_Test
 begin
diff -r 378b9d6c52b2 -r 5e3dd01a9eb2 src/HOL/Codegenerator_Test/Code_Test_Scala.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Sat Jan 04 14:41:30 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Sat Jan 04 17:38:45 2025 +0100
@@ -1,11 +1,9 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_Scala.thy
     Author:     Andreas Lochbihler, ETH Zurich
-    Author:     Florian Haftmann, TU Muenchen
 *)
 
 theory Code_Test_Scala
 imports
-  "HOL-Library.Code_Target_Bit_Shifts"
   "HOL-Library.Code_Test"
   Code_Lazy_Test
 begin
diff -r 378b9d6c52b2 -r 5e3dd01a9eb2 src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Sat Jan 04 17:38:45 2025 +0100
@@ -0,0 +1,63 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Test of target-language bit operations\<close>
+
+theory Generate_Target_Bit_Operations
+imports
+  "HOL-Library.Code_Test"
+  "HOL-Library.Code_Target_Bit_Shifts"
+begin
+
+unbundle bit_operations_syntax
+
+definition computations where
+  \<open>computations = (
+    [bit (473514 :: integer) 5, bit (- 805167 :: integer) 7],
+    [473514 AND 767063, - 805167 AND 767063, 473514 AND - 314527, - 805167 AND - 314527 :: integer],
+    [473514 OR 767063, - 805167 OR 767063, 473514 OR - 314527, - 805167 OR - 314527 :: integer],
+    [473514 XOR 767063, - 805167 XOR 767063, 473514 XOR - 314527, - 805167 XOR - 314527 :: integer],
+    [NOT 473513, NOT (- 805167) :: integer],
+    mask 39 :: integer,
+    [set_bit 15 473514, set_bit 11 (- 805167) :: integer],
+    [unset_bit 13 473514, unset_bit 12 (- 805167) :: integer],
+    [flip_bit 15 473514, flip_bit 12 (- 805167) :: integer],
+    [push_bit 12 473514, push_bit 12 (- 805167) :: integer],
+    [drop_bit 12 473514, drop_bit 12 (- 805167) :: integer],
+    [take_bit 12 473514, take_bit 12 (- 805167) :: integer],
+    [signed_take_bit 12 473514, signed_take_bit 12 (- 805167) :: integer]
+  )\<close>
+
+definition results where
+  \<open>results = (
+    [True, True],
+    [208898, 242769, 209184, - 839103 :: integer],
+    [1031679, - 280873, - 50197, - 280591 :: integer],
+    [822781, - 523642, - 259381, 558512 :: integer],
+    [- 473514, 805166 :: integer],
+    549755813887 :: integer,
+    [506282, - 803119 :: integer],
+    [465322, - 809263 :: integer],
+    [506282, - 809263 :: integer],
+    [1939513344, - 3297964032 :: integer],
+    [115, - 197 :: integer],
+    [2474, 1745 :: integer],
+    [- 1622, - 2351 :: integer]
+  )\<close>
+
+definition check where
+  \<open>check \<longleftrightarrow> computations = results\<close>
+
+lemma check
+  by code_simp
+
+lemma check
+  by normalization
+
+lemma check
+  by eval
+
+test_code check in OCaml
+test_code check in GHC
+test_code check in Scala
+
+end
diff -r 378b9d6c52b2 -r 5e3dd01a9eb2 src/HOL/ROOT
--- a/src/HOL/ROOT	Sat Jan 04 14:41:30 2025 +0100
+++ b/src/HOL/ROOT	Sat Jan 04 17:38:45 2025 +0100
@@ -373,6 +373,7 @@
     Generate_Target_Nat
     Generate_Abstract_Char
     Generate_Efficient_Datastructures
+    Generate_Target_Bit_Operations
     Code_Lazy_Test
     Code_Test_PolyML
     Code_Test_Scala