Add Clash.Class.Convert

changelog/2025-03-30T20_42_00+02_00_add_clash_class_convert

@@ -0,0 +1 @@
+ADD: `Clash.Class.Convert`: Utilities for safely converting between various Clash number types

clash-prelude/clash-prelude.cabal

@@ -182,6 +182,9 @@ Library
                       Clash.Class.Counter
                       Clash.Class.Counter.Internal
                       Clash.Class.Counter.TH
+                      Clash.Class.Convert
+                      Clash.Class.Convert.Internal.Convert
+                      Clash.Class.Convert.Internal.MaybeConvert
                       Clash.Class.Exp
                       Clash.Class.HasDomain
                       Clash.Class.HasDomain.HasSingleDomain
@@ -428,10 +431,12 @@ test-suite unittests
                  Clash.Tests.BlockRam.Blob
                  Clash.Tests.Clocks
                  Clash.Tests.Counter
+                 Clash.Tests.Convert
                  Clash.Tests.DerivingDataRepr
                  Clash.Tests.DerivingDataReprTypes
                  Clash.Tests.Fixed
                  Clash.Tests.FixedExhaustive
+                 Clash.Tests.MaybeConvert
                  Clash.Tests.MaybeX
                  Clash.Tests.NFDataX
                  Clash.Tests.NumNewtypes

clash-prelude/src/Clash/Class/Convert.hs

@@ -0,0 +1,31 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{- | Utilities for converting between Clash number types in a safe way. Its
+existence is motivated by the observation that Clash users often need to convert
+between different number types (e.g., 'Clash.Sized.Unsigned.Unsigned' to
+'Clash.Sized.Signed.Signed') and that it is not always clear how to do so
+properly. Two classes are exported:
+
+* 'Convert': for conversions that, based on types, are guaranteed to succeed.
+* 'MaybeConvert': for conversions that may fail for some values.
+
+As opposed to 'Prelude.fromIntegral', all conversions are translatable to
+synthesizable HDL.
+
+== __Relation to @convertible@__
+@clash-convertible@ is similar to the @convertible@ package in that it aims to
+facilitate conversions between different number types. It has two key differences:
+
+ 1. It offers no partial functions.
+ 2. All its conversions are translatable to synthesizable HDL.
+
+-}
+module Clash.Class.Convert (
+  Convert (..),
+  MaybeConvert (..),
+) where
+
+import Clash.Class.Convert.Internal.Convert
+import Clash.Class.Convert.Internal.MaybeConvert

clash-prelude/src/Clash/Class/Convert/Internal/Convert.hs

