@@ -9,6 +9,7 @@ Maintainer : QBayLogic B.V. <devops@qbaylogic.com>
9
9
{-# LANGUAGE CPP #-}
10
10
{-# LANGUAGE DeriveAnyClass #-}
11
11
{-# LANGUAGE FlexibleContexts #-}
12
+ {-# LANGUAGE FlexibleInstances #-}
12
13
{-# LANGUAGE MultiParamTypeClasses #-}
13
14
{-# LANGUAGE RoleAnnotations #-}
14
15
{-# LANGUAGE TemplateHaskell #-}
@@ -21,6 +22,7 @@ Maintainer : QBayLogic B.V. <devops@qbaylogic.com>
21
22
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
22
23
23
24
{-# OPTIONS_HADDOCK show-extensions not-home #-}
25
+ {-# OPTIONS_GHC -fno-warn-orphans #-}
24
26
25
27
module Clash.Sized.Internal.Index
26
28
( -- * Datatypes
@@ -75,8 +77,10 @@ import Prelude hiding (even, odd)
75
77
76
78
import Control.DeepSeq (NFData (.. ))
77
79
import Data.Bits (Bits (.. ), FiniteBits (.. ))
80
+ import Data.Constraint (Dict (.. ))
78
81
import Data.Data (Data )
79
82
import Data.Default.Class (Default (.. ))
83
+ import Data.Proxy (Proxy (.. ))
80
84
import Text.Read (Read (.. ), ReadPrec )
81
85
import Text.Printf (PrintfArg (.. ), printf )
82
86
import Data.Ix (Ix (.. ))
@@ -93,9 +97,11 @@ import Language.Haskell.TH (TypeQ)
93
97
import GHC.Generics (Generic )
94
98
import GHC.Natural (Natural , naturalFromInteger )
95
99
import GHC.Natural (naturalToInteger )
100
+ import GHC.Num.Integer (integerLog2 )
96
101
import GHC.Stack (HasCallStack )
97
102
import GHC.TypeLits (KnownNat , Nat , type (+ ), type (- ),
98
103
type (* ), type (<= ), natVal )
104
+ import GHC.TypeLits.KnownNat (KnownNat1 (.. ), SNatKn (.. ), nameToSymbol )
99
105
import GHC.TypeLits.Extra (CLog )
100
106
import Test.QuickCheck.Arbitrary (Arbitrary (.. ), CoArbitrary (.. ),
101
107
arbitraryBoundedIntegral ,
@@ -111,9 +117,10 @@ import Clash.Class.BitPack.BitIndex (replaceBit)
111
117
import Clash.Sized.Internal (formatRange )
112
118
import {- # SOURCE #-} Clash.Sized.Internal.BitVector (BitVector (BV ), high , low , undefError )
113
119
import qualified Clash.Sized.Internal.BitVector as BV
114
- import Clash.Promoted.Nat (SNat (.. ), snatToNum , natToInteger , leToPlusKN )
120
+ import Clash.Promoted.Nat (SNat (.. ), SNatLE ( .. ), snatToNum , natToInteger , leToPlusKN , compareSNat )
115
121
import Clash.XException
116
122
(ShowX (.. ), NFDataX (.. ), errorX , showsPrecXWith , rwhnfX , seqX )
123
+ import Unsafe.Coerce (unsafeCoerce )
117
124
118
125
{- $setup
119
126
>>> import Clash.Sized.Internal.Index
@@ -184,10 +191,28 @@ instance NFData (Index n) where
184
191
-- NOINLINE is needed so that Clash doesn't trip on the "Index ~# Integer"
185
192
-- coercion
186
193
187
- instance (KnownNat n , 1 <= n ) => BitPack (Index n ) where
188
- type BitSize (Index n ) = CLog 2 n
189
- pack = packXWith pack#
190
- unpack = unpack#
194
+ instance KnownNat n => BitPack (Index n ) where
195
+ type BitSize (Index n ) = BitSizeIndex n
196
+ pack = case compareSNat (SNat @ 1 ) (SNat @ n ) of
197
+ SNatGT -> const 0
198
+ SNatLE | Dict <- fact @ n -> packXWith pack#
199
+ unpack = case compareSNat (SNat @ 1 ) (SNat @ n ) of
200
+ SNatGT -> const undefined
201
+ SNatLE | Dict <- fact @ n -> unpack#
202
+
203
+ type family BitSizeIndex (n :: Nat ) where
204
+ BitSizeIndex 0 = 0
205
+ BitSizeIndex n = CLog 2 n
206
+
207
+ instance KnownNat n => KnownNat1 $ (nameToSymbol ''BitSizeIndex) n where
208
+ natSing1 = let n = natVal (Proxy @ n )
209
+ in SNatKn $ if n == 0
210
+ then 0
211
+ else fromInteger $ toInteger $ integerLog2 n
212
+ {-# INLINE natSing1 #-}
213
+
214
+ fact :: forall n . 1 <= n => Dict (CLog 2 n ~ BitSizeIndex n )
215
+ fact = unsafeCoerce (Dict :: Dict (0 ~ 0 ))
191
216
192
217
-- | Safely convert an `SNat` value to an `Index`
193
218
fromSNat :: (KnownNat m , n + 1 <= m ) => SNat n -> Index m
0 commit comments