-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.Word4
-- Author    : Brian Huffman
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates how new sizes of word/int types can be defined and
-- used with SBV.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Documentation.SBV.Examples.Misc.Word4 where

import GHC.Enum (boundedEnumFrom, boundedEnumFromThen, toEnumError, succError, predError)

import Data.Bits
import Data.Generics (Data, Typeable)
import System.Random (Random(..))

import Data.SBV
import Data.SBV.Internals

-- | Word4 as a newtype. Invariant: @Word4 x@ should satisfy @x < 16@.
newtype Word4 = Word4 Word8
  deriving (Eq, Ord, Data, Typeable)

-- | Smart constructor; simplifies conversion from Word8
word4 :: Word8 -> Word4
word4 x = Word4 (x .&. 0x0f)

-- | Show instance
instance Show Word4 where
  show (Word4 x) = show x

-- | Read instance. We read as an 8-bit word, and coerce
instance Read Word4 where
  readsPrec p s = [ (word4 x, s') | (x, s') <- readsPrec p s ]

-- | Bounded instance; from 0 to 255
instance Bounded Word4 where
  minBound = Word4 0x00
  maxBound = Word4 0x0f

-- | Enum instance, trivial definitions.
instance Enum Word4 where
  succ (Word4 x) = if x < 0x0f then Word4 (succ x) else succError "Word4"
  pred (Word4 x) = if x > 0x00 then Word4 (pred x) else predError "Word4"
  toEnum i | 0x00 <= i && i <= 0x0f = Word4 (toEnum i)
           | otherwise              = toEnumError "Word4" i (Word4 0x00, Word4 0x0f)
  fromEnum (Word4 x) = fromEnum x
  -- Comprehensions
  enumFrom                                     = boundedEnumFrom
  enumFromThen                                 = boundedEnumFromThen
  enumFromTo     (Word4 x) (Word4 y)           = map Word4 (enumFromTo x y)
  enumFromThenTo (Word4 x) (Word4 y) (Word4 z) = map Word4 (enumFromThenTo x y z)

-- | Num instance, merely lifts underlying 8-bit operation and casts back
instance Num Word4 where
  Word4 x + Word4 y = word4 (x + y)
  Word4 x * Word4 y = word4 (x * y)
  Word4 x - Word4 y = word4 (x - y)
  negate (Word4 x)  = word4 (negate x)
  abs (Word4 x)     = Word4 x
  signum (Word4 x)  = Word4 (if x == 0 then 0 else 1)
  fromInteger n     = word4 (fromInteger n)

-- | Real instance simply uses the Word8 instance
instance Real Word4 where
  toRational (Word4 x) = toRational x

-- | Integral instance, again using Word8 instance and casting. NB. we do
-- not need to use the smart constructor here as neither the quotient nor
-- the remainder can overflow a Word4.
instance Integral Word4 where
  quotRem (Word4 x) (Word4 y) = (Word4 q, Word4 r)
    where (q, r) = quotRem x y
  toInteger (Word4 x) = toInteger x

-- | Bits instance
instance Bits Word4 where
  Word4 x  .&.  Word4 y = Word4 (x  .&.  y)
  Word4 x  .|.  Word4 y = Word4 (x  .|.  y)
  Word4 x `xor` Word4 y = Word4 (x `xor` y)
  complement (Word4 x)  = Word4 (x `xor` 0x0f)
  Word4 x `shift`  i    = word4 (shift x i)
  Word4 x `shiftL` i    = word4 (shiftL x i)
  Word4 x `shiftR` i    = Word4 (shiftR x i)
  Word4 x `rotate` i    = word4 (x `shiftL` k .|. x `shiftR` (4-k))
                            where k = i .&. 3
  bitSize _             = 4
  bitSizeMaybe _        = Just 4
  isSigned _            = False
  testBit (Word4 x)     = testBit x
  bit i                 = word4 (bit i)
  popCount (Word4 x)    = popCount x

-- | Random instance, used in quick-check
instance Random Word4 where
  randomR (Word4 lo, Word4 hi) gen = (Word4 x, gen')
    where (x, gen') = randomR (lo, hi) gen
  random gen = (Word4 x, gen')
    where (x, gen') = randomR (0x00, 0x0f) gen

-- | SWord4 type synonym
type SWord4 = SBV Word4

-- | SymVal instance, allowing this type to be used in proofs/sat etc.
instance SymVal Word4 where
  mkSymVal = genMkSymVar (KBounded False 4)
  literal  = genLiteral  (KBounded False 4)
  fromCV   = genFromCV

-- | HasKind instance; simply returning the underlying kind for the type
instance HasKind Word4 where
  kindOf _ = KBounded False 4

-- | SatModel instance, merely uses the generic parsing method.
instance SatModel Word4 where
  parseCVs = genParse (KBounded False 4)

-- | SDvisible instance, using 0-extension
instance SDivisible Word4 where
  sQuotRem x 0 = (0, x)
  sQuotRem x y = x `quotRem` y
  sDivMod  x 0 = (0, x)
  sDivMod  x y = x `divMod` y

-- | SDvisible instance, using default methods
instance SDivisible SWord4 where
  sQuotRem = liftQRem
  sDivMod  = liftDMod

-- | SIntegral instance, using default methods
instance SIntegral Word4

-- | Joining/splitting to/from Word8
instance Splittable Word8 Word4 where
  split x           = (Word4 (x `shiftR` 4), word4 x)
  Word4 x # Word4 y = (x `shiftL` 4) .|. y
  extend (Word4 x)  = x