Skip to content

Add BitPack instance for Index 0 #2784

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Add BitPack instance for Index 0 #2784

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions cabal.project
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,3 +92,8 @@ package regex-tdfa

-- rewrite-inspector-0.1.0.11 uses brick-0.50 which doesn't compile with vty-6.0
constraints: vty < 6.0

source-repository-package
type: git
location: https://github.com/clash-lang/ghc-typelits-extra.git
tag: 6de31070c86ad451abe329940ba4a0a4b571fb58
22 changes: 16 additions & 6 deletions clash-prelude/src/Clash/Sized/Internal/Index.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,7 @@ import Prelude hiding (even, odd)

import Control.DeepSeq (NFData (..))
import Data.Bits (Bits (..), FiniteBits (..))
import Data.Constraint (Dict(..))
import Data.Data (Data)
import Data.Default.Class (Default (..))
import Text.Read (Read (..), ReadPrec)
Expand All @@ -96,7 +97,7 @@ import GHC.Natural (naturalToInteger)
import GHC.Stack (HasCallStack)
import GHC.TypeLits (KnownNat, Nat, type (+), type (-),
type (*), type (<=), natVal)
import GHC.TypeLits.Extra (CLog)
import GHC.TypeLits.Extra (CLog, CLogWZ)
import Test.QuickCheck.Arbitrary (Arbitrary (..), CoArbitrary (..),
arbitraryBoundedIntegral,
coarbitraryIntegral, shrinkIntegral)
Expand All @@ -111,9 +112,10 @@ import Clash.Class.BitPack.BitIndex (replaceBit)
import Clash.Sized.Internal (formatRange)
import {-# SOURCE #-} Clash.Sized.Internal.BitVector (BitVector (BV), high, low, undefError)
import qualified Clash.Sized.Internal.BitVector as BV
import Clash.Promoted.Nat (SNat(..), snatToNum, natToInteger, leToPlusKN)
import Clash.Promoted.Nat (SNat(..), SNatLE(..), snatToNum, natToInteger, leToPlusKN, compareSNat)
import Clash.XException
(ShowX (..), NFDataX (..), errorX, showsPrecXWith, rwhnfX, seqX)
import Unsafe.Coerce (unsafeCoerce)

{- $setup
>>> import Clash.Sized.Internal.Index
Expand Down Expand Up @@ -184,10 +186,18 @@ instance NFData (Index n) where
-- NOINLINE is needed so that Clash doesn't trip on the "Index ~# Integer"
-- coercion

instance (KnownNat n, 1 <= n) => BitPack (Index n) where
type BitSize (Index n) = CLog 2 n
pack = packXWith pack#
unpack = unpack#
instance KnownNat n => BitPack (Index n) where
type BitSize (Index n) = CLogWZ 2 n 0
pack = case compareSNat (SNat @1) (SNat @n) of
SNatGT -> const 0
SNatLE | Dict <- fact @n @0 -> packXWith pack#
unpack = case compareSNat (SNat @1) (SNat @n) of
SNatGT -> const $ errorX
"any value of type 'Index 0' is undefined"
SNatLE | Dict <- fact @n @0 -> unpack#

fact :: forall n x. 1 <= n => Dict (CLogWZ 2 n x ~ CLog 2 n)
fact = unsafeCoerce (Dict :: Dict (0~0))

-- | Safely convert an `SNat` value to an `Index`
fromSNat :: (KnownNat m, n + 1 <= m) => SNat n -> Index m
Expand Down
Loading