# HG changeset patch
# User haftmann
# Date 1743835793 -7200
# Node ID bb1f2a03b3704e8892672cb7aa77eb2bb4e3f459
# Parent  7a9164068583c03b71077581687efbde6a7d2854
incorporate target-language integer implementation of bit shifts into Main

diff -r 7a9164068583 -r bb1f2a03b370 NEWS
--- a/NEWS	Fri Apr 04 23:12:20 2025 +0200
+++ b/NEWS	Sat Apr 05 08:49:53 2025 +0200
@@ -40,6 +40,9 @@
 
 *** HOL ***
 
+* Theory "HOL-Library.Code_Target_Bit_Shifts" incorporated into HOL-Main.
+Minor INCOMPATIBILITY.
+
 * Theory "HOL.Fun":
   - Added lemmas.
       antimonotone_on_inf_fun
diff -r 7a9164068583 -r bb1f2a03b370 src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Fri Apr 04 23:12:20 2025 +0200
+++ b/src/Doc/Codegen/Adaptation.thy	Sat Apr 05 08:49:53 2025 +0200
@@ -204,11 +204,6 @@
        Pattern matching with \<^term>\<open>0::nat\<close> / \<^const>\<open>Suc\<close> is eliminated
        by a preprocessor.
 
-    \item[\<open>Code_Target_Bit_Shifts\<close>] implements bit shifts on \<^typ>\<open>integer\<close>
-       by target-language operations. Combined with \<open>Code_Target_Int\<close>
-       or \<open>Code_Target_Nat\<close>, bit shifts on \<^typ>\<open>int\<close> or \<^type>\<open>nat\<close> can
-       be implemented by target-language operations.
-
     \item[\<open>Code_Target_Numeral\<close>] is a convenience theory
        containing \<open>Code_Target_Nat\<close>, \<open>Code_Target_Int\<close> and \<open>Code_Target_Bit_Shifts\<close>-
 
diff -r 7a9164068583 -r bb1f2a03b370 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Apr 04 23:12:20 2025 +0200
+++ b/src/HOL/Code_Numeral.thy	Sat Apr 05 08:49:53 2025 +0200
@@ -848,12 +848,36 @@
 
 hide_const (open) Pos Neg sub dup divmod_abs
 
+context
+begin
+
+qualified definition push_bit :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+  where \<open>push_bit i k = Bit_Operations.push_bit (nat_of_integer \<bar>i\<bar>) k\<close>
+
+qualified lemma push_bit_code [code]:
+  \<open>push_bit i k = k * 2 ^ nat_of_integer \<bar>i\<bar>\<close>
+  by (simp add: push_bit_def push_bit_eq_mult)
+
+lemma push_bit_integer_code [code]:
+  \<open>Bit_Operations.push_bit n k = push_bit (of_nat n) k\<close>
+  by (simp add: push_bit_def)
+
+qualified definition drop_bit :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+  where \<open>drop_bit i k = Bit_Operations.drop_bit (nat_of_integer \<bar>i\<bar>) k\<close>
+
+qualified lemma drop_bit_code [code]:
+  \<open>drop_bit i k = k div 2 ^ nat_of_integer \<bar>i\<bar>\<close>
+  by (simp add: drop_bit_def drop_bit_eq_div)
+
+lemma drop_bit_integer_code [code]:
+  \<open>Bit_Operations.drop_bit n k = drop_bit (of_nat n) k\<close>
+  by (simp add: drop_bit_def)
+
+end
+
 
 subsection \<open>Serializer setup for target language integers\<close>
 
-code_reserved
-  (Eval) int Integer abs
-
 code_printing
   type_constructor integer \<rightharpoonup>
     (SML) "IntInf.int"
@@ -864,6 +888,9 @@
 | class_instance integer :: equal \<rightharpoonup>
     (Haskell) -
 
+code_reserved
+  (Eval) int Integer
+
 code_printing
   constant "0::integer" \<rightharpoonup>
     (SML) "!(0/ :/ IntInf.int)"
@@ -965,6 +992,153 @@
     and (Haskell) "Data.Bits.complement"
     and (Scala) "_.unary'_~"
 
