Skip to content

Commit 25c7757

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

File tree

8 files changed

+996
-1
lines changed

8 files changed

+996
-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

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

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

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

0 commit comments

Comments
 (0)