module Data.SBV.Plugin.Examples.BitTricks where
import Data.SBV.Plugin
import Data.Bits
import Data.Word
import Prelude hiding(elem)
elem :: Eq a => a -> [a] -> Bool
elem _ [] = False
elem k (x:xs) = k == x || elem k xs
oneIf :: Num a => Bool -> a
oneIf True = 1
oneIf False = 0
fastMinCorrect :: Proved (Int -> Int -> Bool)
fastMinCorrect x y = m == fm
where m = if x < y then x else y
fm = y `xor` ((x `xor` y) .&. ((oneIf (x < y))));
fastMaxCorrect :: Proved (Int -> Int -> Bool)
fastMaxCorrect x y = m == fm
where m = if x < y then y else x
fm = x `xor` ((x `xor` y) .&. ((oneIf (x < y))));
oppositeSignsCorrect :: Proved (Int -> Int -> Bool)
oppositeSignsCorrect x y = r == os
where r = (x < 0 && y >= 0) || (x >= 0 && y < 0)
os = (x `xor` y) < 0
conditionalSetClearCorrect :: Proved (Bool -> Word32 -> Word32 -> Bool)
conditionalSetClearCorrect f m w = r == r'
where r | f = w .|. m
| True = w .&. complement m
r' = w `xor` (((oneIf f) `xor` w) .&. m)
powerOfTwoCorrect :: Proved (Word32 -> Bool)
powerOfTwoCorrect v = f == (v `elem` [2^i | i <- [(0 :: Word32) .. 31]])
where f = (v /= 0) && ((v .&. (v1)) == 0)
maskedMergeCorrect :: Proved (Word32 -> Word32 -> Word32 -> Bool)
maskedMergeCorrect a b mask = slow == fast
where slow = (a .&. complement mask) .|. (b .&. mask)
fast = a `xor` ((a `xor` b) .&. mask)
roundPowerOfTwoCorrect :: Proved (Word32 -> Bool)
roundPowerOfTwoCorrect v = f == find [2^i | i <- [(0 :: Word32) .. 31]]
where f = let v1 = v 1
v2 = v1 .|. (v1 `shiftR` 1)
v3 = v2 .|. (v2 `shiftR` 2)
v4 = v3 .|. (v3 `shiftR` 4)
v5 = v4 .|. (v4 `shiftR` 8)
v6 = v5 .|. (v5 `shiftR` 16)
v7 = v6 + 1
v8 = v7 + oneIf (v7 == 0)
in v8
find :: [Word32] -> Word32
find [] = 1
find (x:xs)
| v > x = find xs
| True = x
zeroInWord :: Proved (Word32 -> Bool)
zeroInWord v = hasZero == fastHasZero
where b3 = (v .&. 0xFF000000) == 0
b2 = (v .&. 0x00FF0000) == 0
b1 = (v .&. 0x0000FF00) == 0
b0 = (v .&. 0x000000FF) == 0
hasZero = b3 || b2 || b1 || b0
fastHasZero = ((v 0x01010101) .&. complement v .&. 0x80808080) /= 0