+code_reserved
+  (Eval) abs
+
+code_printing code_module Bit_Shifts \<rightharpoonup>
+    (SML) \<open>
+structure Bit_Shifts : sig
+  type int = IntInf.int
+  val push : int -> int -> int
+  val drop : int -> int -> int
+  val word_max_index : Word.word (*only for validation*)
+end = struct
+
+open IntInf;
+
+fun fold _ [] y = y
+  | fold f (x :: xs) y = fold f xs (f x y);
+
+fun replicate n x = (if n <= 0 then [] else x :: replicate (n - 1) x);
+
+val max_index = pow (fromInt 2, Int.- (Word.wordSize, 3)) - fromInt 1; (*experimentally determined*)
+
+val word_of_int = Word.fromLargeInt o toLarge;
+
+val word_max_index = word_of_int max_index;
+
+fun words_of_int k = case divMod (k, max_index)
+  of (b, s) => word_of_int s :: (replicate b word_max_index);
+
+fun push' i k = << (k, i);
+
+fun drop' i k = ~>> (k, i);
+
+(* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
+
+fun push i = fold push' (words_of_int (abs i));
+
+fun drop i = fold drop' (words_of_int (abs i));
+
+end;\<close> for constant Code_Numeral.push_bit Code_Numeral.drop_bit
+    and (OCaml) \<open>
+module Bit_Shifts : sig
+  val push : Z.t -> Z.t -> Z.t
+  val drop : Z.t -> Z.t -> Z.t
+end = struct
+
+let rec fold f xs y = match xs with
+  [] -> y
+  | (x :: xs) -> fold f xs (f x y);;
+
+let rec replicate n x = (if Z.leq n Z.zero then [] else x :: replicate (Z.pred n) x);;
+
+let max_index = Z.of_int max_int;;
+
+let splitIndex i = let (b, s) = Z.div_rem i max_index
+  in Z.to_int s :: (replicate b max_int);;
+
+let push' i k = Z.shift_left k i;;
+
+let drop' i k = Z.shift_right k i;;
+
+(* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
+
+let push i = fold push' (splitIndex (Z.abs i));;
+
+let drop i = fold drop' (splitIndex (Z.abs i));;
+
+end;;
+\<close> for constant Code_Numeral.push_bit Code_Numeral.drop_bit
+    and (Haskell) \<open>
+module Bit_Shifts (push, drop, push', drop') where
+
+import Prelude (Int, Integer, toInteger, fromInteger, maxBound, divMod, (-), (<=), abs, flip)
+import GHC.Bits (Bits)
+import Data.Bits (shiftL, shiftR)
+
+fold :: (a -> b -> b) -> [a] -> b -> b
+fold _ [] y = y
+fold f (x : xs) y = fold f xs (f x y)
+
+replicate :: Integer -> a -> [a]
+replicate k x = if k <= 0 then [] else x : replicate (k - 1) x
+
+maxIndex :: Integer
+maxIndex = toInteger (maxBound :: Int)
+
+splitIndex :: Integer -> [Int]
+splitIndex i = fromInteger s : replicate (fromInteger b) maxBound
+  where (b, s) = i `divMod` maxIndex
+
+{- The implementations are formally total, though indices >~ maxIndex will produce heavy computation load -}
+
+push :: Integer -> Integer -> Integer
+push i = fold (flip shiftL) (splitIndex (abs i))
+
+drop :: Integer -> Integer -> Integer
+drop i = fold (flip shiftR) (splitIndex (abs i))
+
+push' :: Int -> Int -> Int
+push' i = flip shiftL (abs i)
+
+drop' :: Int -> Int -> Int
+drop' i = flip shiftR (abs i)
+\<close> for constant Code_Numeral.push_bit Code_Numeral.drop_bit
+    and (Scala) \<open>
+object Bit_Shifts {
+
+private val maxIndex : BigInt = BigInt(Int.MaxValue);
+
+private def replicate[A](i : BigInt, x : A) : List[A] =
+  i <= 0 match {
+    case true => Nil
+    case false => x :: replicate[A](i - 1, x)
+  }
+
+private def splitIndex(i : BigInt) : List[Int] = {
+  val (b, s) = i /% maxIndex
+  return s.intValue :: replicate(b, Int.MaxValue)
+}
+
+/* The implementations are formally total, though indices >~ maxIndex will produce heavy computation load */
+
+def push(i: BigInt, k: BigInt) : BigInt =
+  splitIndex(i).foldLeft(k) { (l, j) => l << j }
+
+def drop(i: BigInt, k: BigInt) : BigInt =
+  splitIndex(i).foldLeft(k) { (l, j) => l >> j }
+
+}
+\<close> for constant Code_Numeral.push_bit Code_Numeral.drop_bit
+
+code_reserved
+  (SML) Bit_Shifts
+  and (Haskell) Bit_Shifts
+  and (Scala) Bit_Shifts
+
+code_printing
+  constant Code_Numeral.push_bit \<rightharpoonup>
+    (SML) "Bit'_Shifts.push"
+    and (OCaml) "Bit'_Shifts.push"
+    and (Haskell) "Bit'_Shifts.push"
+    and (Scala) "Bit'_Shifts.push"
+| constant Code_Numeral.drop_bit \<rightharpoonup>
+    (SML) "Bit'_Shifts.drop"
+    and (OCaml) "Bit'_Shifts.drop"
+    and (Haskell) "Bit'_Shifts.drop"
+    and (Scala) "Bit'_Shifts.drop"
+
 code_identifier
   code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
diff -r 7a9164068583 -r bb1f2a03b370 src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy
--- a/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Fri Apr 04 23:12:20 2025 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Sat Apr 05 08:49:53 2025 +0200
@@ -5,7 +5,6 @@
 theory Generate_Target_Bit_Operations
 imports
   "HOL-Library.Code_Test"
-  "HOL-Library.Code_Target_Bit_Shifts"
 begin
 
 context
@@ -64,7 +63,7 @@
 
 qualified definition \<open>check_max = ()\<close>
 
-qualified definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close>
+qualified definition \<open>anchor = (Code_Numeral.drop_bit, check_max)\<close>
 
 end
 
diff -r 7a9164068583 -r bb1f2a03b370 src/HOL/Library/Code_Target_Bit_Shifts.thy
--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy	Fri Apr 04 23:12:20 2025 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,182 +0,0 @@
-(*  Title:      HOL/Library/Code_Target_Bit_Shifts.thy
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-section \<open>Implementation of bit-shifts on target-language integers by built-in operations\<close>
-
-theory Code_Target_Bit_Shifts
-imports Main
-begin
-
-context
-begin
-
-qualified definition push_bit :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
-  where \<open>push_bit i k = Bit_Operations.push_bit (nat_of_integer \<bar>i\<bar>) k\<close>
-
-qualified lemma push_bit_code [code]:
-  \<open>push_bit i k = k * 2 ^ nat_of_integer \<bar>i\<bar>\<close>
-  by (simp add: push_bit_def push_bit_eq_mult)
-
-lemma push_bit_integer_code [code]:
-  \<open>Bit_Operations.push_bit n k = push_bit (of_nat n) k\<close>
-  by (simp add: push_bit_def)
-
-qualified definition drop_bit :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
-  where \<open>drop_bit i k = Bit_Operations.drop_bit (nat_of_integer \<bar>i\<bar>) k\<close>
-
-qualified lemma drop_bit_code [code]:
-  \<open>drop_bit i k = k div 2 ^ nat_of_integer \<bar>i\<bar>\<close>
-  by (simp add: drop_bit_def drop_bit_eq_div)
-
-lemma drop_bit_integer_code [code]:
-  \<open>Bit_Operations.drop_bit n k = drop_bit (of_nat n) k\<close>
-  by (simp add: drop_bit_def)
-
-end
-
-code_printing code_module Bit_Shifts \<rightharpoonup>
-    (SML) \<open>
-structure Bit_Shifts : sig
-  type int = IntInf.int
-  val push : int -> int -> int
-  val drop : int -> int -> int
-  val word_max_index : Word.word (*only for validation*)
-end = struct
-
-open IntInf;
-
-fun fold _ [] y = y
-  | fold f (x :: xs) y = fold f xs (f x y);
-
-fun replicate n x = (if n <= 0 then [] else x :: replicate (n - 1) x);
-
-val max_index = pow (fromInt 2, Int.- (Word.wordSize, 3)) - fromInt 1; (*experimentally determined*)
-
-val word_of_int = Word.fromLargeInt o toLarge;
-
-val word_max_index = word_of_int max_index;
-
-fun words_of_int k = case divMod (k, max_index)
-  of (b, s) => word_of_int s :: (replicate b word_max_index);
-
-fun push' i k = << (k, i);
-
-fun drop' i k = ~>> (k, i);
-
-(* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
-
-fun push i = fold push' (words_of_int (abs i));
-
-fun drop i = fold drop' (words_of_int (abs i));
-
-end;\<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
-    and (OCaml) \<open>
-module Bit_Shifts : sig
-  val push : Z.t -> Z.t -> Z.t
-  val drop : Z.t -> Z.t -> Z.t
-end = struct
-
-let rec fold f xs y = match xs with
-  [] -> y
-  | (x :: xs) -> fold f xs (f x y);;
-
-let rec replicate n x = (if Z.leq n Z.zero then [] else x :: replicate (Z.pred n) x);;
-
-let max_index = Z.of_int max_int;;
-
-let splitIndex i = let (b, s) = Z.div_rem i max_index
-  in Z.to_int s :: (replicate b max_int);;
-
-let push' i k = Z.shift_left k i;;
-
-let drop' i k = Z.shift_right k i;;
-
-(* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
-
-let push i = fold push' (splitIndex (Z.abs i));;
-
-let drop i = fold drop' (splitIndex (Z.abs i));;
-
-end;;
-\<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
-    and (Haskell) \<open>
-module Bit_Shifts (push, drop, push', drop') where
-
-import Prelude (Int, Integer, toInteger, fromInteger, maxBound, divMod, (-), (<=), abs, flip)
-import GHC.Bits (Bits)
-import Data.Bits (shiftL, shiftR)
-
-fold :: (a -> b -> b) -> [a] -> b -> b
-fold _ [] y = y
-fold f (x : xs) y = fold f xs (f x y)
-
-replicate :: Integer -> a -> [a]
-replicate k x = if k <= 0 then [] else x : replicate (k - 1) x
-
-maxIndex :: Integer
-maxIndex = toInteger (maxBound :: Int)
-
-splitIndex :: Integer -> [Int]
-splitIndex i = fromInteger s : replicate (fromInteger b) maxBound
-  where (b, s) = i `divMod` maxIndex
-
-{- The implementations are formally total, though indices >~ maxIndex will produce heavy computation load -}
-
-push :: Integer -> Integer -> Integer
-push i = fold (flip shiftL) (splitIndex (abs i))
-
-drop :: Integer -> Integer -> Integer
-drop i = fold (flip shiftR) (splitIndex (abs i))
-
-push' :: Int -> Int -> Int
-push' i = flip shiftL (abs i)
-
-drop' :: Int -> Int -> Int
-drop' i = flip shiftR (abs i)
-\<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
-    and (Scala) \<open>
-object Bit_Shifts {
-
-private val maxIndex : BigInt = BigInt(Int.MaxValue);
-
-private def replicate[A](i : BigInt, x : A) : List[A] =
-  i <= 0 match {
-    case true => Nil
-    case false => x :: replicate[A](i - 1, x)
-  }
-
-private def splitIndex(i : BigInt) : List[Int] = {
-  val (b, s) = i /% maxIndex
-  return s.intValue :: replicate(b, Int.MaxValue)
-}
-
-/* The implementations are formally total, though indices >~ maxIndex will produce heavy computation load */
-
-def push(i: BigInt, k: BigInt) : BigInt =
-  splitIndex(i).foldLeft(k) { (l, j) => l << j }
-
-def drop(i: BigInt, k: BigInt) : BigInt =
-  splitIndex(i).foldLeft(k) { (l, j) => l >> j }
-
-}
-\<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
-| constant Code_Target_Bit_Shifts.push_bit \<rightharpoonup>
-    (SML) "Bit'_Shifts.push"
-    and (OCaml) "Bit'_Shifts.push"
-    and (Haskell) "Bit'_Shifts.push"
-    and (Haskell_Quickcheck) "Bit'_Shifts.push'"
-    and (Scala) "Bit'_Shifts.push"
-| constant Code_Target_Bit_Shifts.drop_bit \<rightharpoonup>
-    (SML) "Bit'_Shifts.drop"
-    and (OCaml) "Bit'_Shifts.drop"
-    and (Haskell) "Bit'_Shifts.drop"
-    and (Haskell_Quickcheck) "Bit'_Shifts.drop'"
-    and (Scala) "Bit'_Shifts.drop"
-
-code_reserved
-  (SML) Bit_Shifts
-  and (Haskell) Bit_Shifts
-  and (Scala) Bit_Shifts
-
-end
diff -r 7a9164068583 -r bb1f2a03b370 src/HOL/Library/Code_Target_Numeral.thy
--- a/src/HOL/Library/Code_Target_Numeral.thy	Fri Apr 04 23:12:20 2025 +0200
+++ b/src/HOL/Library/Code_Target_Numeral.thy	Sat Apr 05 08:49:53 2025 +0200
@@ -5,7 +5,7 @@
 section \<open>Implementation of natural and integer numbers by target-language integers\<close>
 
 theory Code_Target_Numeral
-imports Code_Target_Nat Code_Target_Int Code_Target_Bit_Shifts
+imports Code_Target_Nat Code_Target_Int
 begin
 
 end
diff -r 7a9164068583 -r bb1f2a03b370 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Fri Apr 04 23:12:20 2025 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Sat Apr 05 08:49:53 2025 +0200
@@ -40,6 +40,12 @@
   end
 \<close>
 
+code_printing
+  constant Code_Numeral.push_bit \<rightharpoonup>
+    (Haskell_Quickcheck) "Bit'_Shifts.drop'"
+| constant Code_Numeral.drop_bit \<rightharpoonup>
+    (Haskell_Quickcheck) "Bit'_Shifts.push'"
+
 
 subsubsection \<open>Narrowing's deep representation of types and terms\<close>