content: {-# 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 = resize
  
  instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => NumConvert (Index n) (Unsigned m) where
    numConvert !a = resize $ bitCoerce 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 !a = numConvert $ bitCoerce @_ @(Unsigned (CLog 2 n)) a
  
  instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => NumConvert (Index n) (BitVector m) where
    numConvert !a = resize $ pack a
  
  instance (KnownNat n, KnownNat m, 1 <= m, 2 ^ n <= m) => NumConvert (Unsigned n) (Index m) where
    numConvert !a = bitCoerce $ resize a
  
  instance (KnownNat n, KnownNat m, n <= m) => NumConvert (Unsigned n) (Unsigned m) where
    numConvert = 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 !a = bitCoerce $ resize a
  
  instance (KnownNat n, KnownNat m, n <= m) => NumConvert (Unsigned n) (BitVector m) where
    numConvert !a = resize $ pack a
  
  instance (KnownNat n, KnownNat m, n <= m) => NumConvert (Signed n) (Signed m) where
    numConvert !a = resize a
  
  instance (KnownNat n, KnownNat m, 1 <= m, 2 ^ n <= m) => NumConvert (BitVector n) (Index m) where
    numConvert = unpack . resize
  
  instance (KnownNat n, KnownNat m, n <= m) => NumConvert (BitVector n) (Unsigned m) where
    numConvert = unpack . 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 = unpack . resize
  
  instance (KnownNat n, KnownNat m, n <= m) => NumConvert (BitVector n) (BitVector m) where
    numConvert = resize
  
  instance (NumConvert (Unsigned WORD_SIZE_IN_BITS) a) => NumConvert Word a where
    numConvert !a = numConvert $ bitCoerce @_ @(Unsigned 64) a
  instance (NumConvert (Unsigned 64) a) => NumConvert Word64 a where
    numConvert !a = numConvert $ bitCoerce @_ @(Unsigned 64) a
  instance (NumConvert (Unsigned 32) a) => NumConvert Word32 a where
    numConvert !a = numConvert $ bitCoerce @_ @(Unsigned 32) a
  instance (NumConvert (Unsigned 16) a) => NumConvert Word16 a where
    numConvert !a = numConvert $ bitCoerce @_ @(Unsigned 16) a
  instance (NumConvert (Unsigned 8) a) => NumConvert Word8 a where
    numConvert !a = numConvert $ bitCoerce @_ @(Unsigned 8) a
  
  instance (NumConvert (Signed WORD_SIZE_IN_BITS) a) => NumConvert Int a where
    numConvert !a = numConvert $ bitCoerce @_ @(Signed 64) a
  instance (NumConvert (Signed 64) a) => NumConvert Int64 a where
    numConvert !a = numConvert $ bitCoerce @_ @(Signed 64) a
  instance (NumConvert (Signed 32) a) => NumConvert Int32 a where
    numConvert !a = numConvert $ bitCoerce @_ @(Signed 32) a
  instance (NumConvert (Signed 16) a) => NumConvert Int16 a where
    numConvert !a = numConvert $ bitCoerce @_ @(Signed 16) a
  instance (NumConvert (Signed 8) a) => NumConvert Int8 a where
    numConvert !a = numConvert $ bitCoerce @_ @(Signed 8) a
  
  instance (NumConvert a (Unsigned WORD_SIZE_IN_BITS)) => NumConvert a Word where
    numConvert = bitCoerce @(Unsigned 64) . numConvert
  instance (NumConvert a (Unsigned 64)) => NumConvert a Word64 where
    numConvert = bitCoerce @(Unsigned 64) . numConvert
  instance (NumConvert a (Unsigned 32)) => NumConvert a Word32 where
    numConvert = bitCoerce @(Unsigned 32) . numConvert
  instance (NumConvert a (Unsigned 16)) => NumConvert a Word16 where
    numConvert = bitCoerce @(Unsigned 16) . numConvert
  instance (NumConvert a (Unsigned 8)) => NumConvert a Word8 where
    numConvert = bitCoerce @(Unsigned 8) . numConvert
  
  instance (NumConvert a (Signed WORD_SIZE_IN_BITS)) => NumConvert a Int where
    numConvert = bitCoerce @(Signed 64) . numConvert
  instance (NumConvert a (Signed 64)) => NumConvert a Int64 where
    numConvert = bitCoerce @(Signed 64) . numConvert
  instance (NumConvert a (Signed 32)) => NumConvert a Int32 where
    numConvert = bitCoerce @(Signed 32) . numConvert
  instance (NumConvert a (Signed 16)) => NumConvert a Int16 where
    numConvert = bitCoerce @(Signed 16) . numConvert
  instance (NumConvert a (Signed 8)) => NumConvert a Int8 where
    numConvert = bitCoerce @(Signed 8) . numConvert
  
  instance (NumConvert a (BitVector 1)) => NumConvert a Bit where
    numConvert = unpack . numConvert
  instance (NumConvert (BitVector 1) a) => NumConvert Bit a where
    numConvert = numConvert . pack
  