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

#include "MachDeps.h"

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

import Prelude

import Clash.Class.BitPack
import Clash.Class.Resize
import Clash.Sized.BitVector
import Clash.Sized.Index
import Clash.Sized.Signed
import Clash.Sized.Unsigned

import GHC.TypeLits (KnownNat, type (+), type (<=), type (^))
import GHC.TypeLits.Extra (CLog)

import Data.Int (Int16, Int32, Int64, Int8)
import Data.Word (Word16, Word32, Word64, Word8)

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

{- | Conversions that are, based on their types, guaranteed to succeed. A
successful conversion retains the numerical value interpretation of the source
type in the target type and does not produce errors.

== __Laws__
A conversion is successful if a round trip conversion is lossless. I.e.,

> Just x == maybeNumConvert (numConvert @a @b x)

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 == toInteger (numConvert @a @b x)

Instances should make sure their constraints are as \"tight\" as possible. I.e.,
if an instance's constraints cannot be satisfied, then for the same types
'Clash.Class.NumConvert.maybeNumConvert' should return 'Nothing' for one or more
values in the domain of the source type @a@:

> L.any isNothing (L.map (maybeNumConvert @a @b) [minBound ..])

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

Additionally, any implementation should be translatable to synthesizable HDL.
-}
class NumConvert a b where
  {- | Convert a supplied value of type @a@ to a value of type @b@. The conversion
    is guaranteed to succeed.

    >>> numConvert (3 :: Index 8) :: Unsigned 8
    3

    The following will fail with a type error, as we cannot prove that all values
    of @Index 8@ can be represented by an @Unsigned 2@:

    >>> numConvert (3 :: Index 8) :: Unsigned 2
    ...

    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.
  -}
  numConvert :: a -> b

instance (KnownNat n, KnownNat m, n <= m) => NumConvert (Index n) (Index m) where
  numConvert :: Index n -> Index m
numConvert = Index n -> Index m
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize

instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => NumConvert (Index n) (Unsigned m) where
  numConvert :: Index n -> Unsigned m
numConvert !Index n
a = Unsigned (CLog 2 n) -> Unsigned m
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Unsigned a -> Unsigned b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (Unsigned (CLog 2 n) -> Unsigned m)
-> Unsigned (CLog 2 n) -> Unsigned m
forall a b. (a -> b) -> a -> b
$ Index n -> Unsigned (CLog 2 n)
forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce Index n
a

{- | Note: Conversion from @Index 1@ to @Signed 0@ is lossless, but not within the
constraints of the instance.
-}
instance (KnownNat n, KnownNat m, 1 <= n, CLog 2 n + 1 <= m) => NumConvert (Index n) (Signed m) where
  numConvert :: Index n -> Signed m
numConvert !Index n
a = Unsigned (CLog 2 n) -> Signed m
forall a b. NumConvert a b => a -> b
numConvert (Unsigned (CLog 2 n) -> Signed m)
-> Unsigned (CLog 2 n) -> Signed m
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Unsigned (CLog 2 n)) Index n
a

instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => NumConvert (Index n) (BitVector m) where
  numConvert :: Index n -> BitVector m
numConvert !Index n
a = BitVector (CLog 2 n) -> BitVector m
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
BitVector a -> BitVector b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (BitVector (CLog 2 n) -> BitVector m)
-> BitVector (CLog 2 n) -> 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, 1 <= m, 2 ^ n <= m) => NumConvert (Unsigned n) (Index m) where
  numConvert :: Unsigned n -> Index m
numConvert !Unsigned n
a = Unsigned (CLog 2 m) -> Index m
forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce (Unsigned (CLog 2 m) -> Index m) -> Unsigned (CLog 2 m) -> Index m
forall a b. (a -> b) -> a -> b
$ Unsigned n -> Unsigned (CLog 2 m)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Unsigned a -> Unsigned b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize Unsigned n
a

instance (KnownNat n, KnownNat m, n <= m) => NumConvert (Unsigned n) (Unsigned m) where
  numConvert :: Unsigned n -> Unsigned m
numConvert = Unsigned n -> Unsigned m
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Unsigned a -> Unsigned b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize

{- | Note: Conversion from @Unsigned 0@ to @Signed 0@ is lossless, but not within the
constraints of the instance.
-}
instance (KnownNat n, KnownNat m, n + 1 <= m) => NumConvert (Unsigned n) (Signed m) where
  numConvert :: Unsigned n -> Signed m
numConvert !Unsigned n
a = Unsigned m -> Signed m
forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce (Unsigned m -> Signed m) -> Unsigned m -> Signed m
forall a b. (a -> b) -> a -> b
$ Unsigned n -> Unsigned m
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Unsigned a -> Unsigned b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize Unsigned n
a

instance (KnownNat n, KnownNat m, n <= m) => NumConvert (Unsigned n) (BitVector m) where
  numConvert :: Unsigned n -> BitVector m
