Permalink
Browse files

Simplify KnownNat constraints in for Numeric type operations

Currently, this slows down the performance of the operations
because wrap-around points are computed inside of the operation,
and are not specialised due to the NOINLINE pragmas.

In a planned patch, these NOINLINE pragma's will be removed when
the clash-prelude is compiled for fast compilation, and the
performace lost by the current patch will be recovered.
  • Loading branch information...
christiaanb committed Aug 8, 2016
1 parent 50bbbfa commit e5a6a0ac24ca6c2af59e7410965e69c7b5c42c06
View
@@ -7,6 +7,8 @@ Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
@@ -23,10 +25,11 @@ module CLaSH.Class.BitPack
)
where
import GHC.TypeLits (KnownNat, Nat, type (+), type (^))
import GHC.TypeLits (KnownNat, Nat, type (+))
import Prelude hiding (map)
import CLaSH.Class.Resize (zeroExtend)
import CLaSH.Promoted.Nat (SNat (..), addSNat)
import CLaSH.Sized.BitVector (BitVector, (++#), high, low)
import CLaSH.Sized.Internal.BitVector (split#)
@@ -82,43 +85,43 @@ instance BitPack (BitVector n) where
pack v = v
unpack v = v
instance (KnownNat (BitSize b), KnownNat (2^(BitSize b)), BitPack a, BitPack b) =>
instance (KnownNat (BitSize b), BitPack a, BitPack b) =>
BitPack (a,b) where
type BitSize (a,b) = BitSize a + BitSize b
pack (a,b) = pack a ++# pack b
unpack ab = let (a,b) = split# ab in (unpack a, unpack b)
instance (KnownNat (BitSize c), KnownNat (2^(BitSize c)), BitPack (a,b), BitPack c) =>
instance (KnownNat (BitSize c), BitPack (a,b), BitPack c) =>
BitPack (a,b,c) where
type BitSize (a,b,c) = BitSize (a,b) + BitSize c
pack (a,b,c) = pack (a,b) ++# pack c
unpack (unpack -> ((a,b), c)) = (a,b,c)
instance (KnownNat (BitSize d), KnownNat (2^(BitSize d)), BitPack (a,b,c), BitPack d) =>
instance (KnownNat (BitSize d), BitPack (a,b,c), BitPack d) =>
BitPack (a,b,c,d) where
type BitSize (a,b,c,d) = BitSize (a,b,c) + BitSize d
pack (a,b,c,d) = pack (a,b,c) ++# pack d
unpack (unpack -> ((a,b,c), d)) = (a,b,c,d)
instance (KnownNat (BitSize e), KnownNat (2^(BitSize e)), BitPack (a,b,c,d), BitPack e) =>
instance (KnownNat (BitSize e), BitPack (a,b,c,d), BitPack e) =>
BitPack (a,b,c,d,e) where
type BitSize (a,b,c,d,e) = BitSize (a,b,c,d) + BitSize e
pack (a,b,c,d,e) = pack (a,b,c,d) ++# pack e
unpack (unpack -> ((a,b,c,d), e)) = (a,b,c,d,e)
instance (KnownNat (BitSize f), KnownNat (2^(BitSize f)), BitPack (a,b,c,d,e), BitPack f) =>
instance (KnownNat (BitSize f), BitPack (a,b,c,d,e), BitPack f) =>
BitPack (a,b,c,d,e,f) where
type BitSize (a,b,c,d,e,f) = BitSize (a,b,c,d,e) + BitSize f
pack (a,b,c,d,e,f) = pack (a,b,c,d,e) ++# pack f
unpack (unpack -> ((a,b,c,d,e), f)) = (a,b,c,d,e,f)
instance (KnownNat (BitSize g), KnownNat (2^(BitSize g)), BitPack (a,b,c,d,e,f), BitPack g) =>
instance (KnownNat (BitSize g), BitPack (a,b,c,d,e,f), BitPack g) =>
BitPack (a,b,c,d,e,f,g) where
type BitSize (a,b,c,d,e,f,g) = BitSize (a,b,c,d,e,f) + BitSize g
pack (a,b,c,d,e,f,g) = pack (a,b,c,d,e,f) ++# pack g
unpack (unpack -> ((a,b,c,d,e,f), g)) = (a,b,c,d,e,f,g)
instance (KnownNat (BitSize h), KnownNat (2^(BitSize h)), BitPack (a,b,c,d,e,f,g), BitPack h) =>
instance (KnownNat (BitSize h), BitPack (a,b,c,d,e,f,g), BitPack h) =>
BitPack (a,b,c,d,e,f,g,h) where
type BitSize (a,b,c,d,e,f,g,h) = BitSize (a,b,c,d,e,f,g) + BitSize h
pack (a,b,c,d,e,f,g,h) = pack (a,b,c,d,e,f,g) ++# pack h
@@ -130,5 +133,6 @@ instance (KnownNat (BitSize h), KnownNat (2^(BitSize h)), BitPack (a,b,c,d,e,f,g
-- 00_0001
-- >>> boolToBV False :: BitVector 6
-- 00_0000
boolToBV :: KnownNat (2^(n+1)) => Bool -> BitVector (n + 1)
boolToBV = zeroExtend . pack
boolToBV :: forall n . KnownNat n => Bool -> BitVector (n + 1)
boolToBV = case addSNat (SNat @ n) (SNat @ 1) of
SNat -> zeroExtend . pack
@@ -16,7 +16,7 @@ Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>
module CLaSH.Prelude.BitIndex where
import GHC.TypeLits (KnownNat, type (+), type (-), type (^))
import GHC.TypeLits (KnownNat, type (+), type (-))
import CLaSH.Class.BitPack (BitPack (..))
import CLaSH.Promoted.Nat (SNat)
@@ -74,7 +74,7 @@ slice m n v = slice# (pack v) m n
-- 00_0111
-- >>> split (7 :: Unsigned 6) :: (BitVector 2, BitVector 4)
-- (00,0111)
split :: (BitPack a, BitSize a ~ (m + n), KnownNat n, KnownNat (2^n)) => a
split :: (BitPack a, BitSize a ~ (m + n), KnownNat n) => a
-> (BitVector m, BitVector n)
split v = split# (pack v)
@@ -134,7 +134,7 @@ setSlice m n w v = unpack (setSlice# (pack v) m n w)
-- 00_0100
-- >>> msb (4 :: Signed 6)
-- 0
msb :: (BitPack a, KnownNat (BitSize a - 1)) => a -> Bit
msb :: (BitPack a, KnownNat (BitSize a)) => a -> Bit
msb v = msb# (pack v)
{-# INLINE lsb #-}
@@ -419,7 +419,7 @@ blockRam = blockRam' systemClock
-- * See "CLaSH.Prelude.BlockRam#usingrams" for more information on how to use a
-- Block RAM.
-- * Use the adapter 'readNew' for obtaining write-before-read semantics like this: @readNew (blockRamPow2 inits) wr rd en dt@.
blockRamPow2 :: KnownNat (2^n)
blockRamPow2 :: (KnownNat n, KnownNat (2^n))
=> Vec (2^n) a -- ^ Initial content of the BRAM, also
-- determines the size, @2^n@, of the BRAM.
--
@@ -493,7 +493,7 @@ blockRam' clk content wr rd en din = blockRam# clk content (fromEnum <$> wr)
-- * See "CLaSH.Prelude.BlockRam#usingrams" for more information on how to use a
-- Block RAM.
-- * Use the adapter 'readNew'' for obtaining write-before-read semantics like this: @readNew' clk (blockRamPow2' clk inits) wr rd en dt@.
blockRamPow2' :: KnownNat (2^n)
blockRamPow2' :: (KnownNat n, KnownNat (2^n))
=> SClock clk -- ^ 'Clock' to synchronize to
-> Vec (2^n) a -- ^ Initial content of the BRAM, also
-- determines the size, @2^n@, of
@@ -130,7 +130,7 @@ import CLaSH.Sized.Unsigned (Unsigned)
-- to instantiate a Block RAM with the contents of a data file.
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" for ideas on how to create your
-- own data files.
blockRamFile :: (KnownNat (2^m), Enum addr)
blockRamFile :: (KnownNat m, Enum addr)
=> SNat n -- ^ Size of the blockRAM
-> FilePath -- ^ File describing the initial content
-- of the blockRAM
@@ -170,7 +170,7 @@ blockRamFile = blockRamFile' systemClock
-- to instantiate a Block RAM with the contents of a data file.
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" for ideas on how to create your
-- own data files.
blockRamFilePow2 :: forall n m . (KnownNat (2^m), KnownNat (2^n))
blockRamFilePow2 :: forall n m . (KnownNat m, KnownNat n, KnownNat (2^n))
=> FilePath -- ^ File describing the initial
-- content of the blockRAM
-> Signal (Unsigned n) -- ^ Write address @w@
@@ -209,7 +209,7 @@ blockRamFilePow2 = blockRamFile' systemClock (SNat :: SNat (2^n))
-- to instantiate a Block RAM with the contents of a data file.
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" for ideas on how to create your
-- own data files.
blockRamFilePow2' :: forall clk n m . (KnownNat (2^m), KnownNat (2^n))
blockRamFilePow2' :: forall clk n m . (KnownNat m, KnownNat n, KnownNat (2^n))
=> SClock clk -- ^ 'Clock' to synchronize to
-> FilePath -- ^ File describing the initial
-- content of the blockRAM
@@ -249,7 +249,7 @@ blockRamFilePow2' clk = blockRamFile' clk (SNat :: SNat (2^n))
-- to instantiate a Block RAM with the contents of a data file.
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" for ideas on how to create your
-- own data files.
blockRamFile' :: (KnownNat (2^m), Enum addr)
blockRamFile' :: (KnownNat m, Enum addr)
=> SClock clk -- ^ 'Clock' to synchronize to
-> SNat n -- ^ Size of the blockRAM
-> FilePath -- ^ File describing the initial
@@ -268,7 +268,7 @@ blockRamFile' clk sz file wr rd en din = blockRamFile# clk sz file
{-# NOINLINE blockRamFile# #-}
-- | blockRamFile primitive
blockRamFile# :: KnownNat (2^m)
blockRamFile# :: KnownNat m
=> SClock clk -- ^ 'Clock' to synchronize to
-> SNat n -- ^ Size of the blockRAM
-> FilePath -- ^ File describing the initial
@@ -296,7 +296,7 @@ blockRamFile# clk sz file wr rd en din = register' clk undefined dout
{-# NOINLINE initMem #-}
-- | __NB:__ Not synthesisable
initMem :: KnownNat (2^n) => FilePath -> IO [BitVector n]
initMem :: KnownNat n => FilePath -> IO [BitVector n]
initMem = fmap (map parseBV . lines) . readFile
where
parseBV s = case parseBV' s of
@@ -168,9 +168,8 @@ mooreDF ft fo iS = DF (\i iV oR -> let en = iV .&&. oR
in (o,iV,oR))
fifoDF_mealy :: forall addrSize a .
(((addrSize + 1) - 1) ~ addrSize
,KnownNat addrSize
,KnownNat (2 ^ (addrSize + 1))
(KnownNat addrSize
,KnownNat (addrSize + 1)
,KnownNat (2 ^ addrSize))
=> (Vec (2^addrSize) a, BitVector (addrSize + 1), BitVector (addrSize + 1))
-> (a, Bool, Bool)
@@ -204,7 +203,7 @@ fifoDF :: forall addrSize m n a nm rate .
(((addrSize + 1) - 1) ~ addrSize, KnownNat addrSize,
KnownNat n, KnownNat m,
KnownNat (2 ^ addrSize),
KnownNat (2 ^ (addrSize + 1)),
KnownNat (addrSize + 1),
(m + n) ~ (2 ^ addrSize),
KnownSymbol nm, KnownNat rate)
=> SNat (m + n) -- ^ Depth of the FIFO buffer. Must be a power of two.
@@ -337,7 +336,7 @@ parNDF fs =
--
-- <<doc/loopDF_sync.svg>>
loopDF :: (((addrSize + 1) - 1) ~ addrSize, KnownNat m, KnownNat n, KnownNat addrSize, KnownNat rate
,KnownNat (2 ^ addrSize), KnownNat (2^(addrSize + 1)), KnownSymbol nm
,KnownNat (2 ^ addrSize), KnownNat (addrSize + 1), KnownSymbol nm
,(m+n) ~ (2^addrSize))
=> SNat (m + n) -- ^ Depth of the FIFO buffer. Must be a power of two
-> Vec m d -- ^ Initial content of the FIFO buffer. Can be smaller than
View
@@ -73,7 +73,7 @@ asyncRam = asyncRam' systemClock systemClock
--
-- * See "CLaSH.Prelude.BlockRam#usingrams" for more information on how to use a
-- RAM.
asyncRamPow2 :: forall n a . KnownNat (2^n)
asyncRamPow2 :: forall n a . (KnownNat n, KnownNat (2^n))
=> Signal (Unsigned n) -- ^ Write address @w@
-> Signal (Unsigned n) -- ^ Read address @r@
-> Signal Bool -- ^ Write enable
@@ -91,7 +91,7 @@ asyncRamPow2 = asyncRam' systemClock systemClock (SNat :: SNat (2^n))
-- * See "CLaSH.Prelude.BlockRam#usingrams" for more information on how to use a
-- RAM.
asyncRamPow2' :: forall wclk rclk n a .
KnownNat (2^n)
(KnownNat n, KnownNat (2^n))
=> SClock wclk -- ^ 'Clock' to which to synchronise
-- the write port of the RAM
-> SClock rclk -- ^ 'Clock' to which the read
View
@@ -62,7 +62,7 @@ asyncRom content rd = asyncRom# content (fromEnum rd)
--
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" and "CLaSH.Prelude.BlockRam#usingrams"
-- for ideas on how to use ROMs and RAMs
asyncRomPow2 :: KnownNat (2^n)
asyncRomPow2 :: (KnownNat n, KnownNat (2^n))
=> Vec (2^n) a -- ^ ROM content
--
-- __NB:__ must be a constant
@@ -93,7 +93,7 @@ asyncRom# content rd = arr ! rd
--
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" and "CLaSH.Prelude.BlockRam#usingrams"
-- for ideas on how to use ROMs and RAMs
rom :: (KnownNat n, KnownNat (2^m))
rom :: (KnownNat n, KnownNat m)
=> Vec n a -- ^ ROM content
--
-- __NB:__ must be a constant
@@ -111,7 +111,7 @@ rom = rom' systemClock
--
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" and "CLaSH.Prelude.BlockRam#usingrams"
-- for ideas on how to use ROMs and RAMs
romPow2 :: KnownNat (2^n)
romPow2 :: (KnownNat n, KnownNat (2^n))
=> Vec (2^n) a -- ^ ROM content
--
-- __NB:__ must be a constant
@@ -129,7 +129,7 @@ romPow2 = rom' systemClock
--
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" and "CLaSH.Prelude.BlockRam#usingrams"
-- for ideas on how to use ROMs and RAMs
romPow2' :: KnownNat (2^n)
romPow2' :: (KnownNat n, KnownNat (2^n))
=> SClock clk -- ^ 'Clock' to synchronize to
-> Vec (2^n) a -- ^ ROM content
--
@@ -141,7 +141,7 @@ import CLaSH.Sized.Unsigned (Unsigned)
-- myRomData :: Unsigned 9 -> BitVector 16
-- myRomData = asyncRomFile d512 "memory.bin"
-- @
asyncRomFile :: (KnownNat (2^m), Enum addr)
asyncRomFile :: (KnownNat m, Enum addr)
=> SNat n -- ^ Size of the ROM
-> FilePath -- ^ File describing the content of the ROM
-> addr -- ^ Read address @rd@
@@ -213,15 +213,15 @@ asyncRomFile sz file = asyncRomFile# sz file . fromEnum
-- myRomData :: Unsigned 9 -> BitVector 16
-- myRomData = asyncRomFilePow2 "memory.bin"
-- @
asyncRomFilePow2 :: forall n m . (KnownNat (2^m), KnownNat (2^n))
asyncRomFilePow2 :: forall n m . (KnownNat m, KnownNat n, KnownNat (2^n))
=> FilePath -- ^ File describing the content of the ROM
-> Unsigned n -- ^ Read address @rd@
-> BitVector m -- ^ The value of the ROM at address @rd@
asyncRomFilePow2 = asyncRomFile (SNat :: SNat (2^n))
{-# NOINLINE asyncRomFile# #-}
-- | asyncROMFile primitive
asyncRomFile# :: KnownNat (2^m)
asyncRomFile# :: KnownNat m
=> SNat n -- ^ Size of the ROM
-> FilePath -- ^ File describing the content of the ROM
-> Int -- ^ Read address @rd@
@@ -256,10 +256,10 @@ asyncRomFile# sz file = (content !) -- Leave "(content !)" eta-reduced, see
-- to instantiate a ROM with the contents of a data file.
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" for ideas on how to create your
-- own data files.
romFile :: (KnownNat (2^m), KnownNat (2^k))
romFile :: (KnownNat m, KnownNat n)
=> SNat n -- ^ Size of the ROM
-> FilePath -- ^ File describing the content of the ROM
-> Signal (Unsigned k) -- ^ Read address @rd@
-> Signal (Unsigned n) -- ^ Read address @rd@
-> Signal (BitVector m)
-- ^ The value of the ROM at address @rd@ from the previous clock cycle
romFile = romFile' systemClock
@@ -288,7 +288,7 @@ romFile = romFile' systemClock
-- to instantiate a ROM with the contents of a data file.
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" for ideas on how to create your
-- own data files.
romFilePow2 :: forall n m . (KnownNat (2^m), KnownNat (2^n))
romFilePow2 :: forall n m . (KnownNat m, KnownNat n, KnownNat (2^n))
=> FilePath -- ^ File describing the content of the ROM
-> Signal (Unsigned n) -- ^ Read address @rd@
-> Signal (BitVector m)
@@ -319,7 +319,7 @@ romFilePow2 = romFile' systemClock (SNat :: SNat (2^n))
-- to instantiate a ROM with the contents of a data file.
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" for ideas on how to create your
-- own data files.
romFilePow2' :: forall clk n m . (KnownNat (2^m), KnownNat (2^n))
romFilePow2' :: forall clk n m . (KnownNat m, KnownNat n, KnownNat (2^n))
=> SClock clk -- ^ 'Clock' to synchronize to
-> FilePath -- ^ File describing the content of
-- the ROM
@@ -353,7 +353,7 @@ romFilePow2' clk = romFile' clk (SNat :: SNat (2^n))
-- to instantiate a ROM with the contents of a data file.
-- * See "CLaSH.Sized.Fixed#creatingdatafiles" for ideas on how to create your
-- own data files.
romFile' :: (KnownNat (2^m), Enum addr)
romFile' :: (KnownNat m, Enum addr)
=> SClock clk -- ^ 'Clock' to synchronize to
-> SNat n -- ^ Size of the ROM
-> FilePath -- ^ File describing the content of the
@@ -365,7 +365,7 @@ romFile' clk sz file rd = romFile# clk sz file (fromEnum <$> rd)
{-# NOINLINE romFile# #-}
-- | romFile primitive
romFile# :: KnownNat (2^m)
romFile# :: KnownNat m
=> SClock clk -- ^ 'Clock' to synchronize to
-> SNat n -- ^ Size of the ROM
-> FilePath -- ^ File describing the content of the
Oops, something went wrong.

0 comments on commit e5a6a0a

Please sign in to comment.