{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Ivory.Language.BitData.Bits where
import GHC.TypeLits
import Ivory.Language.Uint
import Ivory.Language.Bits
import Ivory.Language.Init
import Ivory.Language.IBool
import Ivory.Language.Proxy
import Ivory.Language.Type
import Ivory.Language.Ref
import Ivory.Language.BitData.DefBitRep
type family BitRep (n :: Nat) :: *
defBitRep ''BitRep ''Uint8 [1..8]
defBitRep ''BitRep ''Uint16 [9..16]
defBitRep ''BitRep ''Uint32 [17..32]
defBitRep ''BitRep ''Uint64 [33..64]
type IvoryRep a = (IvoryBits a, IvoryOrd a, IvoryInit a,
IvoryStore a, IvoryType a, IvoryZeroVal a)
newtype Bits (n :: Nat) = Bits { unBits :: BitRep n }
deriving instance (IvoryRep (BitRep n)) => IvoryType (Bits n)
deriving instance (IvoryRep (BitRep n)) => IvoryVar (Bits n)
deriving instance (IvoryRep (BitRep n)) => IvoryExpr (Bits n)
deriving instance (IvoryRep (BitRep n)) => IvoryEq (Bits n)
deriving instance (IvoryRep (BitRep n)) => IvoryStore (Bits n)
deriving instance (IvoryRep (BitRep n)) => IvoryInit (Bits n)
deriving instance (IvoryRep (BitRep n)) => IvoryZeroVal (Bits n)
type Bit = Bits 1
type family BitSize a :: Nat
type instance BitSize (Bits n) = n
unsafeIntToBits :: (IvoryRep (BitRep n), Integral a) => a -> Bits n
unsafeIntToBits = Bits . fromIntegral
zeroBits :: (IvoryRep (BitRep n)) => Bits n
zeroBits = Bits 0
unsafeRepToBits :: BitRep n -> Bits n
unsafeRepToBits = Bits
repToBits :: forall n. (ANat n, IvoryRep (BitRep n))
=> BitRep n -> Bits n
repToBits x = Bits (x .& mask)
where mask = fromIntegral (2 ^ fromTypeNat (aNat :: NatType n) - 1 :: Integer)
bitsToRep :: Bits n -> BitRep n
bitsToRep = unBits