numConvert !Unsigned n
a = BitVector n -> BitVector m
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
BitVector a -> BitVector b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (BitVector n -> BitVector m) -> BitVector n -> 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, n <= m) => NumConvert (Signed n) (Signed m) where
  numConvert :: Signed n -> Signed m
numConvert !Signed n
a = Signed n -> Signed m
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
a

instance (KnownNat n, KnownNat m, 1 <= m, 2 ^ n <= m) => NumConvert (BitVector n) (Index m) where
  numConvert :: BitVector n -> Index m
numConvert = BitVector (CLog 2 m) -> Index m
BitVector (BitSize (Index m)) -> Index m
forall a. BitPack a => BitVector (BitSize a) -> a
unpack (BitVector (CLog 2 m) -> Index m)
-> (BitVector n -> BitVector (CLog 2 m)) -> BitVector n -> Index m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector n -> BitVector (CLog 2 m)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
BitVector a -> BitVector b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize

instance (KnownNat n, KnownNat m, n <= m) => NumConvert (BitVector n) (Unsigned m) where
  numConvert :: BitVector n -> Unsigned m
numConvert = BitVector m -> Unsigned m
BitVector (BitSize (Unsigned m)) -> Unsigned m
forall a. BitPack a => BitVector (BitSize a) -> a
unpack (BitVector m -> Unsigned m)
-> (BitVector n -> BitVector m) -> BitVector n -> Unsigned m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector n -> BitVector m
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
BitVector a -> BitVector b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize

{- | Note: Conversion from @BitVector 0@ to @Signed 0@ is lossless, but not within the
constraints of the instance.
-}
instance (KnownNat n, KnownNat m, n + 1 <= m) => NumConvert (BitVector n) (Signed m) where
  numConvert :: BitVector n -> Signed m
numConvert = BitVector m -> Signed m
BitVector (BitSize (Signed m)) -> Signed m
forall a. BitPack a => BitVector (BitSize a) -> a
unpack (BitVector m -> Signed m)
-> (BitVector n -> BitVector m) -> BitVector n -> Signed m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector n -> BitVector m
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
BitVector a -> BitVector b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize

instance (KnownNat n, KnownNat m, n <= m) => NumConvert (BitVector n) (BitVector m) where
  numConvert :: BitVector n -> BitVector m
numConvert = BitVector n -> BitVector m
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
BitVector a -> BitVector b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize

instance (NumConvert (Unsigned WORD_SIZE_IN_BITS) a) => NumConvert Word a where
  numConvert :: Word -> a
numConvert !Word
a = Unsigned 64 -> a
forall a b. NumConvert a b => a -> b
numConvert (Unsigned 64 -> a) -> Unsigned 64 -> a
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Unsigned 64) Word
a
instance (NumConvert (Unsigned 64) a) => NumConvert Word64 a where
  numConvert :: Word64 -> a
numConvert !Word64
a = Unsigned 64 -> a
forall a b. NumConvert a b => a -> b
numConvert (Unsigned 64 -> a) -> Unsigned 64 -> a
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Unsigned 64) Word64
a
instance (NumConvert (Unsigned 32) a) => NumConvert Word32 a where
  numConvert :: Word32 -> a
numConvert !Word32
a = Unsigned 32 -> a
forall a b. NumConvert a b => a -> b
numConvert (Unsigned 32 -> a) -> Unsigned 32 -> a
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Unsigned 32) Word32
a
instance (NumConvert (Unsigned 16) a) => NumConvert Word16 a where
  numConvert :: Word16 -> a
numConvert !Word16
a = Unsigned 16 -> a
forall a b. NumConvert a b => a -> b
numConvert (Unsigned 16 -> a) -> Unsigned 16 -> a
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Unsigned 16) Word16
a
instance (NumConvert (Unsigned 8) a) => NumConvert Word8 a where
  numConvert :: Word8 -> a
numConvert !Word8
a = Unsigned 8 -> a
forall a b. NumConvert a b => a -> b
numConvert (Unsigned 8 -> a) -> Unsigned 8 -> a
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Unsigned 8) Word8
a

instance (NumConvert (Signed WORD_SIZE_IN_BITS) a) => NumConvert Int a where
  numConvert :: Int -> a
numConvert !Int
a = Signed 64 -> a
forall a b. NumConvert a b => a -> b
numConvert (Signed 64 -> a) -> Signed 64 -> a
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Signed 64) Int
a
instance (NumConvert (Signed 64) a) => NumConvert Int64 a where
  numConvert :: Int64 -> a
numConvert !Int64
a = Signed 64 -> a
forall a b. NumConvert a b => a -> b
numConvert (Signed 64 -> a) -> Signed 64 -> a
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Signed 64) Int64
a
instance (NumConvert (Signed 32) a) => NumConvert Int32 a where
  numConvert :: Int32 -> a
numConvert !Int32
a = Signed 32 -> a
forall a b. NumConvert a b => a -> b
numConvert (Signed 32 -> a) -> Signed 32 -> a
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Signed 32) Int32
a
instance (NumConvert (Signed 16) a) => NumConvert Int16 a where
  numConvert :: Int16 -> a
numConvert !Int16
a = Signed 16 -> a
forall a b. NumConvert a b => a -> b
numConvert (Signed 16 -> a) -> Signed 16 -> a
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Signed 16) Int16
a
instance (NumConvert (Signed 8) a) => NumConvert Int8 a where
  numConvert :: Int8 -> a
numConvert !Int8
a = Signed 8 -> a
forall a b. NumConvert a b => a -> b
numConvert (Signed 8 -> a) -> Signed 8 -> a
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @_ @(Signed 8) Int8
a

instance (NumConvert a (Unsigned WORD_SIZE_IN_BITS)) => NumConvert a Word where
  numConvert :: a -> Word
numConvert = forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Unsigned 64) (Unsigned 64 -> Word) -> (a -> Unsigned 64) -> a -> Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Unsigned 64
forall a b. NumConvert a b => a -> b
numConvert
instance (NumConvert a (Unsigned 64)) => NumConvert a Word64 where
  numConvert :: a -> Word64
numConvert = forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Unsigned 64) (Unsigned 64 -> Word64) -> (a -> Unsigned 64) -> a -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Unsigned 64
forall a b. NumConvert a b => a -> b
numConvert
instance (NumConvert a (Unsigned 32)) => NumConvert a Word32 where
  numConvert :: a -> Word32
numConvert = forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Unsigned 32) (Unsigned 32 -> Word32) -> (a -> Unsigned 32) -> a -> Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Unsigned 32
forall a b. NumConvert a b => a -> b
numConvert
instance (NumConvert a (Unsigned 16)) => NumConvert a Word16 where
  numConvert :: a -> Word16
numConvert = forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Unsigned 16) (Unsigned 16 -> Word16) -> (a -> Unsigned 16) -> a -> Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Unsigned 16
forall a b. NumConvert a b => a -> b
numConvert
instance (NumConvert a (Unsigned 8)) => NumConvert a Word8 where
  numConvert :: a -> Word8
numConvert = forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Unsigned 8) (Unsigned 8 -> Word8) -> (a -> Unsigned 8) -> a -> Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Unsigned 8
forall a b. NumConvert a b => a -> b
numConvert

instance (NumConvert a (Signed WORD_SIZE_IN_BITS)) => NumConvert a Int where
  numConvert :: a -> Int
numConvert = forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Signed 64) (Signed 64 -> Int) -> (a -> Signed 64) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Signed 64
forall a b. NumConvert a b => a -> b
numConvert
instance (NumConvert a (Signed 64)) => NumConvert a Int64 where
  numConvert :: a -> Int64
numConvert = forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Signed 64) (Signed 64 -> Int64) -> (a -> Signed 64) -> a -> Int64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Signed 64
forall a b. NumConvert a b => a -> b
numConvert
instance (NumConvert a (Signed 32)) => NumConvert a Int32 where
  numConvert :: a -> Int32
numConvert = forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Signed 32) (Signed 32 -> Int32) -> (a -> Signed 32) -> a -> Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Signed 32
forall a b. NumConvert a b => a -> b
numConvert
instance (NumConvert a (Signed 16)) => NumConvert a Int16 where
  numConvert :: a -> Int16
numConvert = forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Signed 16) (Signed 16 -> Int16) -> (a -> Signed 16) -> a -> Int16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Signed 16
forall a b. NumConvert a b => a -> b
numConvert
instance (NumConvert a (Signed 8)) => NumConvert a Int8 where
  numConvert :: a -> Int8
numConvert = forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Signed 8) (Signed 8 -> Int8) -> (a -> Signed 8) -> a -> Int8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Signed 8
forall a b. NumConvert a b => a -> b
numConvert

instance (NumConvert a (BitVector 1)) => NumConvert a Bit where
  numConvert :: a -> Bit
numConvert = BitVector 1 -> Bit
BitVector (BitSize Bit) -> Bit
forall a. BitPack a => BitVector (BitSize a) -> a
unpack (BitVector 1 -> Bit) -> (a -> BitVector 1) -> a -> Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> BitVector 1
forall a b. NumConvert a b => a -> b
numConvert
instance (NumConvert (BitVector 1) a) => NumConvert Bit a where
  numConvert :: Bit -> a
numConvert = BitVector 1 -> a
forall a b. NumConvert a b => a -> b
numConvert (BitVector 1 -> a) -> (Bit -> BitVector 1) -> Bit -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bit -> BitVector 1
Bit -> BitVector (BitSize Bit)
forall a. BitPack a => a -> BitVector (BitSize a)
pack