{-# LANGUAGE CPP #-}
#ifndef HADDOCK
{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}
#endif
{-# OPTIONS_GHC -Wall -Werror #-}
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 :: forall a. Eq a => a -> [a] -> Bool
elem a
_ [] = Bool
False
elem a
k (a
x:[a]
xs) = a
k a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x Bool -> Bool -> Bool
|| a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
elem a
k [a]
xs
oneIf :: Num a => Bool -> a
oneIf :: forall a. Num a => Bool -> a
oneIf Bool
True = a
1
oneIf Bool
False = a
0
fastMinCorrect :: Proved (Int -> Int -> Bool)
fastMinCorrect :: Proved (Int -> Int -> Bool)
fastMinCorrect Int
x Int
y = Int
m Proved (Int -> Int -> Bool)
forall a. Eq a => a -> a -> Bool
== Int
fm
where m :: Int
m = if Int
x Proved (Int -> Int -> Bool)
forall a. Ord a => a -> a -> Bool
< Int
y then Int
x else Int
y
fm :: Int
fm = Int
y Int -> Int -> Int
forall a. Bits a => a -> a -> a
`xor` ((Int
x Int -> Int -> Int
forall a. Bits a => a -> a -> a
`xor` Int
y) Int -> Int -> Int
forall a. Bits a => a -> a -> a
.&. (-(Bool -> Int
forall a. Num a => Bool -> a
oneIf (Int
x Proved (Int -> Int -> Bool)
forall a. Ord a => a -> a -> Bool
< Int
y))));
fastMaxCorrect :: Proved (Int -> Int -> Bool)
fastMaxCorrect :: Proved (Int -> Int -> Bool)
fastMaxCorrect Int
x Int
y = Int
m Proved (Int -> Int -> Bool)
forall a. Eq a => a -> a -> Bool
== Int
fm
where m :: Int
m = if Int
x Proved (Int -> Int -> Bool)
forall a. Ord a => a -> a -> Bool
< Int
y then Int
y else Int
x
fm :: Int
fm = Int
x Int -> Int -> Int
forall a. Bits a => a -> a -> a
`xor` ((Int
x Int -> Int -> Int
forall a. Bits a => a -> a -> a
`xor` Int
y) Int -> Int -> Int
forall a. Bits a => a -> a -> a
.&. (-(Bool -> Int
forall a. Num a => Bool -> a
oneIf (Int
x Proved (Int -> Int -> Bool)
forall a. Ord a => a -> a -> Bool
< Int
y))));
oppositeSignsCorrect :: Proved (Int -> Int -> Bool)
oppositeSignsCorrect :: Proved (Int -> Int -> Bool)
oppositeSignsCorrect Int
x Int
y = Bool
r Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
os
where r :: Bool
r = (Int
x Proved (Int -> Int -> Bool)
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
&& Int
y Proved (Int -> Int -> Bool)
forall a. Ord a => a -> a -> Bool
>= Int
0) Bool -> Bool -> Bool
|| (Int
x Proved (Int -> Int -> Bool)
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
y Proved (Int -> Int -> Bool)
forall a. Ord a => a -> a -> Bool
< Int
0)
os :: Bool
os = (Int
x Int -> Int -> Int
forall a. Bits a => a -> a -> a
`xor` Int
y) Proved (Int -> Int -> Bool)
forall a. Ord a => a -> a -> Bool
< Int
0
conditionalSetClearCorrect :: Proved (Bool -> Word32 -> Word32 -> Bool)
conditionalSetClearCorrect :: Proved (Bool -> Word32 -> Word32 -> Bool)
conditionalSetClearCorrect Bool
f Word32
m Word32
w = Word32
r Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Word32
r'
where r :: Word32
r | Bool
f = Word32
w Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. Word32
m
| Bool
True = Word32
w Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32 -> Word32
forall a. Bits a => a -> a
complement Word32
m
r' :: Word32
r' = Word32
w Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
`xor` ((-(Bool -> Word32
forall a. Num a => Bool -> a
oneIf Bool
f) Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
`xor` Word32
w) Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
m)
powerOfTwoCorrect :: Proved (Word32 -> Bool)
powerOfTwoCorrect :: Word32 -> Bool
powerOfTwoCorrect Word32
v = Bool
f Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (Word32
v Word32 -> [Word32] -> Bool
forall a. Eq a => a -> [a] -> Bool
`elem` [Word32
2Word32 -> Word32 -> Word32
forall a b. (Num a, Integral b) => a -> b -> a
^Word32
i | Word32
i <- [(Word32
0 :: Word32) .. Word32
31]])
where f :: Bool
f = (Word32
v Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word32
0) Bool -> Bool -> Bool
&& ((Word32
v Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. (Word32
vWord32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
-Word32
1)) Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Word32
0)
maskedMergeCorrect :: Proved (Word32 -> Word32 -> Word32 -> Bool)
maskedMergeCorrect :: Proved (Word32 -> Word32 -> Word32 -> Bool)
maskedMergeCorrect Word32
a Word32
b Word32
mask = Word32
slow Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Word32
fast
where slow :: Word32
slow = (Word32
a Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32 -> Word32
forall a. Bits a => a -> a
complement Word32
mask) Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. (Word32
b Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
mask)
fast :: Word32
fast = Word32
a Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
`xor` ((Word32
a Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
`xor` Word32
b) Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
mask)
roundPowerOfTwoCorrect :: Proved (Word32 -> Bool)
roundPowerOfTwoCorrect :: Word32 -> Bool
roundPowerOfTwoCorrect Word32
v = Word32
f Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== [Word32] -> Word32
find [Word32
2Word32 -> Word32 -> Word32
forall a b. (Num a, Integral b) => a -> b -> a
^Word32
i | Word32
i <- [(Word32
0 :: Word32) .. Word32
31]]
where f :: Word32
f = let v1 :: Word32
v1 = Word32
v Word32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
- Word32
1
v2 :: Word32
v2 = Word32
v1 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. (Word32
v1 Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
`shiftR` Int
1)
v3 :: Word32
v3 = Word32
v2 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. (Word32
v2 Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
`shiftR` Int
2)
v4 :: Word32
v4 = Word32
v3 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. (Word32
v3 Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
`shiftR` Int
4)
v5 :: Word32
v5 = Word32
v4 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. (Word32
v4 Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
`shiftR` Int
8)
v6 :: Word32
v6 = Word32
v5 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. (Word32
v5 Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
`shiftR` Int
16)
v7 :: Word32
v7 = Word32
v6 Word32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
+ Word32
1
v8 :: Word32
v8 = Word32
v7 Word32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
+ Bool -> Word32
forall a. Num a => Bool -> a
oneIf (Word32
v7 Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Word32
0)
in Word32
v8
find :: [Word32] -> Word32
find :: [Word32] -> Word32
find [] = Word32
1
find (Word32
x:[Word32]
xs)
| Word32
v Word32 -> Word32 -> Bool
forall a. Ord a => a -> a -> Bool
> Word32
x = [Word32] -> Word32
find [Word32]
xs
| Bool
True = Word32
x
zeroInWord :: Proved (Word32 -> Bool)
zeroInWord :: Word32 -> Bool
zeroInWord Word32
v = Bool
hasZero Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
fastHasZero
where b3 :: Bool
b3 = (Word32
v Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0xFF000000) Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Word32
0
b2 :: Bool
b2 = (Word32
v Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0x00FF0000) Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Word32
0
b1 :: Bool
b1 = (Word32
v Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0x0000FF00) Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Word32
0
b0 :: Bool
b0 = (Word32
v Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0x000000FF) Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Word32
0
hasZero :: Bool
hasZero = Bool
b3 Bool -> Bool -> Bool
|| Bool
b2 Bool -> Bool -> Bool
|| Bool
b1 Bool -> Bool -> Bool
|| Bool
b0
fastHasZero :: Bool
fastHasZero = ((Word32
v Word32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
- Word32
0x01010101) Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32 -> Word32
forall a. Bits a => a -> a
complement Word32
v Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0x80808080) Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word32
0