{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Extra.Solver #-}
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}
{-# OPTIONS_HADDOCK hide #-}

{- |
Copyright  :  (C) 2025     , Martijn Bastiaan
                  2025-2026, QBayLogic B.V.
License    :  BSD2 (see the file LICENSE)
Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>
-}
module Clash.Class.NumConvert.Internal.MaybeNumConvert where

import Clash.Class.BitPack
import Clash.Class.NumConvert.Internal.NumConvert (NumConvertCanonical (..))
import Clash.Class.NumConvert.Internal.Canonical (Canonical)
import Clash.Class.Resize
import Clash.Promoted.Nat
import Clash.Sized.BitVector
import Clash.Sized.Index
import Clash.Sized.Signed
import Clash.Sized.Unsigned

import GHC.TypeLits (KnownNat, type (+), type (^))
import GHC.TypeLits.Extra (CLogWZ)

{- $setup
>>> import Clash.Prelude
>>> import Clash.Class.NumConvert
>>> import Data.Word
>>> import Data.Int
-}

{- | Internal class for concrete conversions that may fail. This class is used
internally by 'MaybeNumConvert' and should not be used directly. Use
'MaybeNumConvert' instead.
-}
class MaybeNumConvertCanonical a b where
  maybeNumConvertCanonical :: a -> Maybe b

{- | Conversions that may fail for some values. A successful conversion retains
the numerical value interpretation of the source type in the target type. A
failure is expressed by returning 'Nothing', never by an 'Clash.XException.XException'.

== __Laws__
A conversion is either successful or it fails gracefully. I.e., it does not
produce errors (also see "Clash.XException"). I.e.,

> x == fromMaybe x (maybeNumConvert @a @b x >>= maybeNumConvert @b @a)

for all values @x@ of type @a@. It should also preserve the numerical value
interpretation of the bits. For types that have an @Integral@ instance, this
intuition is captured by:

> toInteger x == fromMaybe (toInteger x) (toInteger <$> maybeNumConvert @a @b x)

If a conversion succeeds one way, it should also succeed the other way. I.e.,

> isJust (maybeNumConvert @a @b x) `implies` isJust (maybeNumConvert @a @b x >>= maybeNumConvert @b @a)

A conversion should succeed if and only if the value is representable in the
target type. For types that have a @Bounded@ and @Integral@ instance, this
intuition is captured by:

> isJust (maybeNumConvert @a @b x) == (i x >= i (minBound @b) && i x <= i (maxBound @b))

where @i = toInteger@.

All implementations should be total, i.e., they should not produce \"bottoms\".

Additionally, any implementation should be translatable to synthesizable HDL.
-}
type MaybeNumConvert a b =
  ( NumConvertCanonical a (Canonical a)
  , MaybeNumConvertCanonical (Canonical a) (Canonical b)
  , NumConvertCanonical (Canonical b) b
  )

{- | Convert a supplied value of type @a@ to a value of type @b@. If the value
cannot be represented in the target type, 'Nothing' is returned.

>>> maybeNumConvert (1 :: Index 8) :: Maybe (Unsigned 2)
Just 1
>>> maybeNumConvert (7 :: Index 8) :: Maybe (Unsigned 2)
Nothing

For the time being, if the input is an 'Clash.XException.XException', then
the output is too. This property might be relaxed in the future.
-}
maybeNumConvert :: forall a b. MaybeNumConvert a b => a -> Maybe b
maybeNumConvert :: forall a b. MaybeNumConvert a b => a -> Maybe b
maybeNumConvert a
a =
    (Canonical b -> b) -> Maybe (Canonical b) -> Maybe b
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. NumConvertCanonical a b => a -> b
numConvertCanonical @(Canonical b) @b)
  (Maybe (Canonical b) -> Maybe b) -> Maybe (Canonical b) -> Maybe b
forall a b. (a -> b) -> a -> b
$ forall a b. MaybeNumConvertCanonical a b => a -> Maybe b
maybeNumConvertCanonical @(Canonical a) @(Canonical b)
  (Canonical a -> Maybe (Canonical b))
-> Canonical a -> Maybe (Canonical b)
forall a b. (a -> b) -> a -> b
$ forall a b. NumConvertCanonical a b => a -> b
numConvertCanonical @a @(Canonical a) a
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Index n) (Index m) where
  maybeNumConvertCanonical :: Index n -> Maybe (Index m)
maybeNumConvertCanonical !Index n
a = case forall (n :: Nat). KnownNat n => Integer
natToInteger @m of
    Integer
