    {-|
    Copyright  :  (C) 2013-2016, University of Twente
                      2020,      Myrtle Software Ltd
                      2024,      QBayLogic B.V.
    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 (+))

    import Clash.Sized.Internal (formatRange)

    -- | 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 (a :: Nat) (b :: Nat).
    (KnownNat a, KnownNat b) =>
    f a -> f b
    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 (a :: Nat) (b :: Nat).
    (KnownNat a, KnownNat b) =>
    f a -> f b
    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 :: forall a b.
    (HasCallStack, Integral a, Integral b, Bounded b) =>
    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 (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 (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 -> Integer -> [Char]
    forall a. (Ord a, Show a) => a -> a -> [Char]
    formatRange (b -> Integer
    forall a. Integral a => a -> Integer
    toInteger (forall a. Bounded a => a
    minBound @b)) (b -> Integer
    forall a. Integral a => a -> Integer
    toInteger (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 :: forall a b.
    (HasCallStack, Integral a, Integral b, Bounded b) =>
    a -> b
    checkedFromIntegral a
    v =
      Proxy b -> a -> ()
    forall a b.
    (HasCallStack, Integral a, Integral b, Bounded b) =>
    Proxy b -> a -> ()
    checkIntegral (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b) a
    v () -> b -> b
    forall a b. a -> 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.
    --
    -- __NB__: 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 :: forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
    (HasCallStack, Resize f, KnownNat a, Integral (f a), KnownNat b,
     Integral (f b), Bounded (f b)) =>
    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 (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @(f b)) f a
    v () -> f b -> f b
    forall a b. a -> b -> b
    `seq` f a -> f b
    forall (a :: Nat) (b :: Nat).
    (KnownNat a, KnownNat b) =>
    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.
    --
    -- __NB__: 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 :: forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
    (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)
    v =
      Proxy (f a) -> f (a + b) -> ()
    forall a b.
    (HasCallStack, Integral a, Integral b, Bounded b) =>
    Proxy b -> a -> ()
    checkIntegral (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @(f a)) f (a + b)
    v () -> f a -> f a
    forall a b. a -> b -> b
    `seq` f (a + b) -> f a
    forall (a :: Nat) (b :: Nat). KnownNat a => 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