{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
--
-- BitData.hs --- Typed bit data types.
--
-- Copyright (C) 2013, Galois, Inc.
-- All Rights Reserved.
--

module Ivory.Language.BitData.BitData where

import Ivory.Language.Bits
import Ivory.Language.Proxy
import Ivory.Language.Cast
import Ivory.Language.IBool

import Ivory.Language.BitData.Bits

-- | Class of bit data types defined by the "bitdata" quasiquoter.
class (ANat (BitSize (BitType a)),
       IvoryRep (BitDataRep a),
       BitType a ~ Bits (BitSize (BitType a))) => BitData a where
  -- | Return the base "(Bits n)" type as defined in the "bitdata"
  -- quasiquoter.
  type BitType a :: *

  -- | Convert a bit data type to its raw bit value.  This is always
  -- well defined and should be exported.
  toBits :: a -> BitType a

  -- | Convert a raw bit value to a bit data type.  All values may not
  -- be well defined with respect to the original set of bit data
  -- constructors.  For now, we allow these "junk" values to be
  -- created, but that may change in the future (perhaps by
  -- implementing a checked, Ivory run-time conversion).
  fromBits :: BitType a -> a

-- | The Ivory type that stores the actual value for a bit data type.
--
-- This is a shorthand to simplify the constraints on functions that
-- take arguments of the "BitData" class.
type BitDataRep a = BitRep (BitSize (BitType a))

-- | Convert a raw Ivory type to a bit data type.  If the input value
-- is too large, the out of range upper bits will be masked off.
fromRep :: BitData a => BitDataRep a -> a
fromRep = fromBits . repToBits

-- XXX do not export---used when unwrapping/rewrapping values when
-- setting fields and the size has obviously not changed.
unsafeFromRep :: BitData a => BitDataRep a -> a
unsafeFromRep = fromBits . unsafeRepToBits

-- | Convert a bit data value to its Ivory representation.
toRep :: BitData a => a -> BitDataRep a
toRep = unBits . toBits

-- | Identity instance of "BitData" for the base "Bits n" type.
instance (ANat n, IvoryRep (BitRep n)) => BitData (Bits n) where
  type BitType (Bits n) = Bits n
  toBits = id
  fromBits = id

-- | Description of a bit field defined by the "bitdata" quasiquoter.
-- Each field defined in the record syntax will generate a top-level
-- definition of "BitDataField".
--
-- XXX do not export. This constructor must remain unexported so that only
-- fields checked by the quasiquoter are created.
data BitDataField a b = BitDataField
  { bitDataFieldPos  :: Int
  , bitDataFieldLen  :: Int
  , bitDataFieldName :: String
  } deriving Show

-- | Bit data field composition.  (like Control.Category.>>>)
(#>) :: BitDataField a b -> BitDataField b c -> BitDataField a c
(BitDataField p1 _ n1) #> (BitDataField p2 l2 n2) = BitDataField pos len name
  where
    name = n1 ++ "." ++ n2
    pos = p1 + p2
    len = l2

-- | Extract a field from a bit data definition.  Returns the value as
-- the type defined on the right hand side of the field definition in
-- the "bitdata" quasiquoter.
getBitDataField :: (BitData a, BitData b,
                    BitCast (BitDataRep a) (BitDataRep b))
                => BitDataField a b -> a -> b
getBitDataField f x = unsafeFromRep (bitCast ((toRep x `iShiftR` pos) .& mask))
  where pos  = fromIntegral (bitDataFieldPos f)
        mask = fromIntegral ((2 ^ bitDataFieldLen f) - 1 :: Integer)

-- | Infix operator to read a bit data field.  (like Data.Lens.^.)
(#.) :: (BitData a, BitData b,
         BitCast (BitDataRep a) (BitDataRep b))
     => a -> BitDataField a b -> b
(#.) = flip getBitDataField

-- | Set a field from a bit data definition.
setBitDataField :: (BitData a, BitData b,
                    SafeCast (BitDataRep b) (BitDataRep a))
                => BitDataField a b -> a -> b -> a
setBitDataField f x y = unsafeFromRep ((toRep x .& mask) .| val)
  where val  = safeCast (toRep y) `iShiftL` pos
        pos  = fromIntegral (bitDataFieldPos f)
        fmax = fromIntegral ((2 ^ bitDataFieldLen f) - 1 :: Integer)
        mask = iComplement (fmax `iShiftL` pos)

-- | Set a single-bit field in a bit data value.
setBitDataBit :: BitData a => BitDataField a Bit -> a -> a
setBitDataBit f x = unsafeFromRep (toRep x .| (1 `iShiftL` pos))
  where pos = fromIntegral (bitDataFieldPos f)

-- | Clear a single-bit field in a bit data value.
clearBitDataBit :: BitData a => BitDataField a Bit -> a -> a
clearBitDataBit f x = unsafeFromRep (toRep x .& (iComplement (1 `iShiftL` pos)))
  where pos = fromIntegral (bitDataFieldPos f)

-- | Convert a single bit bitdata to an Ivory boolean.
bitToBool :: Bit -> IBool
bitToBool b = (toRep b ==? 0) ? (false, true)

-- | Convert an Ivory boolean to a single bit.
boolToBit :: IBool -> Bit
boolToBit b = b ? (fromRep 1, fromRep 0)