-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Plugin.Examples.BitTricks
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Checks the correctness of a few tricks from the large collection found in:
--      <https://graphics.stanford.edu/~seander/bithacks.html>
-----------------------------------------------------------------------------

{-# 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)

-- | SBVPlugin can only see definitions in the current module. So we define `elem` ourselves.
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

-- | Returns 1 if bool is @True@
oneIf :: Num a => Bool -> a
oneIf :: forall a. Num a => Bool -> a
oneIf Bool
True  = a
1
oneIf Bool
False = a
0

-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>
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))));

-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>
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))));

-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns>
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

-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching>
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)

-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2>
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)

-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#MaskedMerge>
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)

-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#RoundUpPowerOf2>
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

        -- walk down the powers and return the closest one up
        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

-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#ZeroInWord>
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