Skip to content

Commit 44ee96e

Browse files
kleinreactkleinreact
committed
Add BitPack instance for Index 0
1 parent 2423678 commit 44ee96e

File tree

8 files changed

+79
-70
lines changed

8 files changed

+79
-70
lines changed

‎clash-prelude/clash-prelude.cabal‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -331,9 +331,9 @@ Library
331331
extra >= 1.6.17 && < 1.9,
332332
ghc-bignum >= 1.0 && < 1.4,
333333
ghc-prim >= 0.5.1.0 && < 0.13,
334-
ghc-typelits-extra >= 0.4 && < 0.6,
334+
ghc-typelits-extra >= 0.5.2 && < 0.6,
335335
ghc-typelits-knownnat >= 0.7.2 && < 0.9,
336-
ghc-typelits-natnormalise >= 0.7.2 && < 0.10,
336+
ghc-typelits-natnormalise >= 0.9.3 && < 0.10,
337337
hashable >= 1.2.1.0 && < 1.6,
338338
half >= 0.2.2.3 && < 1.0,
339339
infinite-list ^>= 0.1,

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ import Data.Bifunctor (bimap)
2020
import Data.Functor.Identity (Identity(..))
2121
import Data.Int (Int8, Int16, Int32, Int64)
2222
import Data.Word (Word8, Word16, Word32, Word64)
23-
import GHC.TypeLits (KnownNat, type (<=))
23+
import GHC.TypeLits (KnownNat)
2424

2525
-- $setup
2626
-- >>> :m -Prelude
@@ -79,7 +79,7 @@ class Counter a where
7979
| a == minBound = (True, countMax)
8080
| otherwise = (False, pred a)
8181

82-
instance (1 <= n, KnownNat n) => Counter (Index n)
82+
instance KnownNat n => Counter (Index n)
8383
instance KnownNat n => Counter (Unsigned n)
8484
instance KnownNat n => Counter (Signed n)
8585
instance KnownNat n => Counter (BitVector n)
@@ -214,7 +214,7 @@ rippleR f = mapAccumR step True
214214
-- 1 :> 0 :> Nil
215215
-- >>> iterate (SNat @5) (countSucc @T) (9 :> 8 :> Nil)
216216
-- (9 :> 8 :> Nil) :> (9 :> 9 :> Nil) :> (0 :> 0 :> Nil) :> (0 :> 1 :> Nil) :> (0 :> 2 :> Nil) :> Nil
217-
instance (Counter a, KnownNat n, 1 <= n) => Counter (Vec n a) where
217+
instance (Counter a, KnownNat n) => Counter (Vec n a) where
218218
countMin = Vec.repeat countMin
219219
countMax = Vec.repeat countMax
220220

‎clash-prelude/src/Clash/Class/NumConvert/Internal/MaybeNumConvert.hs‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@ import Clash.Sized.Index
2222
import Clash.Sized.Signed
2323
import Clash.Sized.Unsigned
2424

25-
import GHC.TypeLits (KnownNat, type (+), type (<=), type (^))
26-
import GHC.TypeLits.Extra (CLog)
25+
import GHC.TypeLits (KnownNat, type (+), type (^))
26+
import GHC.TypeLits.Extra (CLogWZ)
2727

2828
import Data.Int (Int16, Int32, Int64, Int8)
2929
import Data.Word (Word16, Word32, Word64, Word8)
@@ -82,13 +82,13 @@ class MaybeNumConvert a b where
8282
instance (KnownNat n, KnownNat m) => MaybeNumConvert (Index n) (Index m) where
8383
maybeNumConvert !a = maybeResize a
8484

85-
instance (KnownNat n, KnownNat m, 1 <= n) => MaybeNumConvert (Index n) (Unsigned m) where
86-
maybeNumConvert !a = maybeResize $ bitCoerce @_ @(Unsigned (CLog 2 n)) a
85+
instance (KnownNat n, KnownNat m) => MaybeNumConvert (Index n) (Unsigned m) where
86+
maybeNumConvert !a = maybeResize $ bitCoerce @_ @(Unsigned (CLogWZ 2 n 0)) a
8787

88-
instance (KnownNat n, KnownNat m, 1 <= n) => MaybeNumConvert (Index n) (Signed m) where
89-
maybeNumConvert !a = maybeNumConvert $ bitCoerce @_ @(Unsigned (CLog 2 n)) a
88+
instance (KnownNat n, KnownNat m) => MaybeNumConvert (Index n) (Signed m) where
89+
maybeNumConvert !a = maybeNumConvert $ bitCoerce @_ @(Unsigned (CLogWZ 2 n 0)) a
9090

91-
instance (KnownNat n, KnownNat m, 1 <= n) => MaybeNumConvert (Index n) (BitVector m) where
91+
instance (KnownNat n, KnownNat m) => MaybeNumConvert (Index n) (BitVector m) where
9292
maybeNumConvert !a = maybeResize $ pack a
9393

9494
instance (KnownNat n, KnownNat m) => MaybeNumConvert (Unsigned n) (Index m) where

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ import Clash.Sized.Signed
2626
import Clash.Sized.Unsigned
2727

2828
import GHC.TypeLits (KnownNat, type (+), type (<=), type (^))
29-
import GHC.TypeLits.Extra (CLog)
29+
import GHC.TypeLits.Extra (CLogWZ)
3030

3131
import Data.Int (Int16, Int32, Int64, Int8)
3232
import Data.Word (Word16, Word32, Word64, Word8)
@@ -83,19 +83,19 @@ class NumConvert a b where
8383
instance (KnownNat n, KnownNat m, n <= m) => NumConvert (Index n) (Index m) where
8484
numConvert = resize
8585

86-
instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => NumConvert (Index n) (Unsigned m) where
86+
instance (KnownNat n, KnownNat m, n <= 2 ^ m) => NumConvert (Index n) (Unsigned m) where
8787
numConvert !a = resize $ bitCoerce a
8888

8989
{- | Note: Conversion from @Index 1@ to @Signed 0@ is lossless, but not within the
9090
constraints of the instance.
9191
-}
92-
instance (KnownNat n, KnownNat m, 1 <= n, CLog 2 n + 1 <= m) => NumConvert (Index n) (Signed m) where
93-
numConvert !a = numConvert $ bitCoerce @_ @(Unsigned (CLog 2 n)) a
92+
instance (KnownNat n, KnownNat m, CLogWZ 2 n 0 + 1 <= m) => NumConvert (Index n) (Signed m) where
93+
numConvert !a = numConvert $ bitCoerce @_ @(Unsigned (CLogWZ 2 n 0)) a
9494

95-
instance (KnownNat n, KnownNat m, 1 <= n, n <= 2 ^ m) => NumConvert (Index n) (BitVector m) where
95+
instance (KnownNat n, KnownNat m, n <= 2 ^ m) => NumConvert (Index n) (BitVector m) where
9696
numConvert !a = resize $ pack a
9797

98-
instance (KnownNat n, KnownNat m, 1 <= m, 2 ^ n <= m) => NumConvert (Unsigned n) (Index m) where
98+
instance (KnownNat n, KnownNat m, 2 ^ n <= m) => NumConvert (Unsigned n) (Index m) where
9999
numConvert !a = bitCoerce $ resize a
100100

101101
instance (KnownNat n, KnownNat m, n <= m) => NumConvert (Unsigned n) (Unsigned m) where
@@ -113,7 +113,7 @@ instance (KnownNat n, KnownNat m, n <= m) => NumConvert (Unsigned n) (BitVector
113113
instance (KnownNat n, KnownNat m, n <= m) => NumConvert (Signed n) (Signed m) where
114114
numConvert !a = resize a
115115

116-
instance (KnownNat n, KnownNat m, 1 <= m, 2 ^ n <= m) => NumConvert (BitVector n) (Index m) where
116+
instance (KnownNat n, KnownNat m, 2 ^ n <= m) => NumConvert (BitVector n) (Index m) where
117117
numConvert = unpack . resize
118118

119119
instance (KnownNat n, KnownNat m, n <= m) => NumConvert (BitVector n) (Unsigned m) where

‎clash-prelude/src/Clash/Explicit/BlockRam.hs‎

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -441,7 +441,7 @@ import Data.String.Interpolate (__i)
441441
import GHC.Arr (STArray, unsafeReadSTArray, unsafeWriteSTArray)
442442
import GHC.Generics (Generic)
443443
import GHC.Stack (HasCallStack, withFrozenCallStack)
444-
import GHC.TypeLits (KnownNat, type (^), type (<=))
444+
import GHC.TypeLits (KnownNat, type (^))
445445
import Unsafe.Coerce (unsafeCoerce)
446446

447447
import Clash.Annotations.Primitive
@@ -451,7 +451,7 @@ import Clash.Class.BitPack (bitToBool, msb)
451451
import Clash.Class.Num (SaturationMode(SatBound), satSucc)
452452
import Clash.Explicit.BlockRam.Model (TdpbramModelConfig(..), tdpbramModel)
453453
import Clash.Explicit.Signal (KnownDomain, Enable, register, fromEnable, andEnable)
454-
import Clash.Promoted.Nat (SNat(..))
454+
import Clash.Promoted.Nat (SNat(..), UNat(..), toUNat)
455455
import Clash.Signal.Bundle (unbundle)
456456
import Clash.Signal.Internal
457457
(Clock(..), Reset, Signal (..), invertReset, (.&&.), mux)
@@ -867,7 +867,7 @@ blockRamU
867867
, NFDataX a
868868
, Enum addr
869869
, NFDataX addr
870-
, 1 <= n )
870+
)
871871
=> Clock dom
872872
-- ^ 'Clock' to synchronize to
873873
-> Reset dom
@@ -887,8 +887,11 @@ blockRamU
887887
-- ^ (write address @w@, value to write)
888888
-> Signal dom a
889889
-- ^ Value of the BRAM at address @r@ from the previous clock cycle
890-
blockRamU clk rst0 en rstStrategy n@SNat rd0 mw0 =
891-
case rstStrategy of
890+
blockRamU clk rst0 en rstStrategy n@SNat rd0 mw0 = case toUNat n of
891+
UZero -> case rstStrategy of
892+
ClearOnReset f -> pure $ f undefined
893+
NoClearOnReset -> pure undefined
894+
USucc _ -> case rstStrategy of
892895
ClearOnReset initF ->
893896
-- Use reset infrastructure
894897
blockRamU# clk en n rd1 we1 wa1 w1
@@ -957,7 +960,7 @@ blockRam1
957960
, NFDataX a
958961
, Enum addr
959962
, NFDataX addr
960-
, 1 <= n )
963+
)
961964
=> Clock dom
962965
-- ^ 'Clock' to synchronize to
963966
-> Reset dom
@@ -979,8 +982,9 @@ blockRam1
979982
-- ^ (write address @w@, value to write)
980983
-> Signal dom a
981984
-- ^ Value of the BRAM at address @r@ from the previous clock cycle
982-
blockRam1 clk rst0 en rstStrategy n@SNat a rd0 mw0 =
983-
case rstStrategy of
985+
blockRam1 clk rst0 en rstStrategy n@SNat a rd0 mw0 = case toUNat n of
986+
UZero -> pure a
987+
USucc _ -> case rstStrategy of
984988
ClearOnReset () ->
985989
-- Use reset infrastructure
986990
blockRam1# clk en n a rd1 we1 wa1 w1

‎clash-prelude/src/Clash/Prelude/BlockRam.hs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -404,7 +404,7 @@ where
404404

405405
import Prelude (Enum, Maybe, Eq)
406406

407-
import GHC.TypeLits (KnownNat, type (^), type (<=))
407+
import GHC.TypeLits (KnownNat, type (^))
408408
import GHC.Stack (HasCallStack, withFrozenCallStack)
409409

410410
import qualified Clash.Explicit.BlockRam as E
@@ -740,7 +740,7 @@ blockRamU
740740
, NFDataX a
741741
, Enum addr
742742
, NFDataX addr
743-
, 1 <= n )
743+
)
744744
=> E.ResetStrategy r (Index n -> a)
745745
-- ^ Whether to clear BRAM on asserted reset ('Clash.Explicit.BlockRam.ClearOnReset')
746746
-- or not ('Clash.Explicit.BlockRam.NoClearOnReset'). The reset needs to be
@@ -767,7 +767,7 @@ blockRam1
767767
, NFDataX a
768768
, Enum addr
769769
, NFDataX addr
770-
, 1 <= n )
770+
)
771771
=> E.ResetStrategy r ()
772772
-- ^ Whether to clear BRAM on asserted reset ('Clash.Explicit.BlockRam.ClearOnReset')
773773
-- or not ('Clash.Explicit.BlockRam.NoClearOnReset'). The reset needs to be

‎clash-prelude/src/Clash/Sized/Internal/Index.hs‎

Lines changed: 44 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ import GHC.Natural (naturalToInteger)
9090
import GHC.Stack (HasCallStack)
9191
import GHC.TypeLits (KnownNat, Nat, type (+), type (-),
9292
type (*), type (<=), natVal)
93-
import GHC.TypeLits.Extra (CLog)
93+
import GHC.TypeLits.Extra (CLogWZ)
9494
import Test.QuickCheck.Arbitrary (Arbitrary (..), CoArbitrary (..),
9595
arbitraryBoundedIntegral,
9696
coarbitraryIntegral, shrinkIntegral)
@@ -105,7 +105,7 @@ import Clash.Class.BitPack.BitIndex (replaceBit)
105105
import Clash.Sized.Internal (formatRange)
106106
import {-# SOURCE #-} Clash.Sized.Internal.BitVector (BitVector (BV), high, low, undefError)
107107
import qualified Clash.Sized.Internal.BitVector as BV
108-
import Clash.Promoted.Nat (SNat(..), snatToNum, natToInteger, leToPlusKN)
108+
import Clash.Promoted.Nat (SNat(..), UNat(..), toUNat, snatToNum, natToInteger)
109109
import Clash.XException
110110
(ShowX (..), NFDataX (..), errorX, showsPrecXWith, rwhnfX, seqX)
111111

@@ -161,7 +161,7 @@ data Index (n :: Nat) =
161161
{-# ANN I hasBlackBox #-}
162162

163163
{-# OPAQUE size# #-}
164-
size# :: (KnownNat n, 1 <= n) => Index n -> Int
164+
size# :: KnownNat n => Index n -> Int
165165
size# = BV.size# . pack#
166166

167167
instance NFData (Index n) where
@@ -170,8 +170,8 @@ instance NFData (Index n) where
170170
-- NOINLINE is needed so that Clash doesn't trip on the "Index ~# Integer"
171171
-- coercion
172172

173-
instance (KnownNat n, 1 <= n) => BitPack (Index n) where
174-
type BitSize (Index n) = CLog 2 n
173+
instance KnownNat n => BitPack (Index n) where
174+
type BitSize (Index n) = CLogWZ 2 n 0
175175
pack = packXWith pack#
176176
unpack = unpack#
177177

@@ -181,12 +181,12 @@ fromSNat = snatToNum
181181

182182
{-# OPAQUE pack# #-}
183183
{-# ANN pack# hasBlackBox #-}
184-
pack# :: Index n -> BitVector (CLog 2 n)
184+
pack# :: Index n -> BitVector (CLogWZ 2 n 0)
185185
pack# (I i) = BV 0 (naturalFromInteger i)
186186

187187
{-# OPAQUE unpack# #-}
188188
{-# ANN unpack# hasBlackBox #-}
189-
unpack# :: (KnownNat n, 1 <= n) => BitVector (CLog 2 n) -> Index n
189+
unpack# :: KnownNat n => BitVector (CLogWZ 2 n 0) -> Index n
190190
unpack# (BV 0 i) = fromInteger_INLINE (naturalToInteger i)
191191
unpack# bv = undefError "Index.unpack" [bv]
192192

@@ -343,29 +343,32 @@ minus# (I a) (I b) =
343343
times# :: Index m -> Index n -> Index (((m - 1) * (n - 1)) + 1)
344344
times# (I a) (I b) = I (a * b)
345345

346-
instance (KnownNat n, 1 <= n) => SaturatingNum (Index n) where
347-
satAdd SatWrap a b =
348-
case natToInteger @n of
349-
1 -> a +# b
350-
_ -> leToPlusKN @1 @n $
351-
case plus# a b of
352-
z | let m = fromInteger# (natToInteger @n)
353-
, z >= m -> resize# (z - m)
354-
z -> resize# z
355-
satAdd SatZero a b =
356-
leToPlusKN @1 @n $
346+
347+
instance KnownNat n => SaturatingNum (Index n) where
348+
satAdd SatWrap a b = case toUNat (SNat @n) of
349+
UZero -> a
350+
USucc UZero -> a +# b
351+
USucc (USucc _) -> case plus# a b of
352+
z | let m = fromInteger# (natToInteger @n)
353+
, z >= m -> resize# (z - m)
354+
z -> resize# z
355+
satAdd SatZero a b = case toUNat (SNat @n) of
356+
UZero -> a
357+
USucc _ ->
357358
case plus# a b of
358359
z | let m = fromInteger# (natToInteger @(n - 1))
359360
, z > m -> fromInteger# 0
360361
z -> resize# z
361-
satAdd SatError a b =
362-
leToPlusKN @1 @n $
362+
satAdd SatError a b = case toUNat (SNat @n) of
363+
UZero -> a
364+
USucc _ ->
363365
case plus# a b of
364366
z | let m = fromInteger# (natToInteger @(n - 1))
365367
, z > m -> errorX "Index.satAdd: overflow"
366368
z -> resize# z
367-
satAdd _ a b =
368-
leToPlusKN @1 @n $
369+
satAdd _ a b = case toUNat (SNat @n) of
370+
UZero -> a
371+
USucc _ ->
369372
case plus# a b of
370373
z | let m = fromInteger# (natToInteger @(n - 1))
371374
, z > m -> maxBound#
@@ -384,28 +387,30 @@ instance (KnownNat n, 1 <= n) => SaturatingNum (Index n) where
384387
then fromInteger# 0
385388
else a -# b
386389

387-
satMul SatWrap a b =
388-
case natToInteger @n of
389-
1 -> a *# b
390-
2 -> case a of {0 -> 0; _ -> b}
391-
_ -> leToPlusKN @1 @n $
392-
case times# a b of
393-
z -> let m = fromInteger# (natToInteger @n)
394-
in resize# (z `mod` m)
395-
satMul SatZero a b =
396-
leToPlusKN @1 @n $
390+
satMul SatWrap a b = case toUNat (SNat @n) of
391+
UZero -> a
392+
USucc UZero -> a *# b
393+
USucc (USucc UZero) -> case a of {0 -> 0; _ -> b}
394+
USucc (USucc (USucc _)) -> case times# a b of
395+
z -> let m = fromInteger# (natToInteger @n)
396+
in resize# (z `mod` m)
397+
satMul SatZero a b = case toUNat (SNat @n) of
398+
UZero -> a
399+
USucc _ ->
397400
case times# a b of
398401
z | let m = fromInteger# (natToInteger @(n - 1))
399402
, z > m -> fromInteger# 0
400403
z -> resize# z
401-
satMul SatError a b =
402-
leToPlusKN @1 @n $
404+
satMul SatError a b = case toUNat (SNat @n) of
405+
UZero -> a
406+
USucc _ ->
403407
case times# a b of
404408
z | let m = fromInteger# (natToInteger @(n - 1))
405409
, z > m -> errorX "Index.satMul: overflow"
406410
z -> resize# z
407-
satMul _ a b =
408-
leToPlusKN @1 @n $
411+
satMul _ a b = case toUNat (SNat @n) of
412+
UZero -> a
413+
USucc _ ->
409414
case times# a b of
410415
z | let m = fromInteger# (natToInteger @(n - 1))
411416
, z > m -> maxBound#
@@ -462,11 +467,11 @@ toInteger# (I n) = n
462467
instance KnownNat n => PrintfArg (Index n) where
463468
formatArg = formatArg . toInteger
464469

465-
instance (KnownNat n, 1 <= n) => Parity (Index n) where
470+
instance KnownNat n => Parity (Index n) where
466471
even = even . pack
467472
odd = odd . pack
468473

469-
instance (KnownNat n, 1 <= n) => Bits (Index n) where
474+
instance KnownNat n => Bits (Index n) where
470475
a .&. b = unpack# $ BV.and# (pack# a) (pack# b)
471476
a .|. b = unpack# $ BV.or# (pack# a) (pack# b)
472477
xor a b = unpack# $ BV.xor# (pack# a) (pack# b)
@@ -486,7 +491,7 @@ instance (KnownNat n, 1 <= n) => Bits (Index n) where
486491
rotateR v i = unpack# $ rotateR (pack# v) i
487492
popCount i = popCount (pack# i)
488493

489-
instance (KnownNat n, 1 <= n) => FiniteBits (Index n) where
494+
instance KnownNat n => FiniteBits (Index n) where
490495
finiteBitSize = size#
491496
countLeadingZeros i = countLeadingZeros (pack# i)
492497
countTrailingZeros i = countTrailingZeros (pack# i)

‎clash-prelude/tests/Clash/Tests/NumConvert.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ case_convertIndexSigned =
149149
forM_ [0 .. otherMax] $ \m ->
150150
withSomeSNat n $ \(SNat :: SNat n) ->
151151
withSomeSNat m $ \(SNat :: SNat m) ->
152-
case SNat @(CLog 2 (n + 1) + 1) `compareSNat` SNat @m of
152+
case SNat @(CLogWZ 2 (n + 1) 0 + 1) `compareSNat` SNat @m of
153153
SNatLE -> do
154154
assertBool (show (n, m)) (convertXException (Proxy @(Index (n + 1))) (Proxy @(Signed m)))
155155
forM_ [minBound .. maxBound] $ \(i :: Index (n + 1)) -> do

0 commit comments

Comments
 (0)