{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

--
-- Bits.hs --- Bit-sized unsigned integer types.
--
-- Copyright (C) 2013, Galois, Inc.
-- All Rights Reserved.
--

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

----------------------------------------------------------------------
-- Bit Representations

-- | Type function: "BitRep (n :: Nat)" returns an Ivory type given a
-- bit size as a type-level natural.  Instances of this type family
-- for bits [1..64] are generated using Template Haskell.
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]

-- | Set of constraints we require on a bit representation type.
type IvoryRep a = (IvoryBits a, IvoryOrd a, IvoryInit a,
                   IvoryStore a, IvoryType a, IvoryZeroVal a)

----------------------------------------------------------------------
-- Bit Data Type

-- | A wrapper for an Ivory type that can hold an "n" bit unsigned
-- integer.
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)

-- | "Bit" is a type alias for "Bits 1".
type Bit = Bits 1

-- | Type function to extract the "n" from a "Bits n" type.
type family BitSize a :: Nat
type instance BitSize (Bits n) = n

-- | Convert a Haskell integer to a bit data value without bounds
-- checking.  This must not be exported, but is used by the
-- quasiquoter when the values are constant at compile-time and
-- already bounds checked.
unsafeIntToBits :: (IvoryRep (BitRep n), Integral a) => a -> Bits n
unsafeIntToBits = Bits . fromIntegral

-- | Return a bit value of all zeros of the given size.
zeroBits :: (IvoryRep (BitRep n)) => Bits n
zeroBits = Bits 0

-- XXX do not export, used when unwrapping/rewrapping values when
-- setting fields and the size has obviously not changed.
unsafeRepToBits :: BitRep n -> Bits n
unsafeRepToBits = Bits

-- | Convert an Ivory value to a bit value.  If the input value
-- contains out of range bits, they will be ignored.
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)

-- | Convert a bit value to an Ivory value.
bitsToRep :: Bits n -> BitRep n
bitsToRep = unBits