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