Skip to content

Commit 6d3840f

Browse files
martijnbastiaanmartijnbastiaan
committed
Add Clash.Class.Convert
Utilities for safely converting between various Clash number types.
1 parent 952fd85 commit 6d3840f

File tree

8 files changed

+972
-1
lines changed

8 files changed

+972
-1
lines changed

‎changelog/2025-03-30T20_42_00+02_00_add_clash_class_convert

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

‎clash-prelude/clash-prelude.cabal

+5
Original file line numberDiff line numberDiff line change
@@ -182,6 +182,9 @@ Library
182182
Clash.Class.Counter
183183
Clash.Class.Counter.Internal
184184
Clash.Class.Counter.TH
185+
Clash.Class.Convert
186+
Clash.Class.Convert.Internal.Convert
187+
Clash.Class.Convert.Internal.MaybeConvert
185188
Clash.Class.Exp
186189
Clash.Class.HasDomain
187190
Clash.Class.HasDomain.HasSingleDomain
@@ -428,10 +431,12 @@ test-suite unittests
428431
Clash.Tests.BlockRam.Blob
429432
Clash.Tests.Clocks
430433
Clash.Tests.Counter
434+
Clash.Tests.Convert
431435
Clash.Tests.DerivingDataRepr
432436
Clash.Tests.DerivingDataReprTypes
433437
Clash.Tests.Fixed
434438
Clash.Tests.FixedExhaustive
439+
Clash.Tests.MaybeConvert
435440
Clash.Tests.MaybeX
436441
Clash.Tests.NFDataX
437442
Clash.Tests.NumNewtypes

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

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
{-# LANGUAGE CPP #-}
2+
{-# LANGUAGE MonoLocalBinds #-}
3+
{-# LANGUAGE UndecidableInstances #-}
4+
5+
{- | Utilities for converting between Clash number types in a safe way. Its
6+
existence is motivated by the observation that Clash users often need to convert
7+
between different number types (e.g., 'Clash.Sized.Unsigned.Unsigned' to
8+
'Clash.Sized.Signed.Signed') and that it is not always clear how to do so
9+
properly. Two classes are exported:
10+
11+
* 'Convert': for conversions that, based on types, are guaranteed to succeed.
12+
* 'MaybeConvert': for conversions that may fail for some values.
13+
14+
As opposed to 'Prelude.fromIntegral', all conversions are translatable to
15+
synthesizable HDL.
16+
17+
== __Relation to @convertible@__
18+
@clash-convertible@ is similar to the @convertible@ package in that it aims to
19+
facilitate conversions between different number types. It has two key differences:
20+
21+
1. It offers no partial functions.
22+
2. All its conversions are translatable to synthesizable HDL.
23+
24+
-}
25+
module Clash.Class.Convert (
26+
Convert (..),
27+
MaybeConvert (..),
28+
) where
29+
30+
import Clash.Class.Convert.Internal.Convert
31+
import Clash.Class.Convert.Internal.MaybeConvert

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

+163
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,163 @@
1+
{-# LANGUAGE FlexibleContexts #-}
2+
{-# LANGUAGE FlexibleInstances #-}
3+
{-# LANGUAGE MultiParamTypeClasses #-}
4+
{-# LANGUAGE UndecidableInstances #-}
5+
6+
{-# OPTIONS_HADDOCK hide #-}
7+
8+
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}
9+
10+
module Clash.Class.Convert.Internal.Convert where
11+
12+
import Prelude
13+
14+
import Clash.Class.BitPack
15+
import Clash.Class.Resize
16+
import Clash.Sized.BitVector
17+
import Clash.Sized.Index
18+
import Clash.Sized.Signed
19+
import Clash.Sized.Unsigned
20+
21+
import GHC.TypeLits.Extra (CLog)
22+
import GHC.TypeLits (KnownNat, type (<=), type (+), type (^))
23+
24+
import Data.Int (Int16, Int32, Int64, Int8)
25+
import Data.Word (Word16, Word32, Word64, Word8)
26+
27+
{- $setup
28+
>>> import Clash.Prelude
29+
>>> import Clash.Clash.Convert
30+
-}
31+
32+
{- | Conversions that are, based on their types, guaranteed to succeed.
33+
34+
== __Laws__
35+
A conversion is safe and total if a round trip conversion is guaranteed to be
36+
lossless. I.e.,
37+
38+
> Just x == maybeConvert (convert @a @b x)
39+
40+
for all values @x@ of type @a@. It should also preserve the numerical value
41+
interpretation of the bits. For types that have an "Integral" instance, this
42+
intuition is captured by:
43+
44+
> toInteger x == toInteger (convert @a @b x)
45+
46+
Instances should make sure their constraints are as \"tight\" as possible. I.e.,
47+
if an instance exist, but the constraints cannot be satisfied, then
48+
'Clash.Class.Convert.convertMaybe' should return 'Nothing' for one or more values in
49+
the domain of the source type @a@:
50+
51+
> L.any isNothing (L.map (maybeConvert @a @b) [minBound ..])
52+
53+
Additionally, any implementation should be translatable to synthesizable RTL.
54+
-}
55+
class Convert a b where
56+
{- | Convert a supplied value of type @a@ to a value of type @b@. The conversion
57+
is guaranteed to succeed.
58+
59+
>>> convert (3 :: Index 8) :: Unsigned 8
60+
3
61+
62+
The following will fail with a type error, as we cannot prove that all values
63+
of @Index 8@ can be represented by an @Unsigned 2@:
64+
65+
>>> convert (3 :: Index 8) :: Unsigned 2
66+
...
67+
68+
For the time being, if the input is an @XException@, then the output is too. This
69+
property might be relaxed in the future.
70+
-}
71+
convert :: a -> b
72+
73+
instance (KnownNat n, KnownNat m, n <= m) => Convert (Index n) (Index m) where
74+
convert = resize
75+
76+
instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => Convert (Index n) (Unsigned m) where
77+
convert !a = resize $ bitCoerce a
78+
79+
{- | Note: Conversion from @Index 1@ to @Signed 0@ is total, but not within the
80+
constraints of the instance.
81+
-}
82+
instance (KnownNat n, KnownNat m, 1 <= n, CLog 2 n + 1 <= m) => Convert (Index n) (Signed m) where
83+
convert !a = convert $ bitCoerce @_ @(Unsigned (CLog 2 n)) a
84+
85+
instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => Convert (Index n) (BitVector m) where
86+
convert !a = resize $ pack a
87+
88+
instance (KnownNat n, KnownNat m, 1 <= m, 2 ^ n <= m) => Convert (Unsigned n) (Index m) where
89+
convert !a = bitCoerce $ resize a
90+
91+
instance (KnownNat n, KnownNat m, n <= m) => Convert (Unsigned n) (Unsigned m) where
92+
convert = resize
93+
94+
{- | Note: Conversion from @Unsigned 0@ to @Signed 0@ is total, but not within the
95+
constraints of the instance.
96+
-}
97+
instance (KnownNat n, KnownNat m, n + 1 <= m) => Convert (Unsigned n) (Signed m) where
98+
convert = bitCoerce . resize
99+
100+
instance (KnownNat n, KnownNat m, n <= m) => Convert (Unsigned n) (BitVector m) where
101+
convert !a = resize $ pack a
102+
103+
instance (KnownNat n, KnownNat m, n <= m) => Convert (Signed n) (Signed m) where
104+
convert !a = resize a
105+
106+
instance (KnownNat n, KnownNat m, 1 <= m, 2 ^ n <= m) => Convert (BitVector n) (Index m) where
107+
convert = unpack . resize
108+
109+
instance (KnownNat n, KnownNat m, n <= m) => Convert (BitVector n) (Unsigned m) where
110+
convert = unpack . resize
111+
112+
{- | Note: Conversion from @BitVector 0@ to @Signed 0@ is total, but not within the
113+
constraints of the instance.
114+
-}
115+
instance (KnownNat n, KnownNat m, n + 1 <= m) => Convert (BitVector n) (Signed m) where
116+
convert = unpack . resize
117+
118+
instance (KnownNat n, KnownNat m, n <= m) => Convert (BitVector n) (BitVector m) where
119+
convert = resize
120+
121+
instance (Convert (Unsigned 64) a) => Convert Word a where
122+
convert = convert . bitCoerce @_ @(Unsigned 64)
123+
instance (Convert (Unsigned 64) a) => Convert Word64 a where
124+
convert = convert . bitCoerce @_ @(Unsigned 64)
125+
instance (Convert (Unsigned 32) a) => Convert Word32 a where
126+
convert = convert . bitCoerce @_ @(Unsigned 32)
127+
instance (Convert (Unsigned 16) a) => Convert Word16 a where
128+
convert = convert . bitCoerce @_ @(Unsigned 16)
129+
instance (Convert (Unsigned 8) a) => Convert Word8 a where
130+
convert = convert . bitCoerce @_ @(Unsigned 8)
131+
132+
instance (Convert (Signed 64) a) => Convert Int a where
133+
convert = convert . bitCoerce @_ @(Signed 64)
134+
instance (Convert (Signed 64) a) => Convert Int64 a where
135+
convert = convert . bitCoerce @_ @(Signed 64)
136+
instance (Convert (Signed 32) a) => Convert Int32 a where
137+
convert = convert . bitCoerce @_ @(Signed 32)
138+
instance (Convert (Signed 16) a) => Convert Int16 a where
139+
convert = convert . bitCoerce @_ @(Signed 16)
140+
instance (Convert (Signed 8) a) => Convert Int8 a where
141+
convert = convert . bitCoerce @_ @(Signed 8)
142+
143+
instance (Convert a (Unsigned 64)) => Convert a Word where
144+
convert = bitCoerce @(Unsigned 64) . convert
145+
instance (Convert a (Unsigned 64)) => Convert a Word64 where
146+
convert = bitCoerce @(Unsigned 64) . convert
147+
instance (Convert a (Unsigned 32)) => Convert a Word32 where
148+
convert = bitCoerce @(Unsigned 32) . convert
149+
instance (Convert a (Unsigned 16)) => Convert a Word16 where
150+
convert = bitCoerce @(Unsigned 16) . convert
151+
instance (Convert a (Unsigned 8)) => Convert a Word8 where
152+
convert = bitCoerce @(Unsigned 8) . convert
153+
154+
instance (Convert a (Signed 64)) => Convert a Int where
155+
convert = bitCoerce @(Signed 64) . convert
156+
instance (Convert a (Signed 64)) => Convert a Int64 where
157+
convert = bitCoerce @(Signed 64) . convert
158+
instance (Convert a (Signed 32)) => Convert a Int32 where
159+
convert = bitCoerce @(Signed 32) . convert
160+
instance (Convert a (Signed 16)) => Convert a Int16 where
161+
convert = bitCoerce @(Signed 16) . convert
162+
instance (Convert a (Signed 8)) => Convert a Int8 where
163+
convert = bitCoerce @(Signed 8) . convert

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

+159
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,159 @@
1+
{-# LANGUAGE UndecidableInstances #-}
2+
{-# LANGUAGE MultiParamTypeClasses #-}
3+
{-# LANGUAGE FlexibleInstances #-}
4+
{-# LANGUAGE FlexibleContexts #-}
5+
6+
{-# OPTIONS_HADDOCK hide #-}
7+
8+
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Extra.Solver #-}
9+
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}
10+
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}
11+
12+
module Clash.Class.Convert.Internal.MaybeConvert where
13+
14+
import Clash.Class.BitPack
15+
import Clash.Class.Resize
16+
import Clash.Sized.BitVector
17+
import Clash.Sized.Index
18+
import Clash.Sized.Signed
19+
import Clash.Sized.Unsigned
20+
21+
import GHC.TypeLits.Extra (CLog)
22+
import GHC.TypeLits (KnownNat, type (<=), type (+), type (^))
23+
24+
import Data.Int (Int16, Int32, Int64, Int8)
25+
import Data.Word (Word16, Word32, Word64, Word8)
26+
27+
{- $setup
28+
>>> import Clash.Prelude
29+
>>> import Clash.Class.Convert
30+
-}
31+
32+
{- | Conversions that may fail for some values.
33+
34+
== __Laws__
35+
A conversion is safe if a round trip conversion does not produce errors (also
36+
see "Clash.XException"). I.e.,
37+
38+
> x == fromMaybe x (maybeConvert @a @b x >>= maybeConvert @b @a)
39+
40+
for all values @x@ of type @a@. It should also preserve the numerical value
41+
interpretation of the bits. For types that have an "Integral" instance, this
42+
intuition is captured by:
43+
44+
> toInteger x == fromMaybe (toInteger x) (toInteger (convert @a @b x))
45+
46+
If a conversion succeeds one way, it should also succeed the other way. I.e.,
47+
48+
> isJust (maybeConvert @a @b x) `implies` isJust (maybeConvert @a @b x >>= maybeConvert @b @a)
49+
50+
A conversion should succeed if and only if the value is representable in the
51+
target type. For types that have a "Bounded" and "Integral" instance, this
52+
intuition is captured by:
53+
54+
> isJust (maybeConvert @a @b x) == (i x >= i (minBound @b) && i x <= i (maxBound @b))
55+
56+
where @i = toInteger@.
57+
58+
Additionally, any implementation should be translatable to synthesizable RTL.
59+
-}
60+
class MaybeConvert a b where
61+
{- | Convert a supplied value of type @a@ to a value of type @b@. If the value
62+
cannot be represented in the target type, 'Nothing' is returned.
63+
64+
>>> maybeConvert (1 :: Index 8) :: Maybe (Unsigned 2)
65+
Just 1
66+
>>> maybeConvert (7 :: Index 8) :: Maybe (Unsigned 2)
67+
Nothing
68+
69+
For the time being, if the input is an @XException@, then the output is too.
70+
This property might be relaxed in the future.
71+
-}
72+
maybeConvert :: a -> Maybe b
73+
74+
instance (KnownNat n, KnownNat m) => MaybeConvert (Index n) (Index m) where
75+
maybeConvert !a = maybeResize a
76+
77+
instance (KnownNat n, KnownNat m, 1 <= n) => MaybeConvert (Index n) (Unsigned m) where
78+
maybeConvert !a = maybeResize $ bitCoerce @_ @(Unsigned (CLog 2 n)) a
79+
80+
instance (KnownNat n, KnownNat m, 1 <= n) => MaybeConvert (Index n) (Signed m) where
81+
maybeConvert !a = maybeConvert $ bitCoerce @_ @(Unsigned (CLog 2 n)) a
82+
83+
instance (KnownNat n, KnownNat m, 1 <= n) => MaybeConvert (Index n) (BitVector m) where
84+
maybeConvert !a = maybeResize $ pack a
85+
86+
instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (Index m) where
87+
maybeConvert !a = maybeResize $ bitCoerce @_ @(Index (2 ^ n)) a
88+
89+
instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (Unsigned m) where
90+
maybeConvert !a = maybeResize a
91+
92+
instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (Signed m) where
93+
maybeConvert !a = maybeResize $ bitCoerce @(Unsigned (n + 1)) $ extend a
94+
95+
instance (KnownNat n, KnownNat m) => MaybeConvert (Unsigned n) (BitVector m) where
96+
maybeConvert !a = maybeResize $ pack a
97+
98+
instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (Index m) where
99+
maybeConvert n
100+
| n < 0 = Nothing
101+
| otherwise = maybeResize (bitCoerce @_ @(Index (2 ^ (n + 1))) (extend n))
102+
103+
instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (Unsigned m) where
104+
maybeConvert n
105+
| n < 0 = Nothing
106+
| otherwise = maybeResize (bitCoerce @(Signed (n + 1)) (extend n))
107+
108+
instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (Signed m) where
109+
maybeConvert !a = maybeResize a
110+
111+
instance (KnownNat n, KnownNat m) => MaybeConvert (Signed n) (BitVector m) where
112+
maybeConvert n
113+
| n < 0 = Nothing
114+
| otherwise = maybeResize (pack @(Signed (n + 1)) (extend n))
115+
116+
instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (Index m) where
117+
maybeConvert !a = maybeResize $ unpack @(Index (2 ^ n)) a
118+
119+
instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (Unsigned m) where
120+
maybeConvert !a = maybeResize $ unpack @(Unsigned n) a
121+
122+
instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (Signed m) where
123+
maybeConvert !a = maybeResize $ unpack @(Signed (n + 1)) $ extend a
124+
125+
instance (KnownNat n, KnownNat m) => MaybeConvert (BitVector n) (BitVector m) where
126+
maybeConvert !a = maybeResize a
127+
128+
instance (MaybeConvert (Unsigned 64) a) => MaybeConvert Word a where
129+
maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 64)
130+
instance (MaybeConvert (Unsigned 64) a) => MaybeConvert Word64 a where
131+
maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 64)
132+
instance (MaybeConvert (Unsigned 32) a) => MaybeConvert Word32 a where
133+
maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 32)
134+
instance (MaybeConvert (Unsigned 16) a) => MaybeConvert Word16 a where
135+
maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 16)
136+
instance (MaybeConvert (Unsigned 8) a) => MaybeConvert Word8 a where
137+
maybeConvert = maybeConvert . bitCoerce @_ @(Unsigned 8)
138+
139+
instance (MaybeConvert (Signed 64) a) => MaybeConvert Int a where
140+
maybeConvert = maybeConvert . bitCoerce @_ @(Signed 64)
141+
instance (MaybeConvert (Signed 64) a) => MaybeConvert Int64 a where
142+
maybeConvert = maybeConvert . bitCoerce @_ @(Signed 64)
143+
instance (MaybeConvert (Signed 32) a) => MaybeConvert Int32 a where
144+
maybeConvert = maybeConvert . bitCoerce @_ @(Signed 32)
145+
instance (MaybeConvert (Signed 16) a) => MaybeConvert Int16 a where
146+
maybeConvert = maybeConvert . bitCoerce @_ @(Signed 16)
147+
instance (MaybeConvert (Signed 8) a) => MaybeConvert Int8 a where
148+
maybeConvert = maybeConvert . bitCoerce @_ @(Signed 8)
149+
150+
instance (MaybeConvert a (Unsigned 64)) => MaybeConvert a Word where
151+
maybeConvert = fmap (bitCoerce @(Unsigned 64)) . maybeConvert
152+
instance (MaybeConvert a (Unsigned 64)) => MaybeConvert a Word64 where
153+
maybeConvert = fmap (bitCoerce @(Unsigned 64)) . maybeConvert
154+
instance (MaybeConvert a (Unsigned 32)) => MaybeConvert a Word32 where
155+
maybeConvert = fmap (bitCoerce @(Unsigned 32)) . maybeConvert
156+
instance (MaybeConvert a (Unsigned 16)) => MaybeConvert a Word16 where
157+
maybeConvert = fmap (bitCoerce @(Unsigned 16)) . maybeConvert
158+
instance (MaybeConvert a (Unsigned 8)) => MaybeConvert a Word8 where
159+
maybeConvert = fmap (bitCoerce @(Unsigned 8)) . maybeConvert

0 commit comments

Comments
 (0)