| Copyright | (C) 2025 Martijn Bastiaan |
|---|---|
| License | BSD2 (see the file LICENSE) |
| Maintainer | QBayLogic B.V. <devops@qbaylogic.com> |
| Safe Haskell | None |
| Language | Haskell2010 |
Clash.Class.NumConvert
Description
Utilities for converting between Clash number types in a non-erroring way. Its
existence is motivated by the observation that Clash users often need to convert
between different number types (e.g., Unsigned to Signed) and that it is not
always clear how to do so properly. Two classes are exported:
NumConvert: for conversions that, based on types, are guaranteed to succeed.MaybeNumConvert: for conversions that may fail for some values.
As opposed to fromIntegral, all conversions are translatable to
synthesizable HDL.
Relation to convertible
Type classes exported here are similar to the convertible package in that it
aims to facilitate conversions between different types. It is different in three
ways:
- It offers no partial functions
- All its conversions are translatable to synthesizable HDL
- It is focused on (Clash's) number types
Synopsis
- class NumConvert a b where
- numConvert :: a -> b
- class MaybeNumConvert a b where
- maybeNumConvert :: a -> Maybe b
Documentation
class NumConvert a b where Source #
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
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.
Methods
numConvert :: a -> b Source #
Convert a supplied value of type a to a value of type b. The conversion
is guaranteed to succeed.
>>>numConvert (3 :: Index 8) :: Unsigned 83
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 XException, then
the output is too. This property might be relaxed in the future.
Instances
class MaybeNumConvert a b where Source #
Conversions that may fail for some values. A successful conversion retains
the numerical value interpretation of the source type in the target type. A
failure is expressed by returning Nothing, never by an XException.
Laws
A conversion is either successful or it fails gracefully. I.e., it does not produces produce errors (also see Clash.XException). I.e.,
x == fromMaybe x (maybeNumConvert @a @b x >>= maybeNumConvert @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 (numConvert @a @b x))
If a conversion succeeds one way, it should also succeed the other way. I.e.,
isJust (maybeNumConvert @a @b x) `implies` isJust (maybeNumConvert @a @b x >>= maybeNumConvert @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 (maybeNumConvert @a @b x) == (i x >= i (minBound @b) && i x <= i (maxBound @b))
where i = toInteger.
All implementations should be total, i.e., they should not produce "bottoms".
Additionally, any implementation should be translatable to synthesizable HDL.
Methods
maybeNumConvert :: a -> Maybe b Source #
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.
>>>maybeNumConvert (1 :: Index 8) :: Maybe (Unsigned 2)Just 1>>>maybeNumConvert (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.