# HG changeset patch # User wenzelm # Date 1735325875 -3600 # Node ID ece4941f0f1786e9c0c268ca3f62e46ff797fd82 # Parent 0ca0a47235e53ec93bce681e2a149726b829db61# Parent 70d2f72098df74a3781d46fd7ba60d652ba4c4b9 merged diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Bit_Operations.thy --- a/src/HOL/Bit_Operations.thy Fri Dec 27 19:49:45 2024 +0100 +++ b/src/HOL/Bit_Operations.thy Fri Dec 27 19:57:55 2024 +0100 @@ -1237,14 +1237,6 @@ \take_bit n (flip_bit m a) = (if n \ m then take_bit n a else flip_bit m (take_bit n a))\ by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_flip_bit_iff) -lemma bit_1_0 [simp]: - \bit 1 0\ - by (simp add: bit_0) - -lemma not_bit_1_Suc [simp]: - \\ bit 1 (Suc n)\ - by (simp add: bit_Suc) - lemma push_bit_Suc_numeral [simp]: \push_bit (Suc n) (numeral k) = push_bit n (numeral (Num.Bit0 k))\ by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0) @@ -1387,7 +1379,7 @@ lemma not_one_eq [simp]: \NOT 1 = - 2\ - by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff) + by (rule bit_eqI, simp add: bit_simps) sublocale "and": semilattice_neutr \(AND)\ \- 1\ by standard (rule bit_eqI, simp add: bit_and_iff) @@ -2695,6 +2687,18 @@ context semiring_bits begin +lemma bit_1_0 [simp]: + \bit 1 0\ + by (simp add: bit_0) + +lemma not_bit_1_Suc [simp]: + \\ bit 1 (Suc n)\ + by (simp add: bit_Suc) + +lemma not_bit_1_numeral [simp]: + \\ bit 1 (numeral m)\ + by (simp add: numeral_eq_Suc) + lemma not_bit_numeral_Bit0_0 [simp]: \\ bit (numeral (Num.Bit0 m)) 0\ by (simp add: bit_0) @@ -2770,7 +2774,6 @@ by (cases n; simp add: bit_0)+ lemma bit_numeral_simps [simp]: - \\ bit 1 (numeral n)\ \bit (numeral (Num.Bit0 w)) (numeral n) \ bit (numeral w) (pred_numeral n)\ \bit (numeral (Num.Bit1 w)) (numeral n) \ bit (numeral w) (pred_numeral n)\ by (simp_all add: bit_1_iff numeral_eq_Suc) @@ -2923,7 +2926,8 @@ \numeral (Num.Bit1 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\ \numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m AND NOT (numeral n))\ \numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\ - by (simp_all add: bit_eq_iff) (auto simp: bit_0 bit_simps bit_Suc bit_numeral_rec BitM_inc_eq sub_inc_One_eq split: nat.split) + by (simp_all add: bit_eq_iff) + (auto simp: bit_0 bit_simps bit_Suc bit_numeral_rec BitM_inc_eq sub_inc_One_eq split: nat.split) fun and_not_num :: \num \ num \ num option\ \<^marker>\contributor \Andreas Lochbihler\\ where diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Fri Dec 27 19:49:45 2024 +0100 +++ b/src/HOL/Code_Numeral.thy Fri Dec 27 19:57:55 2024 +0100 @@ -872,6 +872,26 @@ and (Haskell) "Prelude.abs" and (Scala) "_.abs" and (Eval) "abs" +| constant "Bit_Operations.and :: integer \ integer \ integer" \ + (SML) "IntInf.andb ((_),/ (_))" + and (OCaml) "Z.logand" + and (Haskell) infixl 7 ".&." + and (Scala) infixl 3 "&" +| constant "Bit_Operations.or :: integer \ integer \ integer" \ + (SML) "IntInf.orb ((_),/ (_))" + and (OCaml) "Z.logor" + and (Haskell) infixl 5 ".|." + and (Scala) infixl 1 "|" +| constant "Bit_Operations.xor :: integer \ integer \ integer" \ + (SML) "IntInf.xorb ((_),/ (_))" + and (OCaml) "Z.logxor" + and (Haskell) infixl 6 ".^." + and (Scala) infixl 2 "^" +| constant "Bit_Operations.not :: integer \ integer" \ + (SML) "IntInf.notb" + and (OCaml) "Z.lognot" + and (Haskell) "Data.Bits.complement" + and (Scala) "_.unary'_~" code_identifier code_module Code_Numeral \ (SML) Arith and (OCaml) Arith and (Haskell) Arith diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Codegenerator_Test/Code_Test_GHC.thy --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Fri Dec 27 19:49:45 2024 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Fri Dec 27 19:57:55 2024 +0100 @@ -1,10 +1,15 @@ (* Title: HOL/Codegenerator_Test/Code_Test_GHC.thy Author: Andreas Lochbihler, ETH Zurich - -Test case for test_code on GHC + Author: Florian Haftmann, TU Muenchen *) -theory Code_Test_GHC imports "HOL-Library.Code_Test" Code_Lazy_Test begin +theory Code_Test_GHC +imports + "HOL-Library.Code_Test" + Code_Lazy_Test +begin + +text \Test cases for \<^text>\test_code\\ test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC @@ -22,4 +27,163 @@ test_code "stake 10 (cycle ''ab'') = ''ababababab''" in GHC +text \Test cases for bit operations on target language numerals\ + +unbundle bit_operations_syntax + +lemma \bit (473514 :: integer) 5\ + by normalization + +test_code \bit (473514 :: integer) 5\ in GHC + +lemma \bit (- 805167 :: integer) 7\ + by normalization + +test_code \bit (- 805167 :: integer) 7\ in GHC + +lemma \473514 AND (767063 :: integer) = 208898\ + by normalization + +test_code \473514 AND (767063 :: integer) = 208898\ in GHC + +lemma \- 805167 AND (767063 :: integer) = 242769\ + by normalization + +test_code \- 805167 AND (767063 :: integer) = 242769\ in GHC + +lemma \473514 AND (- 314527 :: integer) = 209184\ + by normalization + +test_code \473514 AND (- 314527 :: integer) = 209184\ in GHC + +lemma \- 805167 AND (- 314527 :: integer) = - 839103\ + by normalization + +test_code \- 805167 AND (- 314527 :: integer) = - 839103\ in GHC + +lemma \473514 OR (767063 :: integer) = 1031679\ + by normalization + +test_code \473514 OR (767063 :: integer) = 1031679\ in GHC + +lemma \- 805167 OR (767063 :: integer) = - 280873\ + by normalization + +test_code \- 805167 OR (767063 :: integer) = - 280873\ in GHC + +lemma \473514 OR (- 314527 :: integer) = - 50197\ + by normalization + +test_code \473514 OR (- 314527 :: integer) = - 50197\ in GHC + +lemma \- 805167 OR (- 314527 :: integer) = - 280591\ + by normalization + +test_code \- 805167 OR (- 314527 :: integer) = - 280591\ in GHC + +lemma \473514 XOR (767063 :: integer) = 822781\ + by normalization + +test_code \473514 XOR (767063 :: integer) = 822781\ in GHC + +lemma \- 805167 XOR (767063 :: integer) = - 523642\ + by normalization + +test_code \- 805167 XOR (767063 :: integer) = - 523642\ in GHC + +lemma \473514 XOR (- 314527 :: integer) = - 259381\ + by normalization + +test_code \473514 XOR (- 314527 :: integer) = - 259381\ in GHC + +lemma \- 805167 XOR (- 314527 :: integer) = 558512\ + by normalization + +test_code \- 805167 XOR (- 314527 :: integer) = 558512\ in GHC + +lemma \NOT (473513 :: integer) = - 473514\ + by normalization + +test_code \NOT (473513 :: integer) = - 473514\ in GHC + +lemma \NOT (- 805167 :: integer) = 805166\ + by normalization + +test_code \NOT (- 805167 :: integer) = 805166\ in GHC + +lemma \(mask 39 :: integer) = 549755813887\ + by normalization + +test_code \(mask 39 :: integer) = 549755813887\ in GHC + +lemma \set_bit 15 (473514 :: integer) = 506282\ + by normalization + +test_code \set_bit 15 (473514 :: integer) = 506282\ in GHC + +lemma \set_bit 11 (- 805167 :: integer) = - 803119\ + by normalization + +test_code \set_bit 11 (- 805167 :: integer) = - 803119\ in GHC + +lemma \unset_bit 13 (473514 :: integer) = 465322\ + by normalization + +test_code \unset_bit 13 (473514 :: integer) = 465322\ in GHC + +lemma \unset_bit 12 (- 805167 :: integer) = - 809263\ + by normalization + +test_code \unset_bit 12 (- 805167 :: integer) = - 809263\ in GHC + +lemma \flip_bit 15 (473514 :: integer) = 506282\ + by normalization + +test_code \flip_bit 15 (473514 :: integer) = 506282\ in GHC + +lemma \flip_bit 12 (- 805167 :: integer) = - 809263\ + by normalization + +test_code \flip_bit 12 (- 805167 :: integer) = - 809263\ in GHC + +lemma \push_bit 12 (473514 :: integer) = 1939513344\ + by normalization + +test_code \push_bit 12 (473514 :: integer) = 1939513344\ in GHC + +lemma \push_bit 12 (- 805167 :: integer) = - 3297964032\ + by normalization + +test_code \push_bit 12 (- 805167 :: integer) = - 3297964032\ in GHC + +lemma \drop_bit 12 (473514 :: integer) = 115\ + by normalization + +test_code \drop_bit 12 (473514 :: integer) = 115\ in GHC + +lemma \drop_bit 12 (- 805167 :: integer) = - 197\ + by normalization + +test_code \drop_bit 12 (- 805167 :: integer) = - 197\ in GHC + +lemma \take_bit 12 (473514 :: integer) = 2474\ + by normalization + +test_code \take_bit 12 (473514 :: integer) = 2474\ in GHC + +lemma \take_bit 12 (- 805167 :: integer) = 1745\ + by normalization + +test_code \take_bit 12 (- 805167 :: integer) = 1745\ in GHC + +lemma \signed_take_bit 12 (473514 :: integer) = - 1622\ + by normalization + +test_code \signed_take_bit 12 (473514 :: integer) = - 1622\ in GHC + +lemma \signed_take_bit 12 (- 805167 :: integer) = - 2351\ + by normalization + +test_code \signed_take_bit 12 (- 805167 :: integer) = - 2351\ in GHC + end diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Fri Dec 27 19:49:45 2024 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Fri Dec 27 19:57:55 2024 +0100 @@ -1,10 +1,15 @@ (* Title: HOL/Codegenerator_Test/Code_Test_OCaml.thy Author: Andreas Lochbihler, ETH Zurich - -Test case for test_code on OCaml + Author: Florian Haftmann, TU Muenchen *) -theory Code_Test_OCaml imports "HOL-Library.Code_Test" Code_Lazy_Test begin +theory Code_Test_OCaml +imports + "HOL-Library.Code_Test" + Code_Lazy_Test +begin + +text \Test cases for \<^text>\test_code\\ test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml @@ -22,4 +27,163 @@ test_code "stake 10 (cycle ''ab'') = ''ababababab''" in OCaml +text \Test cases for bit operations on target language numerals\ + +unbundle bit_operations_syntax + +lemma \bit (473514 :: integer) 5\ + by normalization + +test_code \bit (473514 :: integer) 5\ in OCaml + +lemma \bit (- 805167 :: integer) 7\ + by normalization + +test_code \bit (- 805167 :: integer) 7\ in OCaml + +lemma \473514 AND (767063 :: integer) = 208898\ + by normalization + +test_code \473514 AND (767063 :: integer) = 208898\ in OCaml + +lemma \- 805167 AND (767063 :: integer) = 242769\ + by normalization + +test_code \- 805167 AND (767063 :: integer) = 242769\ in OCaml + +lemma \473514 AND (- 314527 :: integer) = 209184\ + by normalization + +test_code \473514 AND (- 314527 :: integer) = 209184\ in OCaml + +lemma \- 805167 AND (- 314527 :: integer) = - 839103\ + by normalization + +test_code \- 805167 AND (- 314527 :: integer) = - 839103\ in OCaml + +lemma \473514 OR (767063 :: integer) = 1031679\ + by normalization + +test_code \473514 OR (767063 :: integer) = 1031679\ in OCaml + +lemma \- 805167 OR (767063 :: integer) = - 280873\ + by normalization + +test_code \- 805167 OR (767063 :: integer) = - 280873\ in OCaml + +lemma \473514 OR (- 314527 :: integer) = - 50197\ + by normalization + +test_code \473514 OR (- 314527 :: integer) = - 50197\ in OCaml + +lemma \- 805167 OR (- 314527 :: integer) = - 280591\ + by normalization + +test_code \- 805167 OR (- 314527 :: integer) = - 280591\ in OCaml + +lemma \473514 XOR (767063 :: integer) = 822781\ + by normalization + +test_code \473514 XOR (767063 :: integer) = 822781\ in OCaml + +lemma \- 805167 XOR (767063 :: integer) = - 523642\ + by normalization + +test_code \- 805167 XOR (767063 :: integer) = - 523642\ in OCaml + +lemma \473514 XOR (- 314527 :: integer) = - 259381\ + by normalization + +test_code \473514 XOR (- 314527 :: integer) = - 259381\ in OCaml + +lemma \- 805167 XOR (- 314527 :: integer) = 558512\ + by normalization + +test_code \- 805167 XOR (- 314527 :: integer) = 558512\ in OCaml + +lemma \NOT (473513 :: integer) = - 473514\ + by normalization + +test_code \NOT (473513 :: integer) = - 473514\ in OCaml + +lemma \NOT (- 805167 :: integer) = 805166\ + by normalization + +test_code \NOT (- 805167 :: integer) = 805166\ in OCaml + +lemma \(mask 39 :: integer) = 549755813887\ + by normalization + +test_code \(mask 39 :: integer) = 549755813887\ in OCaml + +lemma \set_bit 15 (473514 :: integer) = 506282\ + by normalization + +test_code \set_bit 15 (473514 :: integer) = 506282\ in OCaml + +lemma \set_bit 11 (- 805167 :: integer) = - 803119\ + by normalization + +test_code \set_bit 11 (- 805167 :: integer) = - 803119\ in OCaml + +lemma \unset_bit 13 (473514 :: integer) = 465322\ + by normalization + +test_code \unset_bit 13 (473514 :: integer) = 465322\ in OCaml + +lemma \unset_bit 12 (- 805167 :: integer) = - 809263\ + by normalization + +test_code \unset_bit 12 (- 805167 :: integer) = - 809263\ in OCaml + +lemma \flip_bit 15 (473514 :: integer) = 506282\ + by normalization + +test_code \flip_bit 15 (473514 :: integer) = 506282\ in OCaml + +lemma \flip_bit 12 (- 805167 :: integer) = - 809263\ + by normalization + +test_code \flip_bit 12 (- 805167 :: integer) = - 809263\ in OCaml + +lemma \push_bit 12 (473514 :: integer) = 1939513344\ + by normalization + +test_code \push_bit 12 (473514 :: integer) = 1939513344\ in OCaml + +lemma \push_bit 12 (- 805167 :: integer) = - 3297964032\ + by normalization + +test_code \push_bit 12 (- 805167 :: integer) = - 3297964032\ in OCaml + +lemma \drop_bit 12 (473514 :: integer) = 115\ + by normalization + +test_code \drop_bit 12 (473514 :: integer) = 115\ in OCaml + +lemma \drop_bit 12 (- 805167 :: integer) = - 197\ + by normalization + +test_code \drop_bit 12 (- 805167 :: integer) = - 197\ in OCaml + +lemma \take_bit 12 (473514 :: integer) = 2474\ + by normalization + +test_code \take_bit 12 (473514 :: integer) = 2474\ in OCaml + +lemma \take_bit 12 (- 805167 :: integer) = 1745\ + by normalization + +test_code \take_bit 12 (- 805167 :: integer) = 1745\ in OCaml + +lemma \signed_take_bit 12 (473514 :: integer) = - 1622\ + by normalization + +test_code \signed_take_bit 12 (473514 :: integer) = - 1622\ in OCaml + +lemma \signed_take_bit 12 (- 805167 :: integer) = - 2351\ + by normalization + +test_code \signed_take_bit 12 (- 805167 :: integer) = - 2351\ in OCaml + end diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Codegenerator_Test/Code_Test_PolyML.thy --- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Fri Dec 27 19:49:45 2024 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Fri Dec 27 19:57:55 2024 +0100 @@ -1,10 +1,15 @@ (* Title: HOL/Codegenerator_Test/Code_Test_PolyML.thy Author: Andreas Lochbihler, ETH Zurich - -Test case for test_code on PolyML + Author: Florian Haftmann, TU Muenchen *) -theory Code_Test_PolyML imports "HOL-Library.Code_Test" Code_Lazy_Test begin +theory Code_Test_PolyML +imports + "HOL-Library.Code_Test" + Code_Lazy_Test +begin + +text \Test cases for \<^text>\test_code\\ test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML @@ -12,4 +17,163 @@ test_code "stake 10 (cycle ''ab'') = ''ababababab''" in PolyML +text \Test cases for bit operations on target language numerals\ + +unbundle bit_operations_syntax + +lemma \bit (473514 :: integer) 5\ + by normalization + +test_code \bit (473514 :: integer) 5\ in PolyML + +lemma \bit (- 805167 :: integer) 7\ + by normalization + +test_code \bit (- 805167 :: integer) 7\ in PolyML + +lemma \473514 AND (767063 :: integer) = 208898\ + by normalization + +test_code \473514 AND (767063 :: integer) = 208898\ in PolyML + +lemma \- 805167 AND (767063 :: integer) = 242769\ + by normalization + +test_code \- 805167 AND (767063 :: integer) = 242769\ in PolyML + +lemma \473514 AND (- 314527 :: integer) = 209184\ + by normalization + +test_code \473514 AND (- 314527 :: integer) = 209184\ in PolyML + +lemma \- 805167 AND (- 314527 :: integer) = - 839103\ + by normalization + +test_code \- 805167 AND (- 314527 :: integer) = - 839103\ in PolyML + +lemma \473514 OR (767063 :: integer) = 1031679\ + by normalization + +test_code \473514 OR (767063 :: integer) = 1031679\ in PolyML + +lemma \- 805167 OR (767063 :: integer) = - 280873\ + by normalization + +test_code \- 805167 OR (767063 :: integer) = - 280873\ in PolyML + +lemma \473514 OR (- 314527 :: integer) = - 50197\ + by normalization + +test_code \473514 OR (- 314527 :: integer) = - 50197\ in PolyML + +lemma \- 805167 OR (- 314527 :: integer) = - 280591\ + by normalization + +test_code \- 805167 OR (- 314527 :: integer) = - 280591\ in PolyML + +lemma \473514 XOR (767063 :: integer) = 822781\ + by normalization + +test_code \473514 XOR (767063 :: integer) = 822781\ in PolyML + +lemma \- 805167 XOR (767063 :: integer) = - 523642\ + by normalization + +test_code \- 805167 XOR (767063 :: integer) = - 523642\ in PolyML + +lemma \473514 XOR (- 314527 :: integer) = - 259381\ + by normalization + +test_code \473514 XOR (- 314527 :: integer) = - 259381\ in PolyML + +lemma \- 805167 XOR (- 314527 :: integer) = 558512\ + by normalization + +test_code \- 805167 XOR (- 314527 :: integer) = 558512\ in PolyML + +lemma \NOT (473513 :: integer) = - 473514\ + by normalization + +test_code \NOT (473513 :: integer) = - 473514\ in PolyML + +lemma \NOT (- 805167 :: integer) = 805166\ + by normalization + +test_code \NOT (- 805167 :: integer) = 805166\ in PolyML + +lemma \(mask 39 :: integer) = 549755813887\ + by normalization + +test_code \(mask 39 :: integer) = 549755813887\ in PolyML + +lemma \set_bit 15 (473514 :: integer) = 506282\ + by normalization + +test_code \set_bit 15 (473514 :: integer) = 506282\ in PolyML + +lemma \set_bit 11 (- 805167 :: integer) = - 803119\ + by normalization + +test_code \set_bit 11 (- 805167 :: integer) = - 803119\ in PolyML + +lemma \unset_bit 13 (473514 :: integer) = 465322\ + by normalization + +test_code \unset_bit 13 (473514 :: integer) = 465322\ in PolyML + +lemma \unset_bit 12 (- 805167 :: integer) = - 809263\ + by normalization + +test_code \unset_bit 12 (- 805167 :: integer) = - 809263\ in PolyML + +lemma \flip_bit 15 (473514 :: integer) = 506282\ + by normalization + +test_code \flip_bit 15 (473514 :: integer) = 506282\ in PolyML + +lemma \flip_bit 12 (- 805167 :: integer) = - 809263\ + by normalization + +test_code \flip_bit 12 (- 805167 :: integer) = - 809263\ in PolyML + +lemma \push_bit 12 (473514 :: integer) = 1939513344\ + by normalization + +test_code \push_bit 12 (473514 :: integer) = 1939513344\ in PolyML + +lemma \push_bit 12 (- 805167 :: integer) = - 3297964032\ + by normalization + +test_code \push_bit 12 (- 805167 :: integer) = - 3297964032\ in PolyML + +lemma \drop_bit 12 (473514 :: integer) = 115\ + by normalization + +test_code \drop_bit 12 (473514 :: integer) = 115\ in PolyML + +lemma \drop_bit 12 (- 805167 :: integer) = - 197\ + by normalization + +test_code \drop_bit 12 (- 805167 :: integer) = - 197\ in PolyML + +lemma \take_bit 12 (473514 :: integer) = 2474\ + by normalization + +test_code \take_bit 12 (473514 :: integer) = 2474\ in PolyML + +lemma \take_bit 12 (- 805167 :: integer) = 1745\ + by normalization + +test_code \take_bit 12 (- 805167 :: integer) = 1745\ in PolyML + +lemma \signed_take_bit 12 (473514 :: integer) = - 1622\ + by normalization + +test_code \signed_take_bit 12 (473514 :: integer) = - 1622\ in PolyML + +lemma \signed_take_bit 12 (- 805167 :: integer) = - 2351\ + by normalization + +test_code \signed_take_bit 12 (- 805167 :: integer) = - 2351\ in PolyML + end diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Codegenerator_Test/Code_Test_Scala.thy --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Fri Dec 27 19:49:45 2024 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Fri Dec 27 19:57:55 2024 +0100 @@ -1,10 +1,14 @@ (* Title: HOL/Codegenerator_Test/Code_Test_Scala.thy Author: Andreas Lochbihler, ETH Zurich - -Test case for test_code on Scala + Author: Florian Haftmann, TU Muenchen *) -theory Code_Test_Scala imports "HOL-Library.Code_Test" Code_Lazy_Test begin +theory Code_Test_Scala imports + "HOL-Library.Code_Test" + Code_Lazy_Test +begin + +text \Test cases for \<^text>\test_code\\ test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala @@ -22,4 +26,163 @@ test_code "stake 10 (cycle ''ab'') = ''ababababab''" in Scala +text \Test cases for bit operations on target language numerals\ + +unbundle bit_operations_syntax + +lemma \bit (473514 :: integer) 5\ + by normalization + +test_code \bit (473514 :: integer) 5\ in Scala + +lemma \bit (- 805167 :: integer) 7\ + by normalization + +test_code \bit (- 805167 :: integer) 7\ in Scala + +lemma \473514 AND (767063 :: integer) = 208898\ + by normalization + +test_code \473514 AND (767063 :: integer) = 208898\ in Scala + +lemma \- 805167 AND (767063 :: integer) = 242769\ + by normalization + +test_code \- 805167 AND (767063 :: integer) = 242769\ in Scala + +lemma \473514 AND (- 314527 :: integer) = 209184\ + by normalization + +test_code \473514 AND (- 314527 :: integer) = 209184\ in Scala + +lemma \- 805167 AND (- 314527 :: integer) = - 839103\ + by normalization + +test_code \- 805167 AND (- 314527 :: integer) = - 839103\ in Scala + +lemma \473514 OR (767063 :: integer) = 1031679\ + by normalization + +test_code \473514 OR (767063 :: integer) = 1031679\ in Scala + +lemma \- 805167 OR (767063 :: integer) = - 280873\ + by normalization + +test_code \- 805167 OR (767063 :: integer) = - 280873\ in Scala + +lemma \473514 OR (- 314527 :: integer) = - 50197\ + by normalization + +test_code \473514 OR (- 314527 :: integer) = - 50197\ in Scala + +lemma \- 805167 OR (- 314527 :: integer) = - 280591\ + by normalization + +test_code \- 805167 OR (- 314527 :: integer) = - 280591\ in Scala + +lemma \473514 XOR (767063 :: integer) = 822781\ + by normalization + +test_code \473514 XOR (767063 :: integer) = 822781\ in Scala + +lemma \- 805167 XOR (767063 :: integer) = - 523642\ + by normalization + +test_code \- 805167 XOR (767063 :: integer) = - 523642\ in Scala + +lemma \473514 XOR (- 314527 :: integer) = - 259381\ + by normalization + +test_code \473514 XOR (- 314527 :: integer) = - 259381\ in Scala + +lemma \- 805167 XOR (- 314527 :: integer) = 558512\ + by normalization + +test_code \- 805167 XOR (- 314527 :: integer) = 558512\ in Scala + +lemma \NOT (473513 :: integer) = - 473514\ + by normalization + +test_code \NOT (473513 :: integer) = - 473514\ in Scala + +lemma \NOT (- 805167 :: integer) = 805166\ + by normalization + +test_code \NOT (- 805167 :: integer) = 805166\ in Scala + +lemma \(mask 39 :: integer) = 549755813887\ + by normalization + +test_code \(mask 39 :: integer) = 549755813887\ in Scala + +lemma \set_bit 15 (473514 :: integer) = 506282\ + by normalization + +test_code \set_bit 15 (473514 :: integer) = 506282\ in Scala + +lemma \set_bit 11 (- 805167 :: integer) = - 803119\ + by normalization + +test_code \set_bit 11 (- 805167 :: integer) = - 803119\ in Scala + +lemma \unset_bit 13 (473514 :: integer) = 465322\ + by normalization + +test_code \unset_bit 13 (473514 :: integer) = 465322\ in Scala + +lemma \unset_bit 12 (- 805167 :: integer) = - 809263\ + by normalization + +test_code \unset_bit 12 (- 805167 :: integer) = - 809263\ in Scala + +lemma \flip_bit 15 (473514 :: integer) = 506282\ + by normalization + +test_code \flip_bit 15 (473514 :: integer) = 506282\ in Scala + +lemma \flip_bit 12 (- 805167 :: integer) = - 809263\ + by normalization + +test_code \flip_bit 12 (- 805167 :: integer) = - 809263\ in Scala + +lemma \push_bit 12 (473514 :: integer) = 1939513344\ + by normalization + +test_code \push_bit 12 (473514 :: integer) = 1939513344\ in Scala + +lemma \push_bit 12 (- 805167 :: integer) = - 3297964032\ + by normalization + +test_code \push_bit 12 (- 805167 :: integer) = - 3297964032\ in Scala + +lemma \drop_bit 12 (473514 :: integer) = 115\ + by normalization + +test_code \drop_bit 12 (473514 :: integer) = 115\ in Scala + +lemma \drop_bit 12 (- 805167 :: integer) = - 197\ + by normalization + +test_code \drop_bit 12 (- 805167 :: integer) = - 197\ in Scala + +lemma \take_bit 12 (473514 :: integer) = 2474\ + by normalization + +test_code \take_bit 12 (473514 :: integer) = 2474\ in Scala + +lemma \take_bit 12 (- 805167 :: integer) = 1745\ + by normalization + +test_code \take_bit 12 (- 805167 :: integer) = 1745\ in Scala + +lemma \signed_take_bit 12 (473514 :: integer) = - 1622\ + by normalization + +test_code \signed_take_bit 12 (473514 :: integer) = - 1622\ in Scala + +lemma \signed_take_bit 12 (- 805167 :: integer) = - 2351\ + by normalization + +test_code \signed_take_bit 12 (- 805167 :: integer) = - 2351\ in Scala + end diff -r 70d2f72098df -r ece4941f0f17 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Fri Dec 27 19:49:45 2024 +0100 +++ b/src/Tools/Code/code_haskell.ML Fri Dec 27 19:57:55 2024 +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