# HG changeset patch # User haftmann # Date 1735998090 -3600 # Node ID 378b9d6c52b2c17e2df942fd0ee95cc9e9d57848 # Parent 97987036f051a254988c44b9ff588d88acb2a78a optionally use shift operations on target numerals for efficient execution diff -r 97987036f051 -r 378b9d6c52b2 NEWS --- a/NEWS Sat Jan 04 14:25:56 2025 +0100 +++ b/NEWS Sat Jan 04 14:41:30 2025 +0100 @@ -225,6 +225,10 @@ * Code generator: command 'code_reserved' now uses parentheses for target languages, similar to 'code_printing'. +* Theory HOL-Library.Code_Target_Bit_Shifts implemented bit shifts on numeric +types by target-language operations; this is also used by +HOL-Library.Code_Target_Numeral. + * Sledgehammer: - Update of bundled provers: . E 3.1 -- with patch on Windows/Cygwin for proper interrupts diff -r 97987036f051 -r 378b9d6c52b2 src/Doc/Codegen/Adaptation.thy --- a/src/Doc/Codegen/Adaptation.thy Sat Jan 04 14:25:56 2025 +0100 +++ b/src/Doc/Codegen/Adaptation.thy Sat Jan 04 14:41:30 2025 +0100 @@ -204,13 +204,17 @@ Pattern matching with \<^term>\0::nat\ / \<^const>\Suc\ is eliminated by a preprocessor. + \item[\Code_Target_Bit_Shifts\] implements bit shifts on \<^typ>\integer\ + by target-language operations. Combined with \Code_Target_Int\ + or \Code_Target_Nat\, bit shifts on \<^typ>\int\ or \<^type>\nat\ can + be implemented by target-language operations. + \item[\Code_Target_Numeral\] is a convenience theory - containing both \Code_Target_Nat\ and - \Code_Target_Int\. + containing \Code_Target_Nat\, \Code_Target_Int\ and \Code_Target_Bit_Shifts\- \item[\Code_Abstract_Char\] implements type \<^typ>\char\ by target language integers, sacrificing pattern patching in exchange for dramatically - increased performance for comparisions. + increased performance for comparisons. \item[\<^theory>\HOL-Library.IArray\] provides a type \<^typ>\'a iarray\ isomorphic to lists but implemented by (effectively immutable) diff -r 97987036f051 -r 378b9d6c52b2 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Sat Jan 04 14:25:56 2025 +0100 +++ b/src/HOL/Code_Numeral.thy Sat Jan 04 14:41:30 2025 +0100 @@ -377,19 +377,6 @@ begin lemma [code]: - \bit k n \ odd (drop_bit n k)\ - \NOT k = - k - 1\ - \mask n = 2 ^ n - (1 :: integer)\ - \set_bit n k = k OR push_bit n 1\ - \unset_bit n k = k AND NOT (push_bit n 1)\ - \flip_bit n k = k XOR push_bit n 1\ - \push_bit n k = k * 2 ^ n\ - \drop_bit n k = k div 2 ^ n\ - \take_bit n k = k mod 2 ^ n\ for k :: integer - by (fact bit_iff_odd_drop_bit not_eq_complement mask_eq_exp_minus_1 - set_bit_eq_or unset_bit_eq_and_not flip_bit_eq_xor push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+ - -lemma [code]: \k AND l = (if k = 0 \ l = 0 then 0 else if k = - 1 then l else if l = - 1 then k else (k mod 2) * (l mod 2) + 2 * ((k div 2) AND (l div 2)))\ for k l :: integer by transfer (fact and_int_unfold) @@ -404,6 +391,42 @@ else \k mod 2 - l mod 2\ + 2 * ((k div 2) XOR (l div 2)))\ for k l :: integer by transfer (fact xor_int_unfold) +lemma [code]: + \NOT k = - k - 1\ for k :: integer + by (fact not_eq_complement) + +lemma [code]: + \bit k n \ k AND push_bit n 1 \ (0 :: integer)\ + by (simp add: and_exp_eq_0_iff_not_bit) + +lemma [code]: + \mask n = push_bit n 1 - (1 :: integer)\ + by (simp add: mask_eq_exp_minus_1) + +lemma [code]: + \set_bit n k = k OR push_bit n 1\ for k :: integer + by (fact set_bit_def) + +lemma [code]: + \unset_bit n k = k AND NOT (push_bit n 1)\ for k :: integer + by (fact unset_bit_def) + +lemma [code]: + \flip_bit n k = k XOR push_bit n 1\ for k :: integer + by (fact flip_bit_def) + +lemma [code]: + \push_bit n k = k * 2 ^ n\ for k :: integer + by (fact push_bit_eq_mult) + +lemma [code]: + \drop_bit n k = k div 2 ^ n\ for k :: integer + by (fact drop_bit_eq_div) + +lemma [code]: + \take_bit n k = k AND mask n\ for k :: integer + by (fact take_bit_eq_mask) + end instantiation integer :: linordered_euclidean_semiring_division diff -r 97987036f051 -r 378b9d6c52b2 src/HOL/Codegenerator_Test/Code_Test_GHC.thy --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Sat Jan 04 14:25:56 2025 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Sat Jan 04 14:41:30 2025 +0100 @@ -5,6 +5,7 @@ theory Code_Test_GHC imports + "HOL-Library.Code_Target_Bit_Shifts" "HOL-Library.Code_Test" Code_Lazy_Test begin diff -r 97987036f051 -r 378b9d6c52b2 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Sat Jan 04 14:25:56 2025 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Sat Jan 04 14:41:30 2025 +0100 @@ -5,6 +5,7 @@ theory Code_Test_OCaml imports + "HOL-Library.Code_Target_Bit_Shifts" "HOL-Library.Code_Test" Code_Lazy_Test begin diff -r 97987036f051 -r 378b9d6c52b2 src/HOL/Codegenerator_Test/Code_Test_PolyML.thy --- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Sat Jan 04 14:25:56 2025 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Sat Jan 04 14:41:30 2025 +0100 @@ -5,6 +5,7 @@ theory Code_Test_PolyML imports + "HOL-Library.Code_Target_Bit_Shifts" "HOL-Library.Code_Test" Code_Lazy_Test begin diff -r 97987036f051 -r 378b9d6c52b2 src/HOL/Codegenerator_Test/Code_Test_Scala.thy --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Sat Jan 04 14:25:56 2025 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Sat Jan 04 14:41:30 2025 +0100 @@ -3,7 +3,9 @@ Author: Florian Haftmann, TU Muenchen *) -theory Code_Test_Scala imports +theory Code_Test_Scala +imports + "HOL-Library.Code_Target_Bit_Shifts" "HOL-Library.Code_Test" Code_Lazy_Test begin diff -r 97987036f051 -r 378b9d6c52b2 src/HOL/Library/Code_Target_Bit_Shifts.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy Sat Jan 04 14:41:30 2025 +0100 @@ -0,0 +1,186 @@ +(* Title: HOL/Library/Code_Target_Bit_Shifts.thy + Author: Florian Haftmann, TU Muenchen +*) + +section \Implementation of bit-shifts on target-language integers by built-in operations\ + +theory Code_Target_Bit_Shifts +imports Main +begin + +context +begin + +qualified definition push_bit :: \integer \ integer \ integer\ + where \push_bit i k = Bit_Operations.push_bit (nat_of_integer \i\) k\ + +qualified lemma push_bit_code [code]: + \push_bit i k = k * 2 ^ nat_of_integer \i\\ + by (simp add: push_bit_def push_bit_eq_mult) + +lemma push_bit_integer_code [code]: + \Bit_Operations.push_bit n k = push_bit (of_nat n) k\ + by (simp add: push_bit_def) + +qualified definition drop_bit :: \integer \ integer \ integer\ + where \drop_bit i k = Bit_Operations.drop_bit (nat_of_integer \i\) k\ + +qualified lemma drop_bit_code [code]: + \drop_bit i k = k div 2 ^ nat_of_integer \i\\ + by (simp add: drop_bit_def drop_bit_eq_div) + +lemma drop_bit_integer_code [code]: + \Bit_Operations.drop_bit n k = drop_bit (of_nat n) k\ + by (simp add: drop_bit_def) + +end + +code_printing code_module Bit_Shifts \ + (SML) \ +structure Bit_Shifts : sig + type int = IntInf.int + val push : int -> int -> int + val drop : int -> int -> int +end = struct + +type int = IntInf.int; + +fun curry f x y = f (x, y); + +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 exp = curry IntInf.pow 2; + +val div_mod = curry IntInf.divMod; + +val max_index = exp (Word.wordSize - 3) - 1; (*experimentally determined*) + +val word_of_int = Word.fromLargeInt o IntInf.toLarge; + +val word_max_index = word_of_int max_index; + +fun words_of_int k = case div_mod k max_index + of (b, s) => word_of_int s :: (replicate b word_max_index); + +fun push' i k = IntInf.<< (k, i); + +fun drop' i k = IntInf.~>> (k, i); + +(* The implementations are formally total, though indices >~ max_index will produce heavy computation load *) + +fun push i = fold push' (words_of_int (IntInf.abs i)); + +fun drop i = fold drop' (words_of_int (IntInf.abs i)); + +end;\ for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit + and (OCaml) \ +module Bit_Shifts : sig + val push : Z.t -> Z.t -> Z.t + val drop : Z.t -> Z.t -> Z.t +end = struct + +let curry f x y = f (x, y);; + +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;; +\ for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit + and (Haskell) \ +module Bit_Shifts 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' :: Int -> Int -> Int +push' i = flip shiftL (abs i) + +push :: Integer -> Integer -> Integer +push i = fold (flip shiftL) (splitIndex (abs i)) + +drop' :: Int -> Int -> Int +drop' i = flip shiftR (abs i) + +drop :: Integer -> Integer -> Integer +drop i = fold (flip shiftR) (splitIndex (abs i)) +\ for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit + and (Scala) \ +object Bit_Shifts { + +private val maxIndex : BigInt = BigInt(Int.MaxValue); + +private def replicate[A](i : BigInt, x : A) : List[A] = + if (i <= 0) Nil else 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 } + +} +\ for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit +| constant Code_Target_Bit_Shifts.push_bit \ + (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 \ + (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 97987036f051 -r 378b9d6c52b2 src/HOL/Library/Code_Target_Numeral.thy --- a/src/HOL/Library/Code_Target_Numeral.thy Sat Jan 04 14:25:56 2025 +0100 +++ b/src/HOL/Library/Code_Target_Numeral.thy Sat Jan 04 14:41:30 2025 +0100 @@ -5,7 +5,7 @@ section \Implementation of natural and integer numbers by target-language integers\ theory Code_Target_Numeral -imports Code_Target_Int Code_Target_Nat +imports Code_Target_Nat Code_Target_Int Code_Target_Bit_Shifts begin end