@@ -0,0 +1,164 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_HADDOCK hide #-}
+
+{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}
+
+module Clash.Class.Convert.Internal.Convert 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.Extra (CLog)
+import GHC.TypeLits (KnownNat, type (<=), type (+), type (^))
+
+import Data.Int (Int16, Int32, Int64, Int8)
+import Data.Word (Word16, Word32, Word64, Word8)
+
+{- $setup
+>>> import Clash.Prelude
+>>> import Clash.Class.Convert
+-}
+
+{- | Conversions that are, based on their types, guaranteed to succeed.
+
+== __Laws__
+A conversion is safe and total if a round trip conversion is guaranteed to be
+lossless. I.e.,
+
+> Just x == maybeConvert (convert @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 (convert @a @b x)
+
+Instances should make sure their constraints are as \"tight\" as possible. I.e.,
+if an instance exist, but the constraints cannot be satisfied, then
+'Clash.Class.Convert.convertMaybe' should return 'Nothing' for one or more values in
+the domain of the source type @a@:
+
+> L.any isNothing (L.map (maybeConvert @a @b) [minBound ..])
+
+Additionally, any implementation should be translatable to synthesizable RTL.
+-}
+class Convert a b where
+  {- | Convert a supplied value of type @a@ to a value of type @b@. The conversion
+  is guaranteed to succeed.
+
+  >>> convert (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@:
+
+  >>> convert (3 :: Index 8) :: Unsigned 2
+  ...
+
+  For the time being, if the input is an @XException@, then the output is too. This
+  property might be relaxed in the future.
+  -}
+  convert :: a -> b
+
+instance (KnownNat n, KnownNat m, n <= m) => Convert (Index n) (Index m) where
+  convert = resize
+
+instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => Convert (Index n) (Unsigned m) where
+  convert !a = resize $ bitCoerce a
+
+{- | Note: Conversion from @Index 1@ to @Signed 0@ is total, but not within the
+constraints of the instance.
+-}
+instance (KnownNat n, KnownNat m, 1 <= n, CLog 2 n + 1 <= m) => Convert (Index n) (Signed m) where
+  convert !a = convert $ bitCoerce @_ @(Unsigned (CLog 2 n)) a
+
+instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => Convert (Index n) (BitVector m) where
+  convert !a = resize $ pack a
+
+instance (KnownNat n, KnownNat m, 1 <= m, 2 ^ n <= m) => Convert (Unsigned n) (Index m) where
+  convert !a = bitCoerce $ resize a
+
+instance (KnownNat n, KnownNat m, n <= m) => Convert (Unsigned n) (Unsigned m) where
+  convert = resize
+
+{- | Note: Conversion from @Unsigned 0@ to @Signed 0@ is total, but not within the
+constraints of the instance.
+-}
+instance (KnownNat n, KnownNat m, n + 1 <= m) => Convert (Unsigned n) (Signed m) where
+  convert = bitCoerce . resize
+
+instance (KnownNat n, KnownNat m, n <= m) => Convert (Unsigned n) (BitVector m) where
+  convert !a = resize $ pack a
+
+instance (KnownNat n, KnownNat m, n <= m) => Convert (Signed n) (Signed m) where
+  convert !a = resize a
+
+instance (KnownNat n, KnownNat m, 1 <= m, 2 ^ n <= m) => Convert (BitVector n) (Index m) where
+  convert = unpack . resize
+
+instance (KnownNat n, KnownNat m, n <= m) => Convert (BitVector n) (Unsigned m) where
+  convert = unpack . resize
+
+{- | Note: Conversion from @BitVector 0@ to @Signed 0@ is total, but not within the
+constraints of the instance.
+-}
+instance (KnownNat n, KnownNat m, n + 1 <= m) => Convert (BitVector n) (Signed m) where
+  convert = unpack . resize
+
+instance (KnownNat n, KnownNat m, n <= m) => Convert (BitVector n) (BitVector m) where
+  convert = resize
+
+instance (Convert (Unsigned 64) a) => Convert Word a where
+  convert = convert . bitCoerce @_ @(Unsigned 64)
+instance (Convert (Unsigned 64) a) => Convert Word64 a where
+  convert = convert . bitCoerce @_ @(Unsigned 64)
+instance (Convert (Unsigned 32) a) => Convert Word32 a where
+  convert = convert . bitCoerce @_ @(Unsigned 32)
+instance (Convert (Unsigned 16) a) => Convert Word16 a where
+  convert = convert . bitCoerce @_ @(Unsigned 16)
+instance (Convert (Unsigned 8) a) => Convert Word8 a where
+  convert = convert . bitCoerce @_ @(Unsigned 8)
+
+instance (Convert (Signed 64) a) => Convert Int a where
+  convert = convert . bitCoerce @_ @(Signed 64)
+instance (Convert (Signed 64) a) => Convert Int64 a where
+  convert = convert . bitCoerce @_ @(Signed 64)
+instance (Convert (Signed 32) a) => Convert Int32 a where
+  convert = convert . bitCoerce @_ @(Signed 32)
+instance (Convert (Signed 16) a) => Convert Int16 a where
+  convert = convert . bitCoerce @_ @(Signed 16)
+instance (Convert (Signed 8) a) => Convert Int8 a where
+  convert = convert . bitCoerce @_ @(Signed 8)
+
+instance (Convert a (Unsigned 64)) => Convert a Word where
+  convert = bitCoerce @(Unsigned 64) . convert
+instance (Convert a (Unsigned 64)) => Convert a Word64 where
+  convert = bitCoerce @(Unsigned 64) . convert
+instance (Convert a (Unsigned 32)) => Convert a Word32 where
+  convert = bitCoerce @(Unsigned 32) . convert
+instance (Convert a (Unsigned 16)) => Convert a Word16 where
+  convert = bitCoerce @(Unsigned 16) . convert
+instance (Convert a (Unsigned 8)) => Convert a Word8 where
+  convert = bitCoerce @(Unsigned 8) . convert
+
+instance (Convert a (Signed 64)) => Convert a Int where
+  convert = bitCoerce @(Signed 64) . convert
+instance (Convert a (Signed 64)) => Convert a Int64 where
+  convert = bitCoerce @(Signed 64) . convert
+instance (Convert a (Signed 32)) => Convert a Int32 where
+  convert = bitCoerce @(Signed 32) . convert
+instance (Convert a (Signed 16)) => Convert a Int16 where
+  convert = bitCoerce @(Signed 16) . convert
+instance (Convert a (Signed 8)) => Convert a Int8 where
+  convert = bitCoerce @(Signed 8) . convert

clash-prelude/src/Clash/Class/Convert/Internal/MaybeConvert.hs

@@ -0,0 +1,160 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_HADDOCK hide #-}
+
+{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Extra.Solver #-}
+{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}
+{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}
+
+module Clash.Class.Convert.Internal.MaybeConvert where
+
+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.Extra (CLog)
+import GHC.TypeLits (KnownNat, type (<=), type (+), type (^))
+
+import Data.Int (Int16, Int32, Int64, Int8)
+import Data.Word (Word16, Word32, Word64, Word8)
+
+{- $setup
+>>> import Clash.Prelude
+>>> import Clash.Class.Convert
+-}
+
+{- | Conversions that may fail for some values.
+
+== __Laws__
+A conversion is safe if a round trip conversion does not produce errors (also
+see "Clash.XException"). I.e.,
+
+> x == fromMaybe x (maybeConvert @a @b x >>= maybeConvert @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 (convert @a @b x))
+
+If a conversion succeeds one way, it should also succeed the other way. I.e.,
+
+> isJust (maybeConvert @a @b x) `implies` isJust (maybeConvert @a @b x >>= maybeConvert @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 (maybeConvert @a @b x) == (i x >= i (minBound @b) && i x <= i (maxBound @b))
+
+where @i = toInteger@.
+
+Additionally, any implementation should be translatable to synthesizable RTL.
+-}
+class MaybeConvert a b where
+  {- | 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.
+
+  >>> maybeConvert (1 :: Index 8) :: Maybe (Unsigned 2)
+  Just 1
+  >>> maybeConvert (7 :: Index 8) :: Maybe (Unsigned 2)
+  Nothing
+
+  For the time being, if the input is an @XException@, then the output is too.
+  This property might be relaxed in the future.
+  -}
+  maybeConvert :: a -> Maybe b
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (Index n) (Index m) where
+  maybeConvert !a = maybeResize a
+
+instance (KnownNat n, KnownNat m, 1 <= n) => MaybeConvert (Index n) (Unsigned m) where
+  maybeConvert !a = maybeResize $ bitCoerce @_ @(Unsigned (CLog 2 n)) a
+
+instance (KnownNat n, KnownNat m, 1 <= n) => MaybeConvert (Index n) (Signed m) where
+  maybeConvert !a = maybeConvert $ bitCoerce @_ @(Unsigned (CLog 2 n)) a
+
+instance (KnownNat n, KnownNat m, 1 <= n) => MaybeConvert (Index n) (BitVector m) where
+  maybeConvert !a = maybeResize $ pack a
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (Index m) where
+  maybeConvert !a = maybeResize $ bitCoerce @_ @(Index (2 ^ n)) a
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (Unsigned m) where
+  maybeConvert !a = maybeResize a
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (Signed m) where
+  maybeConvert !a = maybeResize $ bitCoerce @(Unsigned (n + 1)) $ extend a
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (BitVector m) where
+  maybeConvert !a = maybeResize $ pack a
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (Index m) where
+  maybeConvert n
+    | n < 0 = Nothing
+    | otherwise = maybeResize (bitCoerce @_ @(Index (2 ^ (n + 1))) (extend n))
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (Unsigned m) where
+  maybeConvert n
+    | n < 0 = Nothing
+    | otherwise = maybeResize (bitCoerce @(Signed (n + 1)) (extend n))
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (Signed m) where
+  maybeConvert !a = maybeResize a
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (BitVector m) where
+  maybeConvert n
+    | n < 0 = Nothing
+    | otherwise = maybeResize (pack @(Signed (n + 1)) (extend n))
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (Index m) where
+  maybeConvert !a = maybeResize $ unpack @(Index (2 ^ n)) a
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (Unsigned m) where
+  maybeConvert !a = maybeResize $ unpack @(Unsigned n) a
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (Signed m) where
+  maybeConvert !a = maybeResize $ unpack @(Signed (n + 1)) $ extend a
+
+instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (BitVector m) where
+  maybeConvert !a = maybeResize a
+
+instance (MaybeConvert (Unsigned 64) a) => MaybeConvert Word a where
+  maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 64)
+instance (MaybeConvert (Unsigned 64) a) => MaybeConvert Word64 a where
+  maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 64)
+instance (MaybeConvert (Unsigned 32) a) => MaybeConvert Word32 a where
+  maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 32)
+instance (MaybeConvert (Unsigned 16) a) => MaybeConvert Word16 a where
+  maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 16)
+instance (MaybeConvert (Unsigned 8) a) => MaybeConvert Word8 a where
+  maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 8)
+
+instance (MaybeConvert (Signed 64) a) => MaybeConvert Int a where
+  maybeConvert = maybeConvert . bitCoerce @_ @(Signed 64)
+instance (MaybeConvert (Signed 64) a) => MaybeConvert Int64 a where
+  maybeConvert = maybeConvert . bitCoerce @_ @(Signed 64)
+instance (MaybeConvert (Signed 32) a) => MaybeConvert Int32 a where
+  maybeConvert = maybeConvert . bitCoerce @_ @(Signed 32)
+instance (MaybeConvert (Signed 16) a) => MaybeConvert Int16 a where
+  maybeConvert = maybeConvert . bitCoerce @_ @(Signed 16)
+instance (MaybeConvert (Signed 8) a) => MaybeConvert Int8 a where
+  maybeConvert = maybeConvert . bitCoerce @_ @(Signed 8)
+
+instance (MaybeConvert a (Unsigned 64)) => MaybeConvert a Word where
+  maybeConvert = fmap (bitCoerce @(Unsigned 64)) . maybeConvert
+instance (MaybeConvert a (Unsigned 64)) => MaybeConvert a Word64 where
+  maybeConvert = fmap (bitCoerce @(Unsigned 64)) . maybeConvert
+instance (MaybeConvert a (Unsigned 32)) => MaybeConvert a Word32 where
+  maybeConvert = fmap (bitCoerce @(Unsigned 32)) . maybeConvert
+instance (MaybeConvert a (Unsigned 16)) => MaybeConvert a Word16 where
+  maybeConvert = fmap (bitCoerce @(Unsigned 16)) . maybeConvert
+instance (MaybeConvert a (Unsigned 8)) => MaybeConvert a Word8 where
+  maybeConvert = fmap (bitCoerce @(Unsigned 8)) . maybeConvert