{-# LANGUAGE BangPatterns        #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE Safe                #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
-- | Fixed-'Wrd'th (unsigned) integers.
module Data.Wrd (
    Wrd (..),
    -- * Showing
    explicitShow,
    explicitShowsPrec,
    -- * Conversions
    toNatural,
    -- * Universe
    universe,
    -- * Bits
    --
    -- | We have implementation of some 'Bits' members, which doesn't
    -- need 'N.SNatI' constraint.
    xor,
    (.&.),
    (.|.),
    complement,
    complement2,
    shiftR,
    shiftL,
    rotateL,
    rotateR,
    popCount,
    setBit,
    clearBit,
    complementBit,
    testBit,
    -- * Extras
    shiftL1,
    shiftR1,
    rotateL1,
    rotateR1,
    ) where

import Control.DeepSeq (NFData (..))
import Data.Hashable   (Hashable (..))
import Data.Nat        (Nat (..))
import Data.Proxy      (Proxy (..))
import Data.Typeable   (Typeable)
import Numeric.Natural (Natural)

import qualified Data.Type.Nat   as N
import qualified Test.QuickCheck as QC

import qualified Data.Bits as I (Bits (..), FiniteBits (..))

-- $setup
-- >>> :set -XDataKinds
-- >>> import Data.Nat (Nat(..))
-- >>> import qualified Data.Type.Nat as N

-------------------------------------------------------------------------------
-- Data
-------------------------------------------------------------------------------

-- | Fixed-width unsigned integers, 'Wrd's for short.
--
-- The number is thought to be stored in big-endian format,
-- i.e. most-significant bit first. (as in binary literals).
--
data Wrd (n :: Nat) where
    WE :: Wrd 'Z
    W0 :: Wrd n -> Wrd ('S n)
    W1 :: Wrd n -> Wrd ('S n)
  deriving (Typeable)

deriving instance Eq (Wrd n)

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

instance Ord (Wrd n) where
    compare :: Wrd n -> Wrd n -> Ordering
compare Wrd n
WE Wrd n
WE = Ordering
EQ
    compare (W0 Wrd n
a) (W0 Wrd n
b) = Wrd n -> Wrd n -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Wrd n
a Wrd n
Wrd n
b
    compare (W0 Wrd n
_) (W1 Wrd n
_) = Ordering
LT
    compare (W1 Wrd n
_) (W0 Wrd n
_) = Ordering
GT
    compare (W1 Wrd n
a) (W1 Wrd n
b) = Wrd n -> Wrd n -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Wrd n
a Wrd n
Wrd n
b

-- | 'Wrd' is printed as a binary literal.
--
-- >>> let i = W1 $ W0 $ W1 $ W0 WE
-- >>> i
-- 0b1010
--
-- >>> explicitShow i
-- "W1 $ W0 $ W1 $ W0 WE"
--
-- At the time being, there is no 'Num' instance.
--
instance Show (Wrd n) where
    showsPrec :: Int -> Wrd n -> ShowS
showsPrec Int
_ Wrd n
WE = String -> ShowS
showString String
"WE"
    showsPrec Int
_ Wrd n
w  = String -> ShowS
showString String
"0b" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> ShowS -> ShowS) -> ShowS -> [Bool] -> ShowS
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Bool -> ShowS -> ShowS
forall {a}. Bool -> (a -> String) -> a -> String
f ShowS
forall a. a -> a
id (Wrd n -> [Bool]
forall (m :: Nat). Wrd m -> [Bool]
goBits Wrd n
w)
      where
        f :: Bool -> (a -> String) -> a -> String
f Bool
True  a -> String
acc = Char -> ShowS
showChar Char
'1' ShowS -> (a -> String) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
acc
        f Bool
False a -> String
acc = Char -> ShowS
showChar Char
'0' ShowS -> (a -> String) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
acc

        goBits :: Wrd m -> [Bool]
        goBits :: forall (m :: Nat). Wrd m -> [Bool]
goBits Wrd m
WE = []
        goBits (W0 Wrd n
n) = Bool
False Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: Wrd n -> [Bool]
forall (m :: Nat). Wrd m -> [Bool]
goBits Wrd n
n
        goBits (W1 Wrd n
n) = Bool
True  Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: Wrd n -> [Bool]
forall (m :: Nat). Wrd m -> [Bool]
goBits Wrd n
n

instance NFData (Wrd n) where
    rnf :: Wrd n -> ()
rnf Wrd n
WE     = ()
    rnf (W0 Wrd n
w) = Wrd n -> ()
forall a. NFData a => a -> ()
rnf Wrd n
w
    rnf (W1 Wrd n
w) = Wrd n -> ()
forall a. NFData a => a -> ()
rnf Wrd n
w

instance Hashable (Wrd n) where
    hashWithSalt :: Int -> Wrd n -> Int
hashWithSalt Int
salt Wrd n
WE     = Int
salt Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int)
    hashWithSalt Int
salt (W0 Wrd n
w) = Int
salt Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) Int -> Wrd n -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Wrd n
w
    hashWithSalt Int
salt (W1 Wrd n
w) = Int
salt Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2 :: Int) Int -> Wrd n -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Wrd n
w

instance N.SNatI n => Bounded (Wrd n) where
    minBound :: Wrd n