0 -> Maybe (Index m)
forall a. Maybe a
Nothing
    Integer
_ -> Index n -> Maybe (Index m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize Index n
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Index n) (Unsigned m) where
  maybeNumConvertCanonical :: Index n -> Maybe (Unsigned m)
maybeNumConvertCanonical !Index n
a = Unsigned (CLogWZ 2 n 0) -> Maybe (Unsigned m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize (Unsigned (CLogWZ 2 n 0) -> Maybe (Unsigned m))
-> Unsigned (CLogWZ 2 n 0) -> Maybe (Unsigned m)
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Unsigned (CLogWZ 2 n 0)) Index n
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Index n) (Signed m) where
  maybeNumConvertCanonical :: Index n -> Maybe (Signed m)
maybeNumConvertCanonical !Index n
a = Unsigned (CLogWZ 2 n 0) -> Maybe (Signed m)
forall a b. MaybeNumConvertCanonical a b => a -> Maybe b
maybeNumConvertCanonical (Unsigned (CLogWZ 2 n 0) -> Maybe (Signed m))
-> Unsigned (CLogWZ 2 n 0) -> Maybe (Signed m)
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Unsigned (CLogWZ 2 n 0)) Index n
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Index n) (BitVector m) where
  maybeNumConvertCanonical :: Index n -> Maybe (BitVector m)
maybeNumConvertCanonical !Index n
a = BitVector (CLogWZ 2 n 0) -> Maybe (BitVector m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize (BitVector (CLogWZ 2 n 0) -> Maybe (BitVector m))
-> BitVector (CLogWZ 2 n 0) -> Maybe (BitVector m)
forall a b. (a -> b) -> a -> b
$ Index n -> BitVector (BitSize (Index n))
forall a. BitPack a => a -> BitVector (BitSize a)
pack Index n
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Unsigned n) (Index m) where
  maybeNumConvertCanonical :: Unsigned n -> Maybe (Index m)
maybeNumConvertCanonical !Unsigned n
a = case forall (n :: Nat). KnownNat n => Integer
natToInteger @m of
    Integer
0 -> Maybe (Index m)
forall a. Maybe a
Nothing
    Integer
_ -> Index (2 ^ n) -> Maybe (Index m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize (Index (2 ^ n) -> Maybe (Index m))
-> Index (2 ^ n) -> Maybe (Index m)
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Index (2 ^ n)) Unsigned n
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Unsigned n) (Unsigned m) where
  maybeNumConvertCanonical :: Unsigned n -> Maybe (Unsigned m)
maybeNumConvertCanonical !Unsigned n
a = Unsigned n -> Maybe (Unsigned m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize Unsigned n
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Unsigned n) (Signed m) where
  maybeNumConvertCanonical :: Unsigned n -> Maybe (Signed m)
maybeNumConvertCanonical !Unsigned n
a = Signed (n + 1) -> Maybe (Signed m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize (Signed (n + 1) -> Maybe (Signed m))
-> Signed (n + 1) -> Maybe (Signed m)
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Unsigned (n + 1)) (Unsigned (n + 1) -> Signed (n + 1))
-> Unsigned (n + 1) -> Signed (n + 1)
forall a b. (a -> b) -> a -> b
$ Unsigned n -> Unsigned (1 + n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Unsigned a -> Unsigned (b + a)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
extend Unsigned n
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Unsigned n) (BitVector m) where
  maybeNumConvertCanonical :: Unsigned n -> Maybe (BitVector m)
maybeNumConvertCanonical !Unsigned n
a = BitVector n -> Maybe (BitVector m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize (BitVector n -> Maybe (BitVector m))
-> BitVector n -> Maybe (BitVector m)
forall a b. (a -> b) -> a -> b
$ Unsigned n -> BitVector (BitSize (Unsigned n))
forall a. BitPack a => a -> BitVector (BitSize a)
pack Unsigned n
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Signed n) (Index m) where
  maybeNumConvertCanonical :: Signed n -> Maybe (Index m)
maybeNumConvertCanonical Signed n
n = case forall (n :: Nat). KnownNat n => Integer
natToInteger @m of
    Integer
0 -> Maybe (Index m)
forall a. Maybe a
Nothing
    Integer
_ | Signed n
n Signed n -> Signed n -> Bool
forall a. Ord a => a -> a -> Bool
< Signed n
0 -> Maybe (Index m)
forall a. Maybe a
Nothing
      | Bool
otherwise -> Index (2 ^ n) -> Maybe (Index m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize (forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Index (2 ^ n)) (Signed n -> Signed (CLogWZ 2 (2 ^ n) 0)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Signed a -> Signed b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize Signed n
n))

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Signed n) (Unsigned m) where
  maybeNumConvertCanonical :: Signed n -> Maybe (Unsigned m)
maybeNumConvertCanonical Signed n
n
    | Signed n
n Signed n -> Signed n -> Bool
forall a. Ord a => a -> a -> Bool
< Signed n
0 = Maybe (Unsigned m)
forall a. Maybe a
Nothing
    | Bool
otherwise = Unsigned (n + 1) -> Maybe (Unsigned m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize (forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Signed (n + 1)) (Signed n -> Signed (1 + n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Signed a -> Signed (b + a)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
extend Signed n
n))

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Signed n) (Signed m) where
  maybeNumConvertCanonical :: Signed n -> Maybe (Signed m)
maybeNumConvertCanonical !Signed n
a = Signed n -> Maybe (Signed m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize Signed n
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (Signed n) (BitVector m) where
  maybeNumConvertCanonical :: Signed n -> Maybe (BitVector m)
maybeNumConvertCanonical Signed n
n
    | Signed n
n Signed n -> Signed n -> Bool
forall a. Ord a => a -> a -> Bool
< Signed n
0 = Maybe (BitVector m)
forall a. Maybe a
Nothing
    | Bool
otherwise = BitVector (n + 1) -> Maybe (BitVector m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize (forall a. BitPack a => a -> BitVector (BitSize a)
pack @(Signed (n + 1)) (Signed n -> Signed (1 + n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Signed a -> Signed (b + a)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
extend Signed n
n))

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (BitVector n) (Index m) where
  maybeNumConvertCanonical :: BitVector n -> Maybe (Index m)
maybeNumConvertCanonical !BitVector n
a = case forall (n :: Nat). KnownNat n => Integer
natToInteger @m of
    Integer
0 -> Maybe (Index m)
forall a. Maybe a
Nothing
    Integer
_ -> Index (2 ^ n) -> Maybe (Index m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize (Index (2 ^ n) -> Maybe (Index m))
-> Index (2 ^ n) -> Maybe (Index m)
forall a b. (a -> b) -> a -> b
$ forall a. BitPack a => BitVector (BitSize a) -> a
unpack @(Index (2 ^ n)) BitVector n
BitVector (BitSize (Index (2 ^ n)))
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (BitVector n) (Unsigned m) where
  maybeNumConvertCanonical :: BitVector n -> Maybe (Unsigned m)
maybeNumConvertCanonical !BitVector n
a = Unsigned n -> Maybe (Unsigned m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize (Unsigned n -> Maybe (Unsigned m))
-> Unsigned n -> Maybe (Unsigned m)
forall a b. (a -> b) -> a -> b
$ forall a. BitPack a => BitVector (BitSize a) -> a
unpack @(Unsigned n) BitVector n
BitVector (BitSize (Unsigned n))
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (BitVector n) (Signed m) where
  maybeNumConvertCanonical :: BitVector n -> Maybe (Signed m)
maybeNumConvertCanonical !BitVector n
a = Signed (n + 1) -> Maybe (Signed m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize (Signed (n + 1) -> Maybe (Signed m))
-> Signed (n + 1) -> Maybe (Signed m)
forall a b. (a -> b) -> a -> b
$ forall a. BitPack a => BitVector (BitSize a) -> a
unpack @(Signed (n + 1)) (BitVector (BitSize (Signed (n + 1))) -> Signed (n + 1))
-> BitVector (BitSize (Signed (n + 1))) -> Signed (n + 1)
forall a b. (a -> b) -> a -> b
$ BitVector n -> BitVector (1 + n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
BitVector a -> BitVector (b + a)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
extend BitVector n
a

instance (KnownNat n, KnownNat m) => MaybeNumConvertCanonical (BitVector n) (BitVector m) where
  maybeNumConvertCanonical :: BitVector n -> Maybe (BitVector m)
maybeNumConvertCanonical !BitVector n
a = BitVector n -> Maybe (BitVector m)
forall (a :: Nat) (b :: Nat) (f :: Nat -> Type).
(Resize f, KnownNat a, Integral (f a), KnownNat b, Integral (f b),
 Bounded (f b)) =>
f a -> Maybe (f b)
maybeResize BitVector n
a