module Cgm.Data.WordN (
RWord,
toRWord,
fromRWord,
rWord,
WordN(..),
wordNBits,
boolAsWord,
RWordC,
RWord8,
RWord16,
RWord32,
RWord64,
rChangeWord,
rChangeWord',
rAdd,
rWordJoin,
rWordSplit,
rWordBool,
module Cgm.Data.Nat,
module Cgm.Data.Super
) where
import Data.Word
import Data.Int
import Data.Bits
import Control.Applicative
import GHC.Enum
import Cgm.Data.Bool
import Cgm.Data.Super
import Cgm.Data.Nat
import Cgm.Control.Combinators
import Cgm.Control.InFunctor
import Test.QuickCheck (Arbitrary(..), Gen)
import Data.Typeable
class (Bits w, Integral w, Nat (WordNBits w)) => WordN w where
type WordNBits w :: *
instance WordN Word8 where type WordNBits Word8 = D8
instance WordN Word16 where type WordNBits Word16 = D16
instance WordN Word32 where type WordNBits Word32 = D32
instance WordN Word64 where type WordNBits Word64 = D64
wordNBits :: forall w. WordN w => w -> Int
wordNBits _ = (at :: At (WordNBits w)) intOfNat
newtype RWord w n = RWord {unRWord :: w} deriving Typeable
toRWord :: WordN w => w -> RWord w (WordNBits w)
toRWord = RWord
fromRWord :: RWord w n -> w
fromRWord = unRWord
rWord :: WordN w => Bijection' w (RWord w (WordNBits w))
rWord = uncheckedBijection toRWord fromRWord
boolAsWord :: Bijection' Bool (RWord Word8 D1)
boolAsWord = uncheckedBijection (bool 0 1) (== 1)
class (WordN w, Nat n, Nat (WordNBits w :-: n)) => RWordC w n
instance (WordN w, Nat n, Nat (WordNBits w :-: n)) => RWordC w n
rWordJoin :: forall n m w. (Nat n, Nat m, Bits w) => RWord w n -> RWord w m -> Tagged n (RWord w (m :+: n))
rWordJoin (RWord un) (RWord um) = Tagged $ RWord $ um .|. (un `shiftL` (at :: At m) intOfNat)
rWordBool :: RWordC w D1 => RWord w D1 -> Bool
rWordBool = (`testBit` 0)
rWordSplit :: forall w n m. (RWordC w (n :+: m), RWordC w n, RWordC w m) => RWord w (n :+: m) -> Tagged m (RWord w m, RWord w n)
rWordSplit (RWord w) = Tagged $ (RWord (w `shiftR` (at :: At m) intOfNat), rClean $ RWord w)
rClean :: forall w n. RWordC w n => RWord w n -> RWord w n
rClean = liftRToR $ (.&.) $ (at :: At n) $ lowMaskNat
rSaturate :: forall w n. RWordC w n => RWord w n -> RWord w n
rSaturate = liftRToR $ (.|.) $ complement $ (at :: At n) $ lowMaskNat
lowMaskNat :: RWordC w n => Tagged n w
lowMaskNat = (complement . shiftL (complement 0)) <$> intOfNat
liftRToA f = f . unRWord
liftAToR f = RWord . f
liftRToR f = RWord . f . unRWord
liftRRToR f = RWord ./ dot2i f unRWord
liftRRToA f = dot2i f unRWord
liftRAToR f = RWord ./ dot2 f unRWord id
liftRRToRR f = (\(a, b) -> (RWord a, RWord b)) ./ dot2i f unRWord
instance (RWordC w n, RWordC w' n) => Super (RWord w n) w' where
super = uncheckedInjectionM fromIntegral (((RWord . fromIntegral) <$>) . predJust (<= bound)) where
bound = fromIntegral (maxBound :: RWord w n) :: w'
rChangeWord :: forall w w' n . (RWordC w n, RWordC w' n) => Bijection' (RWord w n) (RWord w' n)
rChangeWord = uncheckedBijection (RWord . fromIntegral . unRWord) (RWord . fromIntegral . unRWord)
rChangeWord' :: forall w w' n . (RWordC w n, WordN w', Nat (WordNBits w' :-: WordNBits w)) => Bijection' (RWord w n) (RWord w' n)
rChangeWord' = uncheckedBijection (RWord . fromIntegral . unRWord) (RWord . fromIntegral . unRWord)
rMoreBits :: forall w n n' d . (RWordC w n, Nat d, (n' :-: n) ~ d) => InjectionM' (RWord w n) (RWord w n')
rMoreBits = uncheckedInjectionM (liftRToR id) ((RWord <$>) . predJust (<= (at :: At n) lowMaskNat) . unRWord)
rAdd :: Num w => RWord w n -> RWord w n -> RWord w (Succ n)
rAdd = liftRRToR (+)
instance RWordC w n => Bounded (RWord w n) where
minBound = 0
maxBound = (at :: At n) $ dupTag $ subI $ lowMaskNat
instance RWordC w n => Bits (RWord w n) where
(.&.) = liftRRToR (.&.)
(.|.) = liftRRToR (.|.)
xor = liftRRToR xor
complement = liftRToR (`xor` (at :: At n) lowMaskNat)
shiftL = rClean ./ liftRAToR shiftL
shiftR = liftRAToR shiftR
rotateL x i = shiftL x i .|. shiftR x ((at :: At n) intOfNat i)
rotateR x i = rotateL x ((at :: At n) intOfNat i)
bitSize _ = (at :: At n) intOfNat
isSigned _ = False
instance RWordC w n => Ord (RWord w n) where
compare = liftRRToA compare
instance RWordC w n => Enum (RWord w n) where
succ = rClean . liftRToR succ . rSaturate
pred = liftRToR pred
toEnum = rClean . liftAToR toEnum . ((+) $ fromIntegral $ complement $ ((at :: At n) lowMaskNat :: w))
fromEnum = liftRToA fromEnum
enumFrom = boundedEnumFrom
enumFromThen = boundedEnumFromThen
instance RWordC w n => Real (RWord w n) where
toRational = liftRToA toRational
instance RWordC w n => Integral (RWord w n) where
quot = liftRRToR quot
rem = liftRRToR rem
div = liftRRToR div
mod = liftRRToR mod
quotRem = liftRRToRR quotRem
divMod = liftRRToRR divMod
toInteger = liftRToA toInteger
instance RWordC w n => WordN (RWord w n) where
type WordNBits (RWord w n) = n
instance RWordC w n => Eq (RWord w n) where
(==) = liftRRToA (==)
instance (Show w, RWordC w n) => Show (RWord w n) where
show = liftRToA show
instance RWordC w n => Num (RWord w n) where
(+) = rClean ./ liftRRToR (+)
() = rClean ./ liftRRToR ()
(*) = rClean ./ liftRRToR (*)
negate = rClean . liftRToR negate
fromInteger = rClean . liftAToR fromInteger
abs = liftRToR abs
signum = liftRToR signum
instance (Arbitrary w, RWordC w n) => Arbitrary (RWord w n) where
arbitrary = (rClean . RWord) <$> arbitrary
shrink = (RWord <$>) . shrink . unRWord
type RWord8 = RWord Word8
type RWord16 = RWord Word16
type RWord32 = RWord Word32
type RWord64 = RWord Word64