{-|
Copyright  :  (C) 2013-2016, University of Twente
                  2020,      Myrtle Software Ltd
License    :  BSD2 (see the file LICENSE)
Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>
-}

{-# LANGUAGE NoGeneralizedNewtypeDeriving #-}

{-# LANGUAGE Safe #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_HADDOCK show-extensions #-}

module Clash.Class.Resize
 ( Resize(..)

 -- * Resize helpers
 , checkedResize
 , checkedFromIntegral
 , checkedTruncateB
 ) where

import Data.Kind (Type)
import Data.Proxy (Proxy(Proxy))
import GHC.Stack (HasCallStack)
import GHC.TypeLits (Nat, KnownNat, type (+))

-- | Coerce a value to be represented by a different number of bits
class Resize (f :: Nat -> Type) where
  -- | A sign-preserving resize operation
  --
  -- * For signed datatypes: Increasing the size of the number replicates the
  -- sign bit to the left. Truncating a number to length L keeps the sign bit
  -- and the rightmost L-1 bits.
  --
  -- * For unsigned datatypes: Increasing the size of the number extends with
  -- zeros to the left. Truncating a number of length N to a length L just
  -- removes the left (most significant) N-L bits.
  resize :: (KnownNat a, KnownNat b) => f a -> f b
  -- | Perform a 'zeroExtend' for unsigned datatypes, and 'signExtend' for a
  -- signed datatypes
  extend :: (KnownNat a, KnownNat b) => f a -> f (b + a)
  extend = f a -> f (b + a)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize
  -- | Add extra zero bits in front of the MSB
  zeroExtend :: (KnownNat a, KnownNat b) => f a -> f (b + a)
  -- | Add extra sign bits in front of the MSB
  signExtend :: (KnownNat a, KnownNat b) => f a -> f (b + a)
  signExtend = f a -> f (b + a)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize
  -- | Remove bits from the MSB
  truncateB :: KnownNat a => f (a + b) -> f a

-- | Helper function of 'checkedFromIntegral', 'checkedResize' and 'checkedTruncateB'
checkIntegral ::
  forall a b.
  HasCallStack =>
  (Integral a, Integral b, Bounded b) =>
  Proxy b ->
  a -> ()
checkIntegral :: Proxy b -> a -> ()
checkIntegral Proxy b
Proxy a
v =
  if a -> Integer
forall a. Integral a => a -> Integer
toInteger a
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> b -> Integer
forall a. Integral a => a -> Integer
toInteger (Bounded b => b
forall a. Bounded a => a
maxBound @b)
  Bool -> Bool -> Bool
|| a -> Integer
forall a. Integral a => a -> Integer
toInteger a
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< b -> Integer
forall a. Integral a => a -> Integer
toInteger (Bounded b => b
forall a. Bounded a => a
minBound @b) then
    [Char] -> ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> ()) -> [Char] -> ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Given integral " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Integer -> [Char]
forall a. Show a => a -> [Char]
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
v) [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" is out of bounds for" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<>
            [Char]
" target type. Bounds of target type are: [" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<>
            Integer -> [Char]
forall a. Show a => a -> [Char]
show (b -> Integer
forall a. Integral a => a -> Integer
toInteger (Bounded b => b
forall a. Bounded a => a
minBound @b)) [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
".." [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<>
            Integer -> [Char]
forall a. Show a => a -> [Char]
show (b -> Integer
forall a. Integral a => a -> Integer
toInteger (Bounded b => b
forall a. Bounded a => a
maxBound @b)) [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"]."
  else
    ()

-- | Like 'fromIntegral', but errors if /a/ is out of bounds for /b/. Useful when
-- you "know" /a/ can't be out of bounds, but would like to have your assumptions
-- checked.
--
-- * __NB__: Check only affects simulation. I.e., no checks will be inserted
-- into the generated HDL
-- * __NB__: 'fromIntegral' is not well suited for Clash as it will go through
-- 'Integer' which is arbitrarily bounded in HDL. Instead use
-- 'Clash.Class.BitPack.bitCoerce' and the 'Resize' class.
checkedFromIntegral ::
  forall a b.
  HasCallStack =>
  (Integral a, Integral b, Bounded b) =>
  a -> b
checkedFromIntegral :: a -> b
checkedFromIntegral a
v =
  Proxy b -> a -> ()
forall a b.
(HasCallStack, Integral a, Integral b, Bounded b) =>
Proxy b -> a -> ()
checkIntegral (Proxy b
forall k (t :: k). Proxy t
Proxy @b) a
v () -> b -> b
`seq` a -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
v

-- | Like 'resize', but errors if /f a/ is out of bounds for /f b/. Useful when
-- you "know" /f a/ can't be out of bounds, but would like to have your
-- assumptions checked.
--
-- __N.B.__: Check only affects simulation. I.e., no checks will be inserted
-- into the generated HDL
checkedResize ::
  forall a b f.
  ( HasCallStack
  , Resize f
  , KnownNat a, Integral (f a)
  , KnownNat b, Integral (f b), Bounded (f b) ) =>
  f a -> f b
checkedResize :: f a -> f b
checkedResize f a
v =
  Proxy (f b) -> f a -> ()
forall a b.
(HasCallStack, Integral a, Integral b, Bounded b) =>
Proxy b -> a -> ()
checkIntegral (Proxy (f b)
forall k (t :: k). Proxy t
Proxy @(f b)) f a
v () -> f b -> f b
`seq` f a -> f b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize f a
v

-- | Like 'truncateB', but errors if /f (a + b)/ is out of bounds for /f a/. Useful
-- when you "know" /f (a + b)/ can't be out of bounds, but would like to have your
-- assumptions checked.
--
-- __N.B.__: Check only affects simulation. I.e., no checks will be inserted
-- into the generated HDL
checkedTruncateB ::
  forall a b f.
  ( HasCallStack
  , Resize f
  , KnownNat b, Integral (f (a + b))
  , KnownNat a, Integral (f a), Bounded (f a) ) =>
  f (a + b) -> f a
checkedTruncateB :: f (a + b) -> f a
checkedTruncateB f (a + b)
v =
  Proxy (f a) -> f (a + b) -> ()
forall a b.
(HasCallStack, Integral a, Integral b, Bounded b) =>
Proxy b -> a -> ()
checkIntegral (Proxy (f a)
forall k (t :: k). Proxy t
Proxy @(f a)) f (a + b)
v () -> f a -> f a
`seq` f (a + b) -> f a
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a) =>
f (a + b) -> f a
truncateB f (a + b)
v