minBound = Wrd 'Z
-> (forall (m :: Nat). SNatI m => Wrd m -> Wrd ('S m)) -> Wrd n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Wrd 'Z
WE Wrd m -> Wrd ('S m)
forall (m :: Nat). SNatI m => Wrd m -> Wrd ('S m)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0
    maxBound :: Wrd n
maxBound = Wrd 'Z
-> (forall (m :: Nat). SNatI m => Wrd m -> Wrd ('S m)) -> Wrd n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Wrd 'Z
WE Wrd m -> Wrd ('S m)
forall (m :: Nat). SNatI m => Wrd m -> Wrd ('S m)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1

instance N.SNatI n => Num (Wrd n) where
    fromInteger :: Integer -> Wrd n
fromInteger = (Integer, Wrd n) -> Wrd n
forall a b. (a, b) -> b
snd ((Integer, Wrd n) -> Wrd n)
-> (Integer -> (Integer, Wrd n)) -> Integer -> Wrd n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> (Integer, Bool)) -> Integer -> (Integer, Wrd n)
forall s (n :: Nat). SNatI n => (s -> (s, Bool)) -> s -> (s, Wrd n)
wrdScanl0 Integer -> (Integer, Bool)
f where
        f :: Integer -> (Integer, Bool)
        f :: Integer -> (Integer, Bool)
f Integer
i =
            let (Integer
i', Integer
m) = Integer
i Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`divMod` Integer
2
            in (Integer
i', Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0)

    Wrd n
a + :: Wrd n -> Wrd n -> Wrd n
+ Wrd n
b = (Bool, Wrd n) -> Wrd n
forall a b. (a, b) -> b
snd ((Bool -> Bool -> Bool -> (Bool, Bool))
-> Bool -> Wrd n -> Wrd n -> (Bool, Wrd n)
forall s (n :: Nat).
(s -> Bool -> Bool -> (s, Bool))
-> s -> Wrd n -> Wrd n -> (s, Wrd n)
wrdScanl2 Bool -> Bool -> Bool -> (Bool, Bool)
f Bool
False Wrd n
a Wrd n
b) where
        f :: Bool -> Bool -> Bool -> (Bool, Bool)
f Bool
False Bool
False Bool
False = (Bool
False, Bool
False)
        f Bool
False Bool
False Bool
True  = (Bool
False, Bool
True)
        f Bool
False Bool
True  Bool
False = (Bool
False, Bool
True)
        f Bool
False Bool
True  Bool
True  = (Bool
True,  Bool
False)
        f Bool
True  Bool
False Bool
False = (Bool
False, Bool
True)
        f Bool
True  Bool
False Bool
True  = (Bool
True,  Bool
False)
        f Bool
True  Bool
True  Bool
False = (Bool
True,  Bool
False)
        f Bool
True  Bool
True  Bool
True  = (Bool
True,  Bool
True)

    Wrd n
a * :: Wrd n -> Wrd n -> Wrd n
* Wrd n
b = (Wrd n, Wrd n) -> Wrd n
forall a b. (a, b) -> b
snd ((Wrd n, Wrd n) -> Wrd n) -> (Wrd n, Wrd n) -> Wrd n
forall a b. (a -> b) -> a -> b
$ ((Wrd n, Wrd n), Wrd n) -> (Wrd n, Wrd n)
forall a b. (a, b) -> a
fst (((Wrd n, Wrd n), Wrd n) -> (Wrd n, Wrd n))
-> ((Wrd n, Wrd n), Wrd n) -> (Wrd n, Wrd n)
forall a b. (a -> b) -> a -> b
$ ((Wrd n, Wrd n) -> Bool -> ((Wrd n, Wrd n), Bool))
-> (Wrd n, Wrd n) -> Wrd n -> ((Wrd n, Wrd n), Wrd n)
forall s (n :: Nat).
(s -> Bool -> (s, Bool)) -> s -> Wrd n -> (s, Wrd n)
wrdScanl (Wrd n, Wrd n) -> Bool -> ((Wrd n, Wrd n), Bool)
f (Wrd n
a, Wrd n
forall a. Bits a => a
I.zeroBits) Wrd n
b where
        f :: (Wrd n, Wrd n) -> Bool -> ((Wrd n, Wrd n), Bool)
        f :: (Wrd n, Wrd n) -> Bool -> ((Wrd n, Wrd n), Bool)
f (Wrd n
a', Wrd n
acc) Bool
True  = ((Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n
shiftL1 Wrd n
a', Wrd n
a' Wrd n -> Wrd n -> Wrd n
forall a. Num a => a -> a -> a
+ Wrd n
acc), Bool
False)
        f (Wrd n
a', Wrd n
acc) Bool
False = ((Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n
shiftL1 Wrd n
a', Wrd n
acc), Bool
False)

    abs :: Wrd n -> Wrd n
abs    = Wrd n -> Wrd n
forall a. a -> a
id
    negate :: Wrd n -> Wrd n
negate = Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n
complement2

    signum :: Wrd n -> Wrd n
signum = Bool -> Wrd n -> Wrd n
forall (m :: Nat). Bool -> Wrd m -> Wrd m
go Bool
False where
        go :: Bool -> Wrd m -> Wrd m
        go :: forall (m :: Nat). Bool -> Wrd m -> Wrd m
go Bool
_     Wrd m
WE      = Wrd m
Wrd 'Z
WE
        go Bool
True  (W0 Wrd n
WE) = Wrd 'Z -> Wrd ('S 'Z)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd 'Z
WE
        go Bool
False (W0 Wrd n
WE) = Wrd 'Z -> Wrd ('S 'Z)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd 'Z
WE
        go Bool
True  (W1 Wrd n
WE) = Wrd 'Z -> Wrd ('S 'Z)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd 'Z
WE
        go Bool
False (W1 Wrd n
WE) = Wrd 'Z -> Wrd ('S 'Z)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd 'Z
WE
        go Bool
b     (W0 Wrd n
w)  = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Bool -> Wrd n -> Wrd n
forall (m :: Nat). Bool -> Wrd m -> Wrd m
go Bool
b Wrd n
w)
        go Bool
_     (W1 Wrd n
w)  = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Bool -> Wrd n -> Wrd n
forall (m :: Nat). Bool -> Wrd m -> Wrd m
go Bool
True Wrd n
w)

-------------------------------------------------------------------------------
-- Bits & FiniteBits
-------------------------------------------------------------------------------

-- |
--
-- >>> let u = W0 $ W0 $ W1 $ W1 WE
-- >>> let v = W0 $ W1 $ W0 $ W1 WE
-- >>> (u, v)
-- (0b0011,0b0101)
--
-- >>> (complement u, complement v)
-- (0b1100,0b1010)
--
-- >>> (u .&. v, u .|. v, u `xor` v)
-- (0b0001,0b0111,0b0110)
--
-- >>> (shiftR v 1, shiftL v 1)
-- (0b0010,0b1010)
--
-- >>> (rotateR u 1, rotateL u 3)
-- (0b1001,0b1001)
--
-- >>> popCount u
-- 2
--
instance N.SNatI n => I.Bits (Wrd n) where
    complement :: Wrd n -> Wrd n
complement = Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n
complement
    .&. :: Wrd n -> Wrd n -> Wrd n
(.&.) = Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
(.&.)
    .|. :: Wrd n -> Wrd n -> Wrd n
(.|.) = Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
(.|.)
    xor :: Wrd n -> Wrd n -> Wrd n
xor   = Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
xor

    isSigned :: Wrd n -> Bool
isSigned Wrd n
_ = Bool
False

    shiftR :: Wrd n -> Int -> Wrd n
shiftR = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
shiftR
    shiftL :: Wrd n -> Int -> Wrd n
shiftL = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
shiftL
    rotateR :: Wrd n -> Int -> Wrd n
rotateR = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
rotateR
    rotateL :: Wrd n -> Int -> Wrd n
rotateL = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
rotateL

    clearBit :: Wrd n -> Int -> Wrd n
clearBit      = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
clearBit
    complementBit :: Wrd n -> Int -> Wrd n
complementBit = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
complementBit
    setBit :: Wrd n -> Int -> Wrd n
setBit        = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
setBit
    testBit :: Wrd n -> Int -> Bool
testBit       = Wrd n -> Int -> Bool
forall (n :: Nat). Wrd n -> Int -> Bool
testBit

    zeroBits :: Wrd n
zeroBits = Wrd 'Z
-> (forall (m :: Nat). SNatI m => Wrd m -> Wrd ('S m)) -> Wrd n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Wrd 'Z
WE Wrd m -> Wrd ('S m)
forall (m :: Nat). SNatI m => Wrd m -> Wrd ('S m)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0

    popCount :: Wrd n -> Int
popCount = Wrd n -> Int
forall (n :: Nat). Wrd n -> Int
popCount

    -- this is good enough
    bit :: Int -> Wrd n
bit = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
setBit Wrd n
forall a. Bits a => a
I.zeroBits

    bitSizeMaybe :: Wrd n -> Maybe Int
bitSizeMaybe = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (Wrd n -> Int) -> Wrd n -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> Int
forall b. FiniteBits b => b -> Int
I.finiteBitSize
    bitSize :: Wrd n -> Int
bitSize      = Wrd n -> Int
forall b. FiniteBits b => b -> Int
I.finiteBitSize

instance N.SNatI n => I.FiniteBits (Wrd n) where
    finiteBitSize :: Wrd n -> Int
finiteBitSize Wrd n
_ = Proxy @Nat n -> Int
forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (Proxy @Nat n
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy n)
    countLeadingZeros :: Wrd n -> Int
countLeadingZeros = Wrd n -> Int
forall (n :: Nat). Wrd n -> Int
countLeadingZeros

testBit :: Wrd n -> Int -> Bool
testBit :: forall (n :: Nat). Wrd n -> Int -> Bool
testBit Wrd n
w0 Int
i = (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd (Int -> Wrd n -> (Int, Bool)
forall (n :: Nat). Int -> Wrd n -> (Int, Bool)
go Int
0 Wrd n
w0) where
    go :: Int -> Wrd n -> (Int, Bool)
    go :: forall (n :: Nat). Int -> Wrd n -> (Int, Bool)
go Int
j Wrd n
WE = (Int
j, Bool
False)
    go Int
j (W0 Wrd n
w) =
        let j'' :: Int
j''      = Int -> Int
forall a. Enum a => a -> a
succ Int
j'
            (Int
j', Bool
b') = Int -> Wrd n -> (Int, Bool)
forall (n :: Nat). Int -> Wrd n -> (Int, Bool)
go Int
j Wrd n
w
        in (Int
j'', if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j' then Bool
False else Bool
b')
    go Int
j (W1 Wrd n
w) =
        let j'' :: Int
j''      = Int -> Int
forall a. Enum a => a -> a
succ Int
j'
            (Int
j', Bool
b') = Int -> Wrd n -> (Int, Bool)
forall (n :: Nat). Int -> Wrd n -> (Int, Bool)
go Int
j Wrd n
w
        in (Int
j'', if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j' then Bool
True else Bool
b')

clearBit          :: Wrd n -> Int -> Wrd n
clearBit :: forall (n :: Nat). Wrd n -> Int -> Wrd n
clearBit      Wrd n
w Int
i = (Int -> Bool -> Bool) -> Wrd n -> Wrd n
forall (n :: Nat). (Int -> Bool -> Bool) -> Wrd n -> Wrd n
mapWithBit (\Int
j Bool
b -> if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i then Bool
False else Bool
b) Wrd n
w

setBit            :: Wrd n -> Int -> Wrd n
setBit :: forall (n :: Nat). Wrd n -> Int -> Wrd n
setBit        Wrd n
w Int
i = (Int -> Bool -> Bool) -> Wrd n -> Wrd n
forall (n :: Nat). (Int -> Bool -> Bool) -> Wrd n -> Wrd n
mapWithBit (\Int
j Bool
b -> if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i then Bool
True  else Bool
b) Wrd n
w

complementBit     :: Wrd n -> Int -> Wrd n
complementBit :: forall (n :: Nat). Wrd n -> Int -> Wrd n
complementBit Wrd n
w Int
i = (Int -> Bool -> Bool) -> Wrd n -> Wrd n
forall (n :: Nat). (Int -> Bool -> Bool) -> Wrd n -> Wrd n
mapWithBit (\Int
j Bool
b -> if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i then Bool -> Bool
not Bool
b else Bool
b) Wrd n
w

complement :: Wrd n -> Wrd n
complement :: forall (n :: Nat). Wrd n -> Wrd n
complement Wrd n
WE     = Wrd n
Wrd 'Z
WE
complement (W0 Wrd n
w) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n
complement Wrd n
w)
complement (W1 Wrd n
w) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n
complement Wrd n
w)

-- | @'complement2' w = 'complement' w + 1@
complement2 :: Wrd n -> Wrd n
complement2 :: forall (n :: Nat). Wrd n -> Wrd n
complement2 = (Bool, Wrd n) -> Wrd n
forall a b. (a, b) -> b
snd ((Bool, Wrd n) -> Wrd n)
-> (Wrd n -> (Bool, Wrd n)) -> Wrd n -> Wrd n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Bool -> (Bool, Bool)) -> Bool -> Wrd n -> (Bool, Wrd n)
forall s (n :: Nat).
(s -> Bool -> (s, Bool)) -> s -> Wrd n -> (s, Wrd n)
wrdScanl Bool -> Bool -> (Bool, Bool)
f Bool
True where
    f :: Bool -> Bool -> (Bool, Bool)
    f :: Bool -> Bool -> (Bool, Bool)
f Bool
False Bool
False = (Bool
False, Bool
True)
    f Bool
False Bool
True  = (Bool
False, Bool
False)
    f Bool
True  Bool
False = (Bool
True,  Bool
False)
    f Bool
True  Bool
True  = (Bool
False, Bool
True)

(.&.) :: Wrd n -> Wrd n -> Wrd n
Wrd n
WE   .&. :: forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
.&. Wrd n
_    = Wrd n
Wrd 'Z
WE
W1 Wrd n
a .&. W1 Wrd n
b = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd n
a Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
.&. Wrd n
Wrd n
b)
W1 Wrd n
a .&. W0 Wrd n
b = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd n
a Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
.&. Wrd n
Wrd n
b)
W0 Wrd n
a .&. W1 Wrd n
b = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd n
a Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
.&. Wrd n
Wrd n
b)
W0 Wrd n
a .&. W0 Wrd n
b = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd n
a Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
.&. Wrd n
Wrd n
b)

(.|.) :: Wrd n -> Wrd n -> Wrd n
Wrd n
WE   .|. :: forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
.|. Wrd n
_    = Wrd n
Wrd 'Z
WE
W1 Wrd n
a .|. W1 Wrd n
b = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd n
a Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
.|. Wrd n
Wrd n
b)
W1 Wrd n
a .|. W0 Wrd n
b = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd n
a Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
.|. Wrd n
Wrd n
b)
W0 Wrd n
a .|. W1 Wrd n
b = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd n
a Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
.|. Wrd n
Wrd n
b)
W0 Wrd n
a .|. W0 Wrd n
b = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd n
a Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
.|. Wrd n
Wrd n
b)

xor :: Wrd n -> Wrd n -> Wrd n
xor :: forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
xor Wrd n
WE      Wrd n
_     = Wrd n
Wrd 'Z
WE
xor (W1 Wrd n
a) (W1 Wrd n
b) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
xor Wrd n
a Wrd n
Wrd n
b)
xor (W1 Wrd n
a) (W0 Wrd n
b) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
xor Wrd n
a Wrd n
Wrd n
b)
xor (W0 Wrd n
a) (W1 Wrd n
b) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
xor Wrd n
a Wrd n
Wrd n
b)
xor (W0 Wrd n
a) (W0 Wrd n
b) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd n -> Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n -> Wrd n
xor Wrd n
a Wrd n
Wrd n
b)

shiftR :: Wrd n -> Int -> Wrd n
shiftR :: forall (n :: Nat). Wrd n -> Int -> Wrd n
shiftR Wrd n
w Int
n
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = Wrd n
w
    | Bool
otherwise = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
shiftR (Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n
shiftR1 Wrd n
w) (Int -> Int
forall a. Enum a => a -> a
pred Int
n)

shiftL :: Wrd n -> Int -> Wrd n
shiftL :: forall (n :: Nat). Wrd n -> Int -> Wrd n
shiftL Wrd n
w Int
n
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = Wrd n
w
    | Bool
otherwise = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
shiftL (Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n
shiftL1 Wrd n
w) (Int -> Int
forall a. Enum a => a -> a
pred Int
n)

rotateR :: Wrd n -> Int -> Wrd n
rotateR :: forall (n :: Nat). Wrd n -> Int -> Wrd n
rotateR Wrd n
w Int
n
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = Wrd n
w
    | Bool
otherwise = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
rotateR (Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n
rotateR1 Wrd n
w) (Int -> Int
forall a. Enum a => a -> a
pred Int
n)

rotateL :: Wrd n -> Int -> Wrd n
rotateL :: forall (n :: Nat). Wrd n -> Int -> Wrd n
rotateL Wrd n
w Int
n
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = Wrd n
w
    | Bool
otherwise = Wrd n -> Int -> Wrd n
forall (n :: Nat). Wrd n -> Int -> Wrd n
rotateL (Wrd n -> Wrd n
forall (n :: Nat). Wrd n -> Wrd n
rotateL1 Wrd n
w) (Int -> Int
forall a. Enum a => a -> a
pred Int
n)

popCount :: Wrd n -> Int
popCount :: forall (n :: Nat). Wrd n -> Int
popCount = Int -> Wrd n -> Int
forall (n :: Nat). Int -> Wrd n -> Int
go Int
0 where
    go :: Int -> Wrd m -> Int
    go :: forall (n :: Nat). Int -> Wrd n -> Int
go !Int
acc Wrd m
WE     = Int
acc
    go !Int
acc (W0 Wrd n
w) = Int -> Wrd n -> Int
forall (n :: Nat). Int -> Wrd n -> Int
go Int
acc Wrd n
w
    go !Int
acc (W1 Wrd n
w) = Int -> Wrd n -> Int
forall (n :: Nat). Int -> Wrd n -> Int
go (Int -> Int
forall a. Enum a => a -> a
succ Int
acc) Wrd n
w

shiftL1 :: Wrd n -> Wrd n
shiftL1 :: forall (n :: Nat). Wrd n -> Wrd n
shiftL1 Wrd n
WE = Wrd n
Wrd 'Z
WE
shiftL1 (W0 Wrd n
w) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
pushBack Wrd n
w
shiftL1 (W1 Wrd n
w) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
pushBack Wrd n
w

shiftR1 :: Wrd n -> Wrd n
shiftR1 :: forall (n :: Nat). Wrd n -> Wrd n
shiftR1 Wrd n
WE       = Wrd n
Wrd 'Z
WE
shiftR1 w :: Wrd n
w@(W0 Wrd n
_) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd ('S n) -> Wrd n
forall (n :: Nat). Wrd ('S n) -> Wrd n
dropLast Wrd n
Wrd ('S n)
w)
shiftR1 w :: Wrd n
w@(W1 Wrd n
_) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd ('S n) -> Wrd n
forall (n :: Nat). Wrd ('S n) -> Wrd n
dropLast Wrd n
Wrd ('S n)
w)

rotateL1 :: Wrd n -> Wrd n
rotateL1 :: forall (n :: Nat). Wrd n -> Wrd n
rotateL1 Wrd n
WE = Wrd n
Wrd 'Z
WE
rotateL1 (W0 Wrd n
w) = Wrd n -> Bool -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Bool -> Wrd ('S n)
pushBack' Wrd n
w Bool
False
rotateL1 (W1 Wrd n
w) = Wrd n -> Bool -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Bool -> Wrd ('S n)
pushBack' Wrd n
w Bool
True

rotateR1 :: Wrd n -> Wrd n
rotateR1 :: forall (n :: Nat). Wrd n -> Wrd n
rotateR1 Wrd n
WE       = Wrd n
Wrd 'Z
WE
rotateR1 w :: Wrd n
w@(W0 Wrd n
_) = case Wrd ('S n) -> (Bool, Wrd n)
forall (n :: Nat). Wrd ('S n) -> (Bool, Wrd n)
dropLast' Wrd n
Wrd ('S n)
w of
    (Bool
True, Wrd n
w')  -> Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd n
w'
    (Bool
False, Wrd n
w') -> Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd n
w'
rotateR1 w :: Wrd n
w@(W1 Wrd n
_) = case Wrd ('S n) -> (Bool, Wrd n)
forall (n :: Nat). Wrd ('S n) -> (Bool, Wrd n)
dropLast' Wrd n
Wrd ('S n)
w of
    (Bool
True, Wrd n
w')  -> Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd n
w'
    (Bool
False, Wrd n
w') -> Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd n
w'

pushBack ::  Wrd n ->  Wrd ('S n)
pushBack :: forall (n :: Nat). Wrd n -> Wrd ('S n)
pushBack Wrd n
WE     = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd n
Wrd 'Z
WE
pushBack (W0 Wrd n
w) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
pushBack Wrd n
w)
pushBack (W1 Wrd n
w) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
pushBack Wrd n
w)

pushBack' ::  Wrd n -> Bool -> Wrd ('S n)
pushBack' :: forall (n :: Nat). Wrd n -> Bool -> Wrd ('S n)
pushBack' Wrd n
WE     Bool
False = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd n
Wrd 'Z
WE
pushBack' Wrd n
WE     Bool
True  = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd n
Wrd 'Z
WE
pushBack' (W0 Wrd n
w) Bool
b     = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd n -> Bool -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Bool -> Wrd ('S n)
pushBack' Wrd n
w Bool
b)
pushBack' (W1 Wrd n
w) Bool
b     = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd n -> Bool -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Bool -> Wrd ('S n)
pushBack' Wrd n
w Bool
b)

dropLast :: Wrd ('S n) -> Wrd n
dropLast :: forall (n :: Nat). Wrd ('S n) -> Wrd n
dropLast (W0 Wrd n
WE)       = Wrd n
Wrd 'Z
WE
dropLast (W1 Wrd n
WE)       = Wrd n
Wrd 'Z
WE
dropLast (W0 w :: Wrd n
w@(W0 Wrd n
_)) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd ('S n) -> Wrd n
forall (n :: Nat). Wrd ('S n) -> Wrd n
dropLast Wrd n
Wrd ('S n)
w)
dropLast (W0 w :: Wrd n
w@(W1 Wrd n
_)) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd ('S n) -> Wrd n
forall (n :: Nat). Wrd ('S n) -> Wrd n
dropLast Wrd n
Wrd ('S n)
w)
dropLast (W1 w :: Wrd n
w@(W0 Wrd n
_)) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd ('S n) -> Wrd n
forall (n :: Nat). Wrd ('S n) -> Wrd n
dropLast Wrd n
Wrd ('S n)
w)
dropLast (W1 w :: Wrd n
w@(W1 Wrd n
_)) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd ('S n) -> Wrd n
forall (n :: Nat). Wrd ('S n) -> Wrd n
dropLast Wrd n
Wrd ('S n)
w)

dropLast' :: Wrd ('S n) -> (Bool, Wrd n)
dropLast' :: forall (n :: Nat). Wrd ('S n) -> (Bool, Wrd n)
dropLast' (W0 Wrd n
WE)       = (Bool
False, Wrd n
Wrd 'Z
WE)
dropLast' (W1 Wrd n
WE)       = (Bool
True, Wrd n
Wrd 'Z
WE)
dropLast' (W0 w :: Wrd n
w@(W0 Wrd n
_)) = (Wrd n -> Wrd n) -> (Bool, Wrd n) -> (Bool, Wrd n)
forall a b. (a -> b) -> (Bool, a) -> (Bool, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n -> Wrd n
Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd ('S n) -> (Bool, Wrd n)
forall (n :: Nat). Wrd ('S n) -> (Bool, Wrd n)
dropLast' Wrd n
Wrd ('S n)
w)
dropLast' (W0 w :: Wrd n
w@(W1 Wrd n
_)) = (Wrd n -> Wrd n) -> (Bool, Wrd n) -> (Bool, Wrd n)
forall a b. (a -> b) -> (Bool, a) -> (Bool, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n -> Wrd n
Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd ('S n) -> (Bool, Wrd n)
forall (n :: Nat). Wrd ('S n) -> (Bool, Wrd n)
dropLast' Wrd n
Wrd ('S n)
w)
dropLast' (W1 w :: Wrd n
w@(W0 Wrd n
_)) = (Wrd n -> Wrd n) -> (Bool, Wrd n) -> (Bool, Wrd n)
forall a b. (a -> b) -> (Bool, a) -> (Bool, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n -> Wrd n
Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd ('S n) -> (Bool, Wrd n)
forall (n :: Nat). Wrd ('S n) -> (Bool, Wrd n)
dropLast' Wrd n
Wrd ('S n)
w)
dropLast' (W1 w :: Wrd n
w@(W1 Wrd n
_)) = (Wrd n -> Wrd n) -> (Bool, Wrd n) -> (Bool, Wrd n)
forall a b. (a -> b) -> (Bool, a) -> (Bool, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n -> Wrd n
Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd ('S n) -> (Bool, Wrd n)
forall (n :: Nat). Wrd ('S n) -> (Bool, Wrd n)
dropLast' Wrd n
Wrd ('S n)
w)

countLeadingZeros :: Wrd n -> Int
countLeadingZeros :: forall (n :: Nat). Wrd n -> Int
countLeadingZeros = Int -> Wrd n -> Int
forall (n :: Nat). Int -> Wrd n -> Int
go Int
0 where
    go :: Int -> Wrd m -> Int
    go :: forall (n :: Nat). Int -> Wrd n -> Int
go !Int
acc Wrd m
WE     = Int
acc
    go !Int
acc (W0 Wrd n
w) = Int -> Wrd n -> Int
forall (n :: Nat). Int -> Wrd n -> Int
go (Int -> Int
forall a. Enum a => a -> a
succ Int
acc) Wrd n
w
    go !Int
acc (W1 Wrd n
_) = Int
acc

-------------------------------------------------------------------------------
-- QuickCheck
-------------------------------------------------------------------------------

instance N.SNatI n => QC.Arbitrary (Wrd n) where
    arbitrary :: Gen (Wrd n)
arbitrary = case SNat n
forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
        SNat n
N.SZ -> Wrd n -> Gen (Wrd n)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Wrd n
Wrd 'Z
WE
        SNat n
N.SS -> [Gen (Wrd n)] -> Gen (Wrd n)
forall a. HasCallStack => [Gen a] -> Gen a
QC.oneof [ (Wrd n1 -> Wrd n) -> Gen (Wrd n1) -> Gen (Wrd n)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n1 -> Wrd n
Wrd n1 -> Wrd ('S n1)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Gen (Wrd n1)
forall a. Arbitrary a => Gen a
QC.arbitrary, (Wrd n1 -> Wrd n) -> Gen (Wrd n1) -> Gen (Wrd n)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n1 -> Wrd n
Wrd n1 -> Wrd ('S n1)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Gen (Wrd n1)
forall a. Arbitrary a => Gen a
QC.arbitrary ]

    shrink :: Wrd n -> [Wrd n]
shrink = Wrd n -> [Wrd n]
forall (n :: Nat). Wrd n -> [Wrd n]
shrink

shrink :: Wrd n -> [Wrd n]
shrink :: forall (n :: Nat). Wrd n -> [Wrd n]
shrink Wrd n
WE = []
shrink (W1 Wrd n
w) = Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd n
w Wrd n -> [Wrd n] -> [Wrd n]
forall a. a -> [a] -> [a]
: (Wrd n -> Wrd n) -> [Wrd n] -> [Wrd n]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n -> Wrd n
Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 (Wrd n -> [Wrd n]
forall (n :: Nat). Wrd n -> [Wrd n]
shrink Wrd n
w)
shrink (W0 Wrd n
w) = (Wrd n -> Wrd n) -> [Wrd n] -> [Wrd n]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n -> Wrd n
Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 (Wrd n -> [Wrd n]
forall (n :: Nat). Wrd n -> [Wrd n]
shrink Wrd n
w)

instance QC.CoArbitrary (Wrd n) where
    coarbitrary :: forall b. Wrd n -> Gen b -> Gen b
coarbitrary Wrd n
WE     = Gen b -> Gen b
forall a. a -> a
id
    coarbitrary (W0 Wrd n
w) = (Bool, Wrd n) -> Gen b -> Gen b
forall b. (Bool, Wrd n) -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary (Bool
False, Wrd n
w)
    coarbitrary (W1 Wrd n
w) = (Bool, Wrd n) -> Gen b -> Gen b
forall b. (Bool, Wrd n) -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary (Bool
True,  Wrd n
w)

instance N.SNatI n => QC.Function (Wrd n) where
    function :: forall b. (Wrd n -> b) -> Wrd n :-> b
function = case SNat n
forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
        SNat n
N.SZ -> (Wrd n -> ()) -> (() -> Wrd n) -> (Wrd n -> b) -> Wrd n :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (() -> Wrd n -> ()
forall a b. a -> b -> a
const ()) (Wrd n -> () -> Wrd n
forall a b. a -> b -> a
const Wrd n
Wrd 'Z
WE)
        SNat n
N.SS -> (Wrd n -> (Bool, Wrd n1))
-> ((Bool, Wrd n1) -> Wrd n) -> (Wrd n -> b) -> Wrd n :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap Wrd n -> (Bool, Wrd n1)
Wrd ('S n1) -> (Bool, Wrd n1)
forall (n :: Nat). Wrd ('S n) -> (Bool, Wrd n)
toPair (Bool, Wrd n1) -> Wrd n
(Bool, Wrd n1) -> Wrd ('S n1)
forall (m :: Nat). (Bool, Wrd m) -> Wrd ('S m)
fromPair
      where
        toPair :: Wrd ('S m) -> (Bool, Wrd m)
        toPair :: forall (n :: Nat). Wrd ('S n) -> (Bool, Wrd n)
toPair (W0 Wrd n
w) = (Bool
False, Wrd m
Wrd n
w)
        toPair (W1 Wrd n
w) = (Bool
True,  Wrd m
Wrd n
w)

        fromPair :: (Bool, Wrd m) -> Wrd ('S m)
        fromPair :: forall (m :: Nat). (Bool, Wrd m) -> Wrd ('S m)
fromPair (Bool
False, Wrd m
w) = Wrd m -> Wrd ('S m)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd m
w
        fromPair (Bool
True,  Wrd m
w) = Wrd m -> Wrd ('S m)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd m
w

-------------------------------------------------------------------------------
-- Showing
-------------------------------------------------------------------------------

-- | 'show' displaying a structure of @'Wrd' n@
--
-- >>> explicitShow WE
-- "WE"
--
-- >>> explicitShow $ W0 WE
-- "W0 WE"
--
-- >>> explicitShow $ W1 $ W0 $ W1 $ W0 WE
-- "W1 $ W0 $ W1 $ W0 WE"
--
explicitShow :: Wrd n -> String
explicitShow :: forall (n :: Nat). Wrd n -> String
explicitShow Wrd n
w = Int -> Wrd n -> ShowS
forall (n :: Nat). Int -> Wrd n -> ShowS
explicitShowsPrec Int
0 Wrd n
w String
""

-- | 'showsPrec' displaying a structure of @'Wrd' n@.
--
-- >>> explicitShowsPrec 0 (W0 WE) ""
-- "W0 WE"
--
-- >>> explicitShowsPrec 1 (W0 WE) ""
-- "(W0 WE)"
--
explicitShowsPrec :: Int -> Wrd n -> ShowS
explicitShowsPrec :: forall (n :: Nat). Int -> Wrd n -> ShowS
explicitShowsPrec Int
_ Wrd n
WE = String -> ShowS
showString String
"WE"
explicitShowsPrec Int
d Wrd n
w  = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    [Bool] -> ShowS
go (Wrd n -> [Bool]
forall (m :: Nat). Wrd m -> [Bool]
goBits Wrd n
w)
  where
    go :: [Bool] -> ShowS
go []           = String -> ShowS
showString String
"WE"
    go [Bool
False]      = String -> ShowS
showString String
"W0 WE"
    go [Bool
True]       = String -> ShowS
showString String
"W1 WE"
    go (Bool
False : [Bool]
bs) = String -> ShowS
showString String
"W0 $ " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bool] -> ShowS
go [Bool]
bs
    go (Bool
True  : [Bool]
bs) = String -> ShowS
showString String
"W1 $ " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bool] -> ShowS
go [Bool]
bs

    goBits :: Wrd m -> [Bool]
    goBits :: forall (m :: Nat). Wrd m -> [Bool]
goBits Wrd m
WE = []
    goBits (W0 Wrd n
n) = Bool
False Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: Wrd n -> [Bool]
forall (m :: Nat). Wrd m -> [Bool]
goBits Wrd n
n
    goBits (W1 Wrd n
n) = Bool
True  Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: Wrd n -> [Bool]
forall (m :: Nat). Wrd m -> [Bool]
goBits Wrd n
n

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

-- | Convert to 'Natural' number
--
-- >>> let u = W0 $ W1 $ W1 $ W1 $ W0 $ W1 $ W0 WE
-- >>> u
-- 0b0111010
--
-- >>> toNatural u
-- 58
--
-- >>> map toNatural (universe :: [Wrd N.Nat3])
-- [0,1,2,3,4,5,6,7]
--
toNatural :: Wrd n -> Natural
toNatural :: forall (n :: Nat). Wrd n -> Natural
toNatural = Natural -> Wrd n -> Natural
forall (m :: Nat). Natural -> Wrd m -> Natural
go Natural
0 where
    go :: Natural -> Wrd m -> Natural
    go :: forall (m :: Nat). Natural -> Wrd m -> Natural
go !Natural
acc Wrd m
WE = Natural
acc
    go !Natural
acc (W0 Wrd n
w) = Natural -> Wrd n -> Natural
forall (m :: Nat). Natural -> Wrd m -> Natural
go (Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
acc)     Wrd n
w
    go !Natural
acc (W1 Wrd n
w) = Natural -> Wrd n -> Natural
forall (m :: Nat). Natural -> Wrd m -> Natural
go (Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
acc Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1) Wrd n
w

-------------------------------------------------------------------------------
-- Universe
-------------------------------------------------------------------------------

-- | All values, i.e. universe of @'Wrd' @.
--
-- >>> universe :: [Wrd 'Z]
-- [WE]
--
-- >>> universe :: [Wrd N.Nat3]
-- [0b000,0b001,0b010,0b011,0b100,0b101,0b110,0b111]
universe :: forall n. N.SNatI n => [Wrd n]
universe :: forall (n :: Nat). SNatI n => [Wrd n]
universe = Universe n -> [Wrd n]
forall (n :: Nat). Universe n -> [Wrd n]
getUniverse (Universe n -> [Wrd n]) -> Universe n -> [Wrd n]
forall a b. (a -> b) -> a -> b
$ Universe 'Z
-> (forall (m :: Nat). SNatI m => Universe m -> Universe ('S m))
-> Universe n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction ([Wrd 'Z] -> Universe 'Z
forall (n :: Nat). [Wrd n] -> Universe n
Universe [Wrd 'Z
WE]) Universe m -> Universe ('S m)
forall (m :: Nat). SNatI m => Universe m -> Universe ('S m)
forall (m :: Nat). Universe m -> Universe ('S m)
go where
    go :: Universe m -> Universe ('S m)
    go :: forall (m :: Nat). Universe m -> Universe ('S m)
go (Universe [Wrd m]
u) = [Wrd ('S m)] -> Universe ('S m)
forall (n :: Nat). [Wrd n] -> Universe n
Universe ((Wrd m -> Wrd ('S m)) -> [Wrd m] -> [Wrd ('S m)]
forall a b. (a -> b) -> [a] -> [b]
map Wrd m -> Wrd ('S m)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 [Wrd m]
u [Wrd ('S m)] -> [Wrd ('S m)] -> [Wrd ('S m)]
forall a. [a] -> [a] -> [a]
++ (Wrd m -> Wrd ('S m)) -> [Wrd m] -> [Wrd ('S m)]
forall a b. (a -> b) -> [a] -> [b]
map Wrd m -> Wrd ('S m)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 [Wrd m]
u)

newtype Universe n = Universe { forall (n :: Nat). Universe n -> [Wrd n]
getUniverse :: [Wrd n] }

-------------------------------------------------------------------------------
-- Scans
-------------------------------------------------------------------------------

mapWithBit :: (Int -> Bool -> Bool) -> Wrd n -> Wrd n
mapWithBit :: forall (n :: Nat). (Int -> Bool -> Bool) -> Wrd n -> Wrd n
mapWithBit Int -> Bool -> Bool
f = (Int, Wrd n) -> Wrd n
forall a b. (a, b) -> b
snd ((Int, Wrd n) -> Wrd n)
-> (Wrd n -> (Int, Wrd n)) -> Wrd n -> Wrd n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Bool -> (Int, Bool)) -> Int -> Wrd n -> (Int, Wrd n)
forall s (n :: Nat).
(s -> Bool -> (s, Bool)) -> s -> Wrd n -> (s, Wrd n)
wrdScanl Int -> Bool -> (Int, Bool)
g Int
0 where
    g :: Int -> Bool -> (Int, Bool)
g Int
i Bool
b = (Int -> Int
forall a. Enum a => a -> a
succ Int
i, Int -> Bool -> Bool
f Int
i Bool
b)

wrdScanl0 :: forall s n. N.SNatI n => (s -> (s, Bool)) -> s -> (s, Wrd n)
wrdScanl0 :: forall s (n :: Nat). SNatI n => (s -> (s, Bool)) -> s -> (s, Wrd n)
wrdScanl0 s -> (s, Bool)
g = s -> (s, Wrd n)
forall (m :: Nat). SNatI m => s -> (s, Wrd m)
go where
    go :: forall m. N.SNatI m => s -> (s, Wrd m)
    go :: forall (m :: Nat). SNatI m => s -> (s, Wrd m)
go s
s = case SNat m
forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat m of
        SNat m
N.SZ -> (s
s, Wrd m
Wrd 'Z
WE)
        SNat m
N.SS ->
            let (s
s'', Bool
b)  = s -> (s, Bool)
g s
s'
                (s
s' , Wrd n1
w') = s -> (s, Wrd n1)
forall (m :: Nat). SNatI m => s -> (s, Wrd m)
go s
s
            in (s
s'', if Bool
b then Wrd n1 -> Wrd ('S n1)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd n1
w' else Wrd n1 -> Wrd ('S n1)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd n1
w')

wrdScanl :: forall s n. (s -> Bool -> (s, Bool)) -> s ->  Wrd n -> (s, Wrd n)
wrdScanl :: forall s (n :: Nat).
(s -> Bool -> (s, Bool)) -> s -> Wrd n -> (s, Wrd n)
wrdScanl s -> Bool -> (s, Bool)
g = s -> Wrd n -> (s, Wrd n)
forall (m :: Nat). s -> Wrd m -> (s, Wrd m)
go where
    go :: s -> Wrd m -> (s, Wrd m)
    go :: forall (m :: Nat). s -> Wrd m -> (s, Wrd m)
go s
s Wrd m
WE = (s
s, Wrd m
Wrd 'Z
WE)
    go s
s (W0 Wrd n
w) =
        let (s
s'', Bool
b)  = s -> Bool -> (s, Bool)
g s
s' Bool
False
            (s
s' , Wrd n
w') = s -> Wrd n -> (s, Wrd n)
forall (m :: Nat). s -> Wrd m -> (s, Wrd m)
go s
s Wrd n
w
        in (s
s'', if Bool
b then Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd n
w' else Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd n
w')
    go s
s (W1 Wrd n
w) =
        let (s
s'', Bool
b)  = s -> Bool -> (s, Bool)
g s
s' Bool
True
            (s
s' , Wrd n
w') = s -> Wrd n -> (s, Wrd n)
forall (m :: Nat). s -> Wrd m -> (s, Wrd m)
go s
s Wrd n
w
        in (s
s'', if Bool
b then Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd n
w' else Wrd n -> Wrd ('S n)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd n
w')

wrdScanl2 :: forall s n. (s -> Bool -> Bool -> (s, Bool)) -> s ->  Wrd n -> Wrd n -> (s, Wrd n)
wrdScanl2 :: forall s (n :: Nat).
(s -> Bool -> Bool -> (s, Bool))
-> s -> Wrd n -> Wrd n -> (s, Wrd n)
wrdScanl2 s -> Bool -> Bool -> (s, Bool)
g = s -> Wrd n -> Wrd n -> (s, Wrd n)
forall (m :: Nat). s -> Wrd m -> Wrd m -> (s, Wrd m)
go where
    go :: s -> Wrd m -> Wrd m -> (s, Wrd m)
    go :: forall (m :: Nat). s -> Wrd m -> Wrd m -> (s, Wrd m)
go s
s Wrd m
WE Wrd m
_ = (s
s, Wrd m
Wrd 'Z
WE)
    go s
s (W0 Wrd n
w) (W0 Wrd n
w') = s -> Bool -> Bool -> Wrd n -> Wrd n -> (s, Wrd ('S n))
forall (m :: Nat).
s -> Bool -> Bool -> Wrd m -> Wrd m -> (s, Wrd ('S m))
go' s
s Bool
False Bool
False Wrd n
w Wrd n
Wrd n
w'
    go s
s (W0 Wrd n
w) (W1 Wrd n
w') = s -> Bool -> Bool -> Wrd n -> Wrd n -> (s, Wrd ('S n))
forall (m :: Nat).
s -> Bool -> Bool -> Wrd m -> Wrd m -> (s, Wrd ('S m))
go' s
s Bool
False Bool
True  Wrd n
w Wrd n
Wrd n
w'
    go s
s (W1 Wrd n
w) (W0 Wrd n
w') = s -> Bool -> Bool -> Wrd n -> Wrd n -> (s, Wrd ('S n))
forall (m :: Nat).
s -> Bool -> Bool -> Wrd m -> Wrd m -> (s, Wrd ('S m))
go' s
s Bool
True  Bool
False Wrd n
w Wrd n
Wrd n
w'
    go s
s (W1 Wrd n
w) (W1 Wrd n
w') = s -> Bool -> Bool -> Wrd n -> Wrd n -> (s, Wrd ('S n))
forall (m :: Nat).
s -> Bool -> Bool -> Wrd m -> Wrd m -> (s, Wrd ('S m))
go' s
s Bool
True  Bool
True  Wrd n
w Wrd n
Wrd n
w'

    go' :: s -> Bool -> Bool -> Wrd m -> Wrd m -> (s, Wrd ('S m))
    go' :: forall (m :: Nat).
s -> Bool -> Bool -> Wrd m -> Wrd m -> (s, Wrd ('S m))
go' s
s Bool
i Bool
j Wrd m
w Wrd m
u =
        let (s
s'', Bool
b)  = s -> Bool -> Bool -> (s, Bool)
g s
s' Bool
i Bool
j
            (s
s' , Wrd m
v) = s -> Wrd m -> Wrd m -> (s, Wrd m)
forall (m :: Nat). s -> Wrd m -> Wrd m -> (s, Wrd m)
go s
s Wrd m
w Wrd m
u
        in (s
s'', if Bool
b then Wrd m -> Wrd ('S m)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W1 Wrd m
v else Wrd m -> Wrd ('S m)
forall (n :: Nat). Wrd n -> Wrd ('S n)
W0 Wrd m
v)