clash-prelude 0.3 → 0.4
raw patch · 10 files changed
+564/−120 lines, 10 files
Files
- CHANGELOG.md +14/−0
- clash-prelude.cabal +16/−3
- src/CLaSH/Class/Num.hs +14/−0
- src/CLaSH/Prelude.hs +75/−23
- src/CLaSH/Promoted/Nat.hs +1/−6
- src/CLaSH/Signal.hs +9/−9
- src/CLaSH/Sized/Fixed.hs +157/−0
- src/CLaSH/Sized/Signed.hs +70/−29
- src/CLaSH/Sized/Unsigned.hs +59/−19
- src/CLaSH/Sized/Vector.hs +149/−31
+ CHANGELOG.md view
@@ -0,0 +1,14 @@+# Changelog for [`clash-prelude` package](http://hackage.haskell.org/package/clash-prelude)++## 0.4 *March 20th 2014*+ * Add fixed-point integers+ * Extend documentation+ * 'bit' and 'testBit' functions give run-time errors on out-of-bound positions++## 0.3 *March 14th 2014*+ * Add Documentation+ * Easy SNat literals for 0..1024, e.g. d4 = snat :: SNat 4+ * Fix blockRamPow2++## 0.2 *March 5th 2014*+ * Initial release
clash-prelude.cabal view
@@ -1,8 +1,18 @@ Name: clash-prelude-Version: 0.3+Version: 0.4 Synopsis: CAES Language for Synchronous Hardware - Prelude library--- Description:-Homepage: http://clash.ewi.utwente.nl/+Description:+ CλaSH (pronounced ‘clash’) is a functional hardware description language that+ borrows both its syntax and semantics from the functional programming language+ Haskell. The merits of using a functional language to describe hardware comes+ from the fact that combinational circuits can be directly modeled as+ mathematical functions and that functional languages lend themselves very well+ at describing and (de-)composing mathematical functions.+ .+ This package provides:+ .+ * Prelude library containing datatypes and functions for circuit design+Homepage: http://christiaanb.github.io/clash2/ bug-reports: http://github.com/christiaanb/clash-prelude/issues License: BSD3 License-file: LICENSE@@ -13,6 +23,7 @@ Build-type: Simple Extra-source-files: README.md+ CHANGELOG.md Cabal-version: >=1.10 @@ -28,6 +39,7 @@ Exposed-modules: CLaSH.Bit CLaSH.Class.BitVector+ CLaSH.Class.Num CLaSH.Prelude CLaSH.Promoted.Bool CLaSH.Promoted.Nat@@ -35,6 +47,7 @@ CLaSH.Promoted.Nat.Literals CLaSH.Promoted.Ord CLaSH.Signal+ CLaSH.Sized.Fixed CLaSH.Sized.Signed CLaSH.Sized.Unsigned CLaSH.Sized.Vector
+ src/CLaSH/Class/Num.hs view
@@ -0,0 +1,14 @@+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE TypeFamilies #-}+module CLaSH.Class.Num where++class Add a b where+ type AResult a b+ plus :: a -> b -> AResult a b+ minus :: a -> b -> AResult a b++class Mult a b where+ type MResult a b+ mult :: a -> b -> MResult a b
src/CLaSH/Prelude.hs view
@@ -7,17 +7,23 @@ {-# OPTIONS_GHC -O0 -fno-omit-interface-pragmas #-} module CLaSH.Prelude- ( module Exported- , (<^>)+ ( -- * Creating synchronous sequential circuits+ (<^>) , registerP+ -- * 'Arrow' interface for synchronous sequential circuits , Comp (..)+ , (^^^) , registerC , simulateC- , (^^^)+ -- * BlockRAM primitives , blockRam , blockRamPow2+ , blockRamC+ , blockRamPow2C+ -- * Utility functions , window , windowD+ , module Exported ) where @@ -27,11 +33,13 @@ import Data.Bits as Exported import Data.Default as Exported import CLaSH.Class.BitVector as Exported+import CLaSH.Class.Num as Exported import CLaSH.Promoted.Bool as Exported import CLaSH.Promoted.Nat as Exported import CLaSH.Promoted.Nat.TH as Exported import CLaSH.Promoted.Nat.Literals as Exported import CLaSH.Promoted.Ord as Exported+import CLaSH.Sized.Fixed as Exported import CLaSH.Sized.Signed as Exported import CLaSH.Sized.Unsigned as Exported import CLaSH.Sized.Vector as Exported@@ -45,7 +53,7 @@ -- > window4 :: Signal Int -> Vec 4 (Signal Int) -- > window4 = window -- >--- > simulateP window4 [1,2,3,4,5,... = [<1,0,0,0>,<2,1,0,0>,<3,2,1,0>,<4,3,2,1>,<5,4,3,2>,...+-- > simulateP window4 [1,2,3,4,5,... == [1:>0:>0:>0:>Nil, 2:>1:>0:>0:>Nil, 3:>2:>1:>0:>Nil, 4:>3:>2:>1:>Nil, 5:>4:>3:>2:>Nil,... window :: (KnownNat (n + 1), Default a) => Signal a -> Vec ((n + 1) + 1) (Signal a)@@ -60,7 +68,7 @@ -- > windowD3 :: Signal Int -> Vec 3 (Signal Int) -- > windowD3 = windowD -- >--- > simulateP windowD3 [1,2,3,4,... = [<0,0,0>,<1,0,0>,<2,1,0>,<3,2,1>,<4,3,2>,...+-- > simulateP windowD3 [1,2,3,4,... == [0:>0:>0:>Nil, 1:>0:>0:>Nil, 2:>1:>0:>Nil, 3:>2:>1:>Nil, 4:>3:>2:>Nil,... windowD :: (KnownNat (n + 1), Default a) => Signal a -> Vec (n + 1) (Signal a)@@ -73,6 +81,9 @@ -- | Create a synchronous function from a combinational function describing -- a mealy machine --+-- > mac :: Int -- Current state+-- > -> (Int,Int) -- Input+-- > -> (Int,Int) -- (Updated state, output) -- > mac s (x,y) = (s',s) -- > where -- > s' = x * y + s@@ -80,11 +91,21 @@ -- > topEntity :: (Signal Int, Signal Int) -> Signal Int -- > topEntity = mac <^> 0 -- >--- > simulateP topEntity [(1,1),(2,2),(3,3),(4,4),... = [0,1,5,14,30,...+-- > simulateP topEntity [(1,1),(2,2),(3,3),(4,4),... == [0,1,5,14,30,...+--+-- Synchronous sequential functions can be composed just like their combinational counterpart:+--+-- > dualMac :: (Signal Int, Signal Int)+-- > -> (Signal Int, Signal Int)+-- > -> Signal Int+-- > dualMac (a,b) (x,y) = s1 + s2+-- > where+-- > s1 = (mac <^> 0) (a,b)+-- > s2 = (mac <^> 0) (x,y) (<^>) :: (Pack i, Pack o)- => (s -> i -> (s,o)) -- ^ Transfer function in mealy machine form- -> s -- ^ Initial state- -> (SignalP i -> SignalP o) -- ^ Synchronous function with input and output matching that of the mealy machine+ => (s -> i -> (s,o)) -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@+ -> s -- ^ Initial state+ -> (SignalP i -> SignalP o) -- ^ Synchronous sequential function with input and output matching that of the mealy machine f <^> iS = \i -> let (s',o) = unpack $ f <$> s <*> (pack i) s = register iS s' in unpack o@@ -95,7 +116,7 @@ -- > rP :: (Signal Int,Signal Int) -> (Signal Int, Signal Int) -- > rP = registerP (8,8) -- >--- > simulateP rP [(1,1),(2,2),(3,3),... = [(8,8),(1,1),(2,2),(3,3),...+-- > simulateP rP [(1,1),(2,2),(3,3),... == [(8,8),(1,1),(2,2),(3,3),... registerP :: Pack a => a -> SignalP a -> SignalP a registerP i = unpack Prelude.. register i Prelude.. pack @@ -105,12 +126,12 @@ -- > bram40 :: Signal (Unsigned 6) -> Signal (Unsigned 6) -> Signal Bool -> Signal a -> Signal a -- > bram40 = blockRam d50 blockRam :: forall n m a . (KnownNat n, KnownNat m, Pack a)- => SNat n -- ^ Size @n@ of the blockram+ => SNat n -- ^ Size @n@ of the blockram -> Signal (Unsigned m) -- ^ Write address @w@ -> Signal (Unsigned m) -- ^ Read address @r@- -> Signal Bool -- ^ Write enable- -> Signal a -- ^ Value to write (at address @w@)- -> Signal a -- ^ Value of the 'blockRAM' at address @r@ from the previous clock cycle+ -> Signal Bool -- ^ Write enable+ -> Signal a -- ^ Value to write (at address @w@)+ -> Signal a -- ^ Value of the 'blockRAM' at address @r@ from the previous clock cycle blockRam n wr rd en din = pack $ (bram' <^> binit) (wr,rd,en,din) where binit :: (Vec n a,a)@@ -124,21 +145,39 @@ | otherwise = ram o' = ram ! r +-- | Create a blockRAM with space for @n@ elements+--+-- > bramC40 :: Comp (Unsigned 6, Unsigned 6, Bool, a) a+-- > bramC40 = blockRamC d50+blockRamC :: (KnownNat n, KnownNat m, Pack a)+ => SNat n -- ^ Size @n@ of the blockram+ -> Comp (Unsigned m, Unsigned m, Bool, a) a+blockRamC n = C ((\(wr,rd,en,din) -> blockRam n wr rd en din) Prelude.. unpack)+ {-# INLINABLE blockRamPow2 #-} -- | Create a blockRAM with space for 2^@n@ elements -- -- > bram32 :: Signal (Unsigned 5) -> Signal (Unsigned 5) -> Signal Bool -> Signal a -> Signal a -- > bram32 = blockRamPow2 d32 blockRamPow2 :: (KnownNat n, KnownNat (2^n), Pack a)- => (SNat ((2^n) :: Nat)) -- ^ Size 2^@n@ of the blockram+ => SNat ((2^n) :: Nat) -- ^ Size @2^n@ of the blockram -> Signal (Unsigned n) -- ^ Write address @w@ -> Signal (Unsigned n) -- ^ Read address @r@- -> Signal Bool -- ^ Write enable- -> Signal a -- ^ Value to write (at address @w@)- -> Signal a -- ^ Value of the 'blockRAM' at address @r@ from the previous clock cycle+ -> Signal Bool -- ^ Write enable+ -> Signal a -- ^ Value to write (at address @w@)+ -> Signal a -- ^ Value of the 'blockRAM' at address @r@ from the previous clock cycle blockRamPow2 = blockRam --- | 'Arrow' interface to synchronous functions+-- | Create a blockRAM with space for 2^@n@ elements+--+-- > bramC32 :: Comp (Unsigned 5, Unsigned 5, Bool, a) a+-- > bramC32 = blockRamPow2C d32+blockRamPow2C :: (KnownNat n, KnownNat (2^n), Pack a)+ => SNat ((2^n) :: Nat) -- ^ Size @2^n@ of the blockram+ -> Comp (Unsigned n, Unsigned n, Bool, a) a+blockRamPow2C n = C ((\(wr,rd,en,din) -> blockRamPow2 n wr rd en din) Prelude.. unpack)++-- | 'Comp'onent: an 'Arrow' interface to synchronous sequential functions newtype Comp a b = C { asFunction :: Signal a -> Signal b } instance Category Comp where@@ -164,13 +203,13 @@ -- > rC :: Comp (Int,Int) (Int,Int) -- > rC = registerC (8,8) -- >--- > simulateC rP [(1,1),(2,2),(3,3),... = [(8,8),(1,1),(2,2),(3,3),...+-- > simulateC rP [(1,1),(2,2),(3,3),... == [(8,8),(1,1),(2,2),(3,3),... registerC :: a -> Comp a a registerC = C Prelude.. register -- | Simulate a 'Comp'onent given a list of samples ----- > simulateC (registerC 8) [1, 2, 3, ... = [8, 1, 2, 3, ...+-- > simulateC (registerC 8) [1, 2, 3, ... == [8, 1, 2, 3, ... simulateC :: Comp a b -> [a] -> [b] simulateC f = simulate (asFunction f) @@ -178,6 +217,9 @@ -- | Create a synchronous 'Comp'onent from a combinational function describing -- a mealy machine --+-- > mac :: Int -- Current state+-- > -> (Int,Int) -- Input+-- > -> (Int,Int) -- (Updated state, output) -- > mac s (x,y) = (s',s) -- > where -- > s' = x * y + s@@ -185,8 +227,18 @@ -- > topEntity :: Comp (Int,Int) Int -- > topEntity = mac ^^^ 0 -- >--- > simulateC topEntity [(1,1),(2,2),(3,3),(4,4),... = [0,1,5,14,30,...-(^^^) :: (s -> i -> (s,o)) -> s -> Comp i o+-- > simulateC topEntity [(1,1),(2,2),(3,3),(4,4),... == [0,1,5,14,30,...+--+-- Synchronous sequential must be composed using the 'Arrow' syntax+--+-- > dualMac :: Comp (Int,Int,Int,Int) Int+-- > dualMac = proc (a,b,x,y) -> do+-- > rec s1 <- mac ^^^ 0 -< (a,b)+-- > s2 <- mac ^^^ 0 -< (x,y)+-- > returnA -< (s1 + s2)+(^^^) :: (s -> i -> (s,o)) -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@+ -> s -- ^ Initial state+ -> Comp i o -- ^ Synchronous sequential 'Comp'onent with input and output matching that of the mealy machine f ^^^ sI = C $ \i -> let (s',o) = unpack $ f <$> s <*> i s = register sI s' in o
src/CLaSH/Promoted/Nat.hs view
@@ -4,7 +4,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} module CLaSH.Promoted.Nat- ( SNat, snat, withSNat, fromSNat+ ( SNat, snat, withSNat , UNat (..), toUNat, addUNat, multUNat, powUNat ) where@@ -29,11 +29,6 @@ UZero :: UNat 0 USucc :: UNat n -> UNat (n + 1) --- | Convert a singleton natural number to an integer-fromSNat :: SNat n -> Integer-fromSNat (SNat p) = natVal p--{-# NOINLINE fromSNat #-} -- | Convert a singleton natural number to it's unary representation toUNat :: SNat n -> UNat n toUNat (SNat p) = fromI (natVal p)
src/CLaSH/Signal.hs view
@@ -39,7 +39,7 @@ -- Every element in the list will correspond to a value of the signal for one -- clock cycle. ----- > sampleN 2 (fromList [1,2,3,4,5]) = [1,2]+-- > sampleN 2 (fromList [1,2,3,4,5]) == [1,2] fromList :: [a] -> Signal a fromList [] = error "finite list" fromList (x:xs) = x :- fromList xs@@ -58,7 +58,7 @@ -- The elements in the list correspond to the values of the 'Signal' at -- consecutive clock cycles ----- > sample s = [s0, s1, s2, s3, ...+-- > sample s == [s0, s1, s2, s3, ... sample :: Signal a -> [a] sample ~(x :- xs) = x : sample xs @@ -67,14 +67,14 @@ -- The elements in the list correspond to the values of the 'Signal' at -- consecutive clock cycles ----- > sampleN 3 s = [s0, s1, s2]+-- > sampleN 3 s == [s0, s1, s2] sampleN :: Int -> Signal a -> [a] sampleN 0 _ = [] sampleN n ~(x :- xs) = x : (sampleN (n-1) xs) -- | Create a constant 'Signal' from a combinational value ----- > sample (signal 4) = [4, 4, 4, 4, ...+-- > sample (signal 4) == [4, 4, 4, 4, ... signal :: a -> Signal a signal a = a :- signal a @@ -107,13 +107,13 @@ -- | 'register' @i s@ delays the values in 'Signal' @s@ for one cycle, and sets -- the value at time 0 to @i@ ----- > sampleN 3 (register 8 (fromList [1,2,3,4])) = [8,1,2]+-- > sampleN 3 (register 8 (fromList [1,2,3,4])) == [8,1,2] register :: a -> Signal a -> Signal a register i s = i :- s -- | Simulate a ('Signal' -> 'Signal') function given a list of samples ----- > simulate (register 8) [1, 2, 3, ... = [8, 1, 2, 3, ...+-- > simulate (register 8) [1, 2, 3, ... == [8, 1, 2, 3, ... simulate :: (Signal a -> Signal b) -> [a] -> [b] simulate f = sample . f . fromList @@ -134,7 +134,7 @@ -- | Simulate a ('SignalP' -> 'SignalP') function given a list of samples ----- > simulateP (unpack . register (8,8) . pack) [(1,1), (2,2), (3,3), ... = [(8,8), (1,1), (2,2), (3,3), ...+-- > simulateP (unpack . register (8,8) . pack) [(1,1), (2,2), (3,3), ... == [(8,8), (1,1), (2,2), (3,3), ... simulateP :: (Pack a, Pack b) => (SignalP a -> SignalP b) -> [a] -> [b] simulateP f = simulate (pack . f . unpack) @@ -263,7 +263,7 @@ -- > add2 :: Signal Int -> Signal Int -- > add2 x = x <^(+)^> (signal 2) -- >--- > simulate add2 [1,2,3, = [3,4,5,...+-- > simulate add2 [1,2,3,... == [3,4,5,... (<^) :: Applicative f => f a -> (a -> b -> c) -> f b -> f c v <^ f = liftA2 f v @@ -272,7 +272,7 @@ -- > add2 :: Signal Int -> Signal Int -- > add2 x = x <^(+)^> (signal 2) -- >--- > simulate add2 [1,2,3, = [3,4,5,...+-- > simulate add2 [1,2,3,... == [3,4,5,... (^>) :: Applicative f => (f a -> f b) -> f a -> f b f ^> v = f v
+ src/CLaSH/Sized/Fixed.hs view
@@ -0,0 +1,157 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+module CLaSH.Sized.Fixed+ ( -- * Signed fixed point+ SFixed, sf, unSF+ -- * Unsigned fixed point+ , UFixed, uf, unUF+ )+where++import Control.Arrow+import Data.Bits+import Data.Default+import Data.Function+import Data.List+import Data.Maybe+import Data.Proxy+import Data.Ratio+import GHC.TypeLits+import Language.Haskell.TH+import Language.Haskell.TH.Syntax(Lift(..))++import CLaSH.Class.BitVector+import CLaSH.Class.Num+import CLaSH.Signal+import CLaSH.Sized.Signed+import CLaSH.Sized.Unsigned++-- | Fixed point signed integer with @i@ integer bits and @f@ fractional bits+--+-- For now, overflow behaviour for the 'Num' functions is wrap-around, not saturate+newtype SFixed (i :: Nat) (f :: Nat) = SF { unSF :: Signed (i + f) }+ deriving (Eq,Ord)++-- | Fixed point unsigned integer with @i@ integer bits and @f@ fractional bits+--+-- For now, overflow behaviour for the 'Num' functions is wrap-around, not saturate+newtype UFixed (i :: Nat) (f :: Nat) = UF { unUF :: Unsigned (i + f) }+ deriving (Eq,Ord)++fracShift :: KnownNat n => proxy n -> Int+fracShift = fromInteger . natVal++sf :: Signed (i + f) -> SFixed i f+sf = SF++uf :: Unsigned (i + f) -> UFixed i f+uf = UF++showFixed :: (Bits a, KnownNat n, Show a, Integral a) =>+ (proxy n -> a) -> proxy n -> [Char]+showFixed unRep f = show i ++ "." ++ (uncurry pad . second (show . numerator) .+ fromJust . find ((==1) . denominator . snd) .+ iterate (succ *** (*10)) . (,) 0 $ (nom % denom))+ where+ pad n str = replicate (n - length str) '0' ++ str+ nF = fracShift f+ rep = unRep f+ i = rep `shiftR` nF+ nom = toInteger rep .&. ((2 ^ nF) - 1)+ denom = 2 ^ nF++instance (KnownNat (i + f), KnownNat f) => Show (SFixed i f) where+ show = showFixed unSF++instance (KnownNat (i + f), KnownNat f) => Show (UFixed i f) where+ show = showFixed unUF++multFixedS :: (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f)+ => SFixed i f -> SFixed i f -> SFixed i f+multFixedS (SF a) (SF b) = res+ where+ resM = mult a b+ resS = resM `shiftR` (fracShift res)+ res = SF (resizeS resS)++multFixedU :: (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f)+ => UFixed i f -> UFixed i f -> UFixed i f+multFixedU (UF a) (UF b) = res+ where+ resM = mult a b+ resS = resM `shiftR` (fracShift res)+ res = UF (resizeU resS)++fixedFromInteger :: (Bits a, KnownNat n, Num a)+ => (a -> proxy n) -> Integer -> proxy n+fixedFromInteger toF i = res+ where+ res = toF (fromInteger i `shiftL` fracShift res)++instance (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f) => Num (SFixed i f) where+ (+) = (SF .) . on (+) unSF+ (*) = multFixedS+ (-) = (SF .) . on (-) unSF+ negate = SF . negate . unSF+ abs = SF . abs . unSF+ signum = SF . signum . unSF+ fromInteger = fixedFromInteger SF++instance (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f) => Num (UFixed i f) where+ (+) = (UF .) . on (+) unUF+ (*) = multFixedU+ (-) = (UF .) . on (-) unUF+ negate = UF . negate . unUF+ abs = UF . abs . unUF+ signum = UF . signum . unUF+ fromInteger = fixedFromInteger UF++instance BitVector (SFixed i f) where+ type BitSize (SFixed i f) = i + f+ toBV (SF s) = toBV s+ fromBV bv = SF (fromBV bv)++instance BitVector (UFixed i f) where+ type BitSize (UFixed i f) = i + f+ toBV (UF s) = toBV s+ fromBV bv = UF (fromBV bv)++instance Pack (SFixed i f) where+ type SignalP (SFixed i f) = Signal (SFixed i f)+ pack = id+ unpack = id++instance Pack (UFixed i f) where+ type SignalP (UFixed i f) = Signal (UFixed i f)+ pack = id+ unpack = id++instance (KnownNat i, KnownNat f, KnownNat (i + f)) => Lift (SFixed i f) where+ lift s@(SF i) = sigE [| SF i |] (decSFixed (natVal (asProxy s)) (natVal s))+ where+ asProxy :: SFixed n a -> Proxy n+ asProxy _ = Proxy++instance (KnownNat i, KnownNat f, KnownNat (i + f)) => Lift (UFixed i f) where+ lift s@(UF i) = sigE [| UF i |] (decUFixed (natVal (asProxy s)) (natVal s))+ where+ asProxy :: UFixed n a -> Proxy n+ asProxy _ = Proxy++decSFixed :: Integer -> Integer -> TypeQ+decSFixed i f = appT (appT (conT ''SFixed) (litT $ numTyLit i)) (litT $ numTyLit f)++decUFixed :: Integer -> Integer -> TypeQ+decUFixed i f = appT (appT (conT ''SFixed) (litT $ numTyLit i)) (litT $ numTyLit f)++instance KnownNat (i + f) => Default (SFixed i f) where+ def = SF 0++instance KnownNat (i + f) => Default (UFixed i f) where+ def = UF 0
src/CLaSH/Sized/Signed.hs view
@@ -1,10 +1,10 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fno-warn-missing-methods #-} @@ -23,9 +23,11 @@ import CLaSH.Bit import CLaSH.Class.BitVector-import CLaSH.Promoted.Nat+import CLaSH.Class.Num+import CLaSH.Promoted.Ord import CLaSH.Sized.Vector +-- | Arbitrary-width signed integer represented by @n@ bits newtype Signed (n :: Nat) = S Integer instance Eq (Signed n) where@@ -61,11 +63,11 @@ minBound = minBoundS maxBound = maxBoundS -minBoundS,maxBoundS :: forall n . KnownNat n => Signed n+minBoundS,maxBoundS :: KnownNat n => Signed n {-# NOINLINE minBoundS #-}-minBoundS = S $ negate $ 2 ^ (fromSNat (snat :: SNat n) -1)+minBoundS = let res = S $ negate $ 2 ^ (natVal res - 1) in res {-# NOINLINE maxBoundS #-}-maxBoundS = S $ 2 ^ (fromSNat (snat :: SNat n) - 1) - 1+maxBoundS = let res = S $ 2 ^ (natVal res - 1) - 1 in res instance KnownNat n => Num (Signed n) where (+) = plusS@@ -78,13 +80,13 @@ plusS,minS,timesS :: KnownNat n => Signed n -> Signed n -> Signed n {-# NOINLINE plusS #-}-plusS (S a) (S b) = fromIntegerS_inlineable $ a + b+plusS (S a) (S b) = fromIntegerS_inlineable (a + b) {-# NOINLINE minS #-}-minS (S a) (S b) = fromIntegerS_inlineable $ a - b+minS (S a) (S b) = fromIntegerS_inlineable (a - b) {-# NOINLINE timesS #-}-timesS (S a) (S b) = fromIntegerS_inlineable $ a * b+timesS (S a) (S b) = fromIntegerS_inlineable (a * b) negateS,absS,signumS :: KnownNat n => Signed n -> Signed n {-# NOINLINE negateS #-}@@ -96,7 +98,7 @@ {-# NOINLINE signumS #-} signumS (S n) = fromIntegerS_inlineable (signum n) -fromIntegerS,fromIntegerS_inlineable :: forall n . KnownNat n => Integer -> Signed (n :: Nat)+fromIntegerS,fromIntegerS_inlineable :: KnownNat n => Integer -> Signed (n :: Nat) {-# NOINLINE fromIntegerS #-} fromIntegerS = fromIntegerS_inlineable {-# INLINABLE fromIntegerS_inlineable #-}@@ -104,12 +106,32 @@ | nS == 0 = S 0 | otherwise = res where- nS = fromSNat (snat :: SNat n)+ nS = natVal res sz = 2 ^ (nS - 1) res = case divMod i sz of (s,i') | even s -> S i' | otherwise -> S (i' - sz) +instance KnownNat (Max m n) => Add (Signed m) (Signed n) where+ type AResult (Signed m) (Signed n) = Signed (Max m n)+ plus = plusS2+ minus = minusS2++plusS2, minusS2 :: KnownNat (Max m n) => Signed m -> Signed n -> Signed (Max m n)+{-# NOINLINE plusS2 #-}+plusS2 (S a) (S b) = fromIntegerS_inlineable (a + b)++{-# NOINLINE minusS2 #-}+minusS2 (S a) (S b) = fromIntegerS_inlineable (a - b)++instance KnownNat (m + n) => Mult (Signed m) (Signed n) where+ type MResult (Signed m) (Signed n) = Signed (m + n)+ mult = multS2++{-# NOINLINE multS2 #-}+multS2 :: KnownNat (m + n) => Signed m -> Signed n -> Signed (m + n)+multS2 (S a) (S b) = fromIntegerS_inlineable (a * b)+ instance KnownNat n => Real (Signed n) where toRational = toRational . toIntegerS @@ -177,11 +199,29 @@ {-# NOINLINE bitS #-} bitS :: KnownNat n => Int -> Signed n-bitS = fromIntegerS_inlineable . bit+bitS i = res+ where+ sz = finiteBitSizeS res+ res | sz > i = fromIntegerS_inlineable (bit i)+ | otherwise = error $ concat [ "bit: "+ , "Setting out-of-range bit position, size: "+ , show sz+ , ", position: "+ , show i+ ] {-# NOINLINE testBitS #-}-testBitS :: Signed n -> Int -> Bool-testBitS (S n) i = testBit n i+testBitS :: KnownNat n => Signed n -> Int -> Bool+testBitS s@(S n) i+ | sz > i = testBit n i+ | otherwise = error $ concat [ "testBit: "+ , "Setting out-of-range bit position, size: "+ , show sz+ , ", position: "+ , show i+ ]+ where+ sz = finiteBitSizeS s shiftLS,shiftRS,rotateLS,rotateRS :: KnownNat n => Signed n -> Int -> Signed n {-# NOINLINE shiftLS #-}@@ -207,8 +247,8 @@ finiteBitSize = finiteBitSizeS {-# NOINLINE finiteBitSizeS #-}-finiteBitSizeS :: forall n . KnownNat n => Signed n -> Int-finiteBitSizeS _ = fromInteger $ fromSNat (snat :: SNat n)+finiteBitSizeS :: KnownNat n => Signed n -> Int+finiteBitSizeS i = let res = fromInteger (natVal i) in res instance Show (Signed n) where show (S n) = show n@@ -217,7 +257,7 @@ def = fromIntegerS 0 instance KnownNat n => Lift (Signed n) where- lift (S i) = sigE [| fromIntegerS i |] (decSigned $ fromSNat (snat :: (SNat n)))+ lift s@(S i) = sigE [| fromIntegerS i |] (decSigned (natVal s)) decSigned :: Integer -> TypeQ decSigned n = appT (conT ''Signed) (litT $ numTyLit n)@@ -249,15 +289,16 @@ -- Increasing the size of the number replicates the sign bit to the left. -- Truncating a number to length L keeps the sign bit and the rightmost L-1 bits. ---resizeS :: forall n m . (KnownNat n, KnownNat m) => Signed n -> Signed m-resizeS s@(S n) | n' <= m' = fromIntegerS_inlineable n- | otherwise = case l of+resizeS :: (KnownNat n, KnownNat m) => Signed n -> Signed m+resizeS s@(S n) | n' <= m' = extend+ | otherwise = trunc+ where+ n' = fromInteger (natVal s)+ m' = fromInteger (natVal extend)+ extend = fromIntegerS_inlineable n+ trunc = case toList (toBitVector s) of (x:xs) -> fromBitList $ reverse $ x : (drop (n' - m') xs) _ -> error "resizeS impossible case: empty list"- where- n' = fromInteger $ fromSNat (snat :: SNat n) :: Int- m' = fromInteger $ fromSNat (snat :: SNat m) :: Int- l = toList $ toBitVector s {-# NOINLINE resizeS_wrap #-} -- | A resize operation that is sign-preserving on extension, but wraps on truncation.
src/CLaSH/Sized/Unsigned.hs view
@@ -1,10 +1,10 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fno-warn-missing-methods #-} @@ -22,9 +22,11 @@ import CLaSH.Bit import CLaSH.Class.BitVector-import CLaSH.Promoted.Nat+import CLaSH.Class.Num+import CLaSH.Promoted.Ord import CLaSH.Sized.Vector +-- | Arbitrary-width unsigned integer represented by @n@ bits newtype Unsigned (n :: Nat) = U Integer instance Eq (Unsigned n) where@@ -61,8 +63,8 @@ maxBound = maxBoundU {-# NOINLINE maxBoundU #-}-maxBoundU :: forall n . KnownNat n => Unsigned n-maxBoundU = U $ (2 ^ fromSNat (snat :: SNat n)) - 1+maxBoundU :: KnownNat n => Unsigned n+maxBoundU = let res = U ((2 ^ natVal res) - 1) in res instance KnownNat n => Num (Unsigned n) where (+) = plusU@@ -88,12 +90,32 @@ signumU (U 0) = (U 0) signumU (U _) = (U 1) -fromIntegerU,fromIntegerU_inlineable :: forall n . KnownNat n => Integer -> Unsigned (n :: Nat)+fromIntegerU,fromIntegerU_inlineable :: KnownNat n => Integer -> Unsigned n {-# NOINLINE fromIntegerU #-} fromIntegerU = fromIntegerU_inlineable {-# INLINABLE fromIntegerU_inlineable #-}-fromIntegerU_inlineable i = U $ i `mod` (2 ^ fromSNat (snat :: SNat n))+fromIntegerU_inlineable i = let res = U (i `mod` (2 ^ natVal res)) in res +instance KnownNat (Max m n) => Add (Unsigned m) (Unsigned n) where+ type AResult (Unsigned m) (Unsigned n) = Unsigned (Max m n)+ plus = plusU2+ minus = minusU2++plusU2, minusU2 :: KnownNat (Max m n) => Unsigned m -> Unsigned n -> Unsigned (Max m n)+{-# NOINLINE plusU2 #-}+plusU2 (U a) (U b) = fromIntegerU_inlineable (a + b)++{-# NOINLINE minusU2 #-}+minusU2 (U a) (U b) = fromIntegerU_inlineable (a - b)++instance KnownNat (m + n) => Mult (Unsigned m) (Unsigned n) where+ type MResult (Unsigned m) (Unsigned n) = Unsigned (m + n)+ mult = multU2++{-# NOINLINE multU2 #-}+multU2 :: KnownNat (m + n) => Unsigned m -> Unsigned n -> Unsigned (m + n)+multU2 (U a) (U b) = fromIntegerU_inlineable (a * b)+ instance KnownNat n => Real (Unsigned n) where toRational = toRational . toIntegerU @@ -156,11 +178,29 @@ {-# NOINLINE bitU #-} bitU :: KnownNat n => Int -> Unsigned n-bitU = fromIntegerU_inlineable . bit+bitU i = res+ where+ sz = finiteBitSizeU res+ res | sz > i = fromIntegerU_inlineable (bit i)+ | otherwise = error $ concat [ "bit: "+ , "Setting out-of-range bit position, size: "+ , show sz+ , ", position: "+ , show i+ ] {-# NOINLINE testBitU #-}-testBitU :: Unsigned n -> Int -> Bool-testBitU (U n) i = testBit n i+testBitU :: KnownNat n => Unsigned n -> Int -> Bool+testBitU s@(U n) i+ | sz > i = testBit n i+ | otherwise = error $ concat [ "testBit: "+ , "Setting out-of-range bit position, size: "+ , show sz+ , ", position: "+ , show i+ ]+ where+ sz = finiteBitSizeU s shiftLU,shiftRU,rotateLU,rotateRU :: KnownNat n => Unsigned n -> Int -> Unsigned n {-# NOINLINE shiftLU #-}@@ -186,11 +226,11 @@ finiteBitSize = finiteBitSizeU {-# NOINLINE finiteBitSizeU #-}-finiteBitSizeU :: forall n . KnownNat n => Unsigned n -> Int-finiteBitSizeU _ = fromInteger $ fromSNat (snat :: SNat n)+finiteBitSizeU :: KnownNat n => Unsigned n -> Int+finiteBitSizeU u = fromInteger (natVal u) -instance forall n . KnownNat n => Lift (Unsigned n) where- lift (U i) = sigE [| fromIntegerU i |] (decUnsigned $ fromSNat (snat :: (SNat n)))+instance KnownNat n => Lift (Unsigned n) where+ lift u@(U i) = sigE [| fromIntegerU i |] (decUnsigned (natVal u)) decUnsigned :: Integer -> TypeQ decUnsigned n = appT (conT ''Unsigned) (litT $ numTyLit n)
src/CLaSH/Sized/Vector.hs view
@@ -1,5 +1,4 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}@@ -18,20 +17,21 @@ , vreverse, vmap, vzipWith , vfoldr, vfoldl, vfoldr1, vfoldl1 , vzip, vunzip- , (!), vreplace, maxIndex+ , (!), vreplace, maxIndex, vlength , vtake, vtakeI, vdrop, vdropI, vexact, vselect, vselectI , vcopy, vcopyI, viterate, viterateI, vgenerate, vgenerateI- , toList, v+ , toList, v, lazyV, asNatProxy ) where import Control.Applicative import Data.Traversable-import Data.Foldable hiding (toList)+import Data.Foldable hiding (toList)+import Data.Proxy import GHC.TypeLits-import Language.Haskell.TH (ExpQ)+import Language.Haskell.TH (ExpQ) import Language.Haskell.TH.Syntax (Lift(..))-import Unsafe.Coerce (unsafeCoerce)+import Unsafe.Coerce (unsafeCoerce) import CLaSH.Promoted.Nat @@ -68,22 +68,34 @@ {-# NOINLINE vhead #-} -- | Extract the first element of a vector+--+-- > vhead (1:>2:>3:>Nil) == 1+-- > vhead Nil == TYPE ERROR vhead :: Vec (n + 1) a -> a vhead (x :> _) = x {-# NOINLINE vtail #-} -- | Extract the elements after the head of a vector+--+-- > vtail (1:>2:>3:>Nil) == (2:>3:>Nil)+-- > vtail Nil == TYPE ERROR vtail :: Vec (n + 1) a -> Vec n a vtail (_ :> xs) = unsafeCoerce xs {-# NOINLINE vlast #-} -- | Extract the last element of a vector+--+-- > vlast (1:>2:>3:>Nil) == 3+-- > vlast Nil == TYPE ERROR vlast :: Vec (n + 1) a -> a vlast (x :> Nil) = x vlast (_ :> y :> ys) = vlast (y :> ys) {-# NOINLINE vinit #-} -- | Extract all the elements of a vector except the last element+--+-- > vinit (1:>2:>3:>Nil) == (1:>2:>Nil)+-- > vinit Nil == TYPE ERROR vinit :: Vec (n + 1) a -> Vec n a vinit (_ :> Nil) = unsafeCoerce Nil vinit (x :> y :> ys) = unsafeCoerce (x :> vinit (y :> ys))@@ -99,6 +111,9 @@ {-# INLINEABLE (+>>) #-} -- | Add an element to the head of the vector, and extract all elements of the -- resulting vector except the last element+--+-- > 1 +>> (3:>4:>5:>Nil) == (1:>3:>4:>Nil)+-- > 1 +>> Nil == Nil (+>>) :: a -> Vec n a -> Vec n a s +>> xs = shiftIntoL s xs @@ -111,6 +126,9 @@ infixl 5 <: {-# INLINEABLE (<:) #-} -- | Add an element to the tail of the vector+--+-- > (3:>4:>5:>Nil) <: 1 == (3:>4:>5:>1:>Nil)+-- > Nil <: 1 == (1:>Nil) (<:) :: Vec n a -> a -> Vec (n + 1) a xs <: s = snoc s xs @@ -125,6 +143,9 @@ {-# INLINE (<<+) #-} -- | Add an element to the tail of the vector, and extract all elements of the -- resulting vector except the first element+--+-- > (3:>4:>5:>Nil) <<+ 1 == (4:>5:>1:>Nil)+-- > Nil <<+ 1 == Nil (<<+) :: Vec n a -> a -> Vec n a xs <<+ s = shiftIntoR s xs @@ -137,11 +158,16 @@ infixr 5 <++> {-# INLINE (<++>) #-} -- | Append two vectors+--+-- > (1:>2:>3:>Nil) <++> (7:>8:>Nil) = (1:>2:>3:>7:>8:>Nil) (<++>) :: Vec n a -> Vec m a -> Vec (n + m) a xs <++> ys = vappend xs ys {-# NOINLINE vsplit #-} -- | Split a vector into two vectors at the given point+--+-- > vsplit (snat :: SNat 3) (1:>2:>3:>7:>8:>Nil) == (1:>2:>3:>Nil, 7:>8:>Nil)+-- > vsplit d3 (1:>2:>3:>7:>8:>Nil) == (1:>2:>3:>Nil, 7:>8:>Nil) vsplit :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a) vsplit n xs = vsplitU (toUNat n) xs @@ -158,6 +184,12 @@ {-# NOINLINE vconcat #-} -- | Concatenate a vector of vectors+--+-- > vunconcat ((1:>2:>3:>Nil) :>+-- > (4:>5:>6:>Nil) :>+-- > (7:>8:>9:>Nil) :>+-- > (10:>11:>12:>Nil) :>+-- > Nil) == (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) vconcat :: Vec n (Vec m a) -> Vec (n * m) a vconcat Nil = Nil vconcat (x :> xs) = unsafeCoerce (vappend x (vconcat xs))@@ -165,6 +197,11 @@ {-# NOINLINE vunconcat #-} -- | Split a vector of (n * m) elements into a vector of vectors with length m, -- where m is given+--+-- > vunconcat d4 (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) == ((1:>2:>3:>4:>Nil) :>+-- > (5:>6:>7:>8:>Nil) :>+-- > (9:>10:>11:>12:>Nil) :>+-- > Nil) vunconcat :: KnownNat n => SNat m -> Vec (n * m) a -> Vec n (Vec m a) vunconcat n xs = vunconcatU (withSNat toUNat) (toUNat n) xs @@ -182,7 +219,7 @@ {-# NOINLINE vmerge #-} -- | Merge two vectors, alternating their elements, i.e., ----- > vmerge <xn, ..., x2, x1> <yn, ..., y2, y1> == <xn, yn, ..., x2, y2, x1, y1>+-- > vmerge (xn :> ... :> x2 :> x1 :> Nil) (yn :> ... :> y2 :> y1 :> Nil) == (xn :> yn :> ... :> x2 :> y2 :> x1 :> y1 :> Nil) -- vmerge :: Vec n a -> Vec n a -> Vec (n + n) a vmerge Nil Nil = Nil@@ -198,7 +235,7 @@ -- | 'vmap' @f xs@ is the list obtained by applying @f@ to each element -- of @xs@, i.e., ----- > vmap f <xn, ..., x2, x1> == <f xn, ..., f x2, f x1>+-- > vmap f (xn :> ... :> x2 :> x1 :> Nil) == (f xn :> ... :> f x2 :> f x1 :> Nil) vmap :: (a -> b) -> Vec n a -> Vec n b vmap _ Nil = Nil vmap f (x :> xs) = f x :> vmap f xs@@ -208,6 +245,8 @@ -- as the first argument, instead of a tupling function. -- For example, @'vzipWith' (+)@ is applied to two vectors to produce the -- vector of corresponding sums.+--+-- > vzipWith f (xn :> ... :> x2 :> x1 :> Nil) (yn :> ... :> y2 :> y1 :> Nil) == (f xn yn :> ... :> f x2 y2 :> f x1 y1 :> Nil) vzipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c vzipWith _ Nil Nil = Nil vzipWith f (x :> xs) (y :> ys) = f x y :> (vzipWith f xs (unsafeCoerce ys))@@ -217,7 +256,8 @@ -- the right-identity of the operator), and a vector, reduces the vector -- using the binary operator, from right to left: ----- > foldr f z <xn, ..., x2, x1> == xn `f` (... (x2 `f` (x1 `f` z))...)+-- > vfoldr f z (xn :> ... :> x2 :> x1 :> Nil) == xn `f` (... (x2 `f` (x1 `f` z))...)+-- > vfoldr r z Nil == z vfoldr :: (a -> b -> b) -> b -> Vec n a -> b vfoldr _ z Nil = z vfoldr f z (x :> xs) = f x (vfoldr f z xs)@@ -227,7 +267,8 @@ -- the left-identity of the operator), and a vector, reduces the vector -- using the binary operator, from left to right: ----- > vfoldl f z <xn, ..., x2, x1> == (...((z `f` xn)... `f` x2) `f` x1+-- > vfoldl f z (xn :> ... :> x2 :> x1 :> Nil) == (...((z `f` xn)... `f` x2) `f` x1+-- > vfoldl f z Nil == z vfoldl :: (b -> a -> b) -> b -> Vec n a -> b vfoldl _ z Nil = z vfoldl f z (x :> xs) = vfoldl f (f z x) xs@@ -235,6 +276,10 @@ {-# NOINLINE vfoldr1 #-} -- | 'vfoldr1' is a variant of 'vfoldr' that has no starting value argument, -- and thus must be applied to non-empty vectors.+--+-- > vfoldr1 f (xn :> ... :> x3 :> x2 :> x1 :> Nil) == xn `f` (... (x3 `f` (x2 `f` x1))...)+-- > vfoldr1 f (x1 :> Nil) == x1+-- > vfoldr1 f Nil == TYPE ERROR vfoldr1 :: (a -> a -> a) -> Vec (n + 1) a -> a vfoldr1 _ (x :> Nil) = x vfoldr1 f (x :> (y :> ys)) = f x (vfoldr1 f (y :> ys))@@ -242,11 +287,17 @@ {-# INLINEABLE vfoldl1 #-} -- | 'vfoldl1' is a variant of 'vfoldl' that has no starting value argument, -- and thus must be applied to non-empty vectors.+--+-- > vfoldl f (xn :> xn1 :> ... :> x2 :> x1 :> Nil) == (...((xn `f` xn1)... `f` x2) `f` x1+-- > vfoldl f (x1 :> Nil) == x1+-- > vfoldl f Nil == TYPE ERROR vfoldl1 :: (a -> a -> a) -> Vec (n + 1) a -> a vfoldl1 f xs = vfoldl f (vhead xs) (vtail xs) {-# NOINLINE vzip #-} -- | 'vzip' takes two lists and returns a list of corresponding pairs.+--+-- > vzip (xn :> ... :> x2 :> x1 :> Nil) (yn :> ... :> y2 :> y1 :> Nil) == ((xn,yn) :> ... :> ... (x2,y2) :> (x1,y1) :> Nil) vzip :: Vec n a -> Vec n b -> Vec n (a,b) vzip Nil Nil = Nil vzip (x :> xs) (y :> ys) = (x,y) :> (vzip xs (unsafeCoerce ys))@@ -254,6 +305,8 @@ {-# NOINLINE vunzip #-} -- | 'vunzip' transforms a list of pairs into a list of first components -- and a list of second components.+--+-- > vunzip ((xn,yn) :> ... :> ... (x2,y2) :> (x1,y1) :> Nil) == (xn :> ... :> x2 :> x1 :> Nil, yn :> ... :> y2 :> y1 :> Nil) vunzip :: Vec n (a,b) -> (Vec n a, Vec n b) vunzip Nil = (Nil,Nil) vunzip ((a,b) :> xs) = let (as,bs) = vunzip xs@@ -275,17 +328,27 @@ -- | Vector index (subscript) operator, descending from 'maxIndex', where the -- last element has subscript 0. ----- > <1,2,3,4,5> ! 4 == 1--- > <1,2,3,4,5> ! maxIndex == 1--- > <1,2,3,4,5> ! 1 == 4+-- > (1:>2:>3:>4:>5:>Nil) ! 4 == 1+-- > (1:>2:>3:>4:>5:>Nil) ! maxIndex == 1+-- > (1:>2:>3:>4:>5:>Nil) ! 1 == 4+-- > (1:>2:>3:>4:>5:>Nil) ! 14 == RUNTIME ERROR: Out of bounds (!) :: (KnownNat n, Integral i) => Vec n a -> i -> a xs ! i = vindex_integer xs (toInteger i) {-# NOINLINE maxIndex #-}--- | Index (subscript) of the head of the vector-maxIndex :: forall n a . KnownNat n => Vec n a -> Integer-maxIndex _ = fromSNat (snat :: SNat n) - 1+-- | Index (subscript) of the head of the 'Vec'tor+--+-- > maxIndex (6 :> 7 :> 8 :> Nil) == 2+maxIndex :: KnownNat n => Vec n a -> Integer+maxIndex = subtract 1 . vlength +{-# NOINLINE vlength #-}+-- | Length of a 'Vec'tor as an Integer+--+-- > vlength (6 :> 7 :> 8 :> Nil) == 3+vlength :: KnownNat n => Vec n a -> Integer+vlength = natVal . asNatProxy+ {-# NOINLINE vreplaceM_integer #-} vreplaceM_integer :: Vec n a -> Integer -> a -> Maybe (Vec n a) vreplaceM_integer Nil _ _ = Nothing@@ -304,17 +367,19 @@ -- | Replace an element of a vector at the given index (subscript), NB: vector -- elements have a descending subscript starting from 'maxIndex' and ending at 0 ----- > vreplace <1,2,3,4,5> 3 7 == <1,7,3,4,5>+-- > vreplace (1:>2:>3:>4:>5:>Nil) 3 7 == (1:>7:>3:>4:>5:>Nil)+-- > vreplace (1:>2:>3:>4:>5:>Nil) 0 7 == (1:>2:>3:>4:>7:>Nil)+-- > vreplace (1:>2:>3:>4:>5:>Nil) 9 7 == RUNTIME ERROR: Out of bounds vreplace :: (KnownNat n, Integral i) => Vec n a -> i -> a -> Vec n a vreplace xs i y = vreplace_integer xs (toInteger i) y {-# NOINLINE vtake #-} -- | 'vtake' @n@, applied to a vector @xs@, returns the @n@-length prefix of @xs@ ----- > vtake (snat :: SNat 3) <1,2,3,4,5> == <1,2,3>--- > vtake d3 <1,2,3,4,5> == <1,2,3>--- > vtake (snat :: SNat 0) <1,2> == <>--- > vtake (snat :: SNat 4) <1,2> == TYPE ERROR+-- > vtake (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil) == (1:>2:>3:>Nil)+-- > vtake d3 (1:>2:>3:>4:>5:>Nil) == (1:>2:>3:>Nil)+-- > vtake d0 (1:>2:>Nil) == Nil+-- > vtake d4 (1:>2:>Nil) == TYPE ERROR vtake :: SNat m -> Vec (m + n) a -> Vec m a vtake n = fst . vsplit n @@ -326,10 +391,10 @@ {-# NOINLINE vdrop #-} -- | 'vdrop' @n xs@ returns the suffix of @xs@ after the first @n@ elements ----- > vdrop (snat :: SNat 3) <1,2,3,4,5> == <4,5>--- > vdrop d3 <1,2,3,4,5> == <4,5>--- > vdrop (snat :: SNat 0) <1,2> == <1,2>--- > vdrop (snat :: SNat 4) <1,2> == TYPE ERROR+-- > vdrop (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil) == (4:>5:>Nil)+-- > vdrop d3 (1:>2:>3:>4:>5:>Nil) == (4:>5:>Nil)+-- > vdrop d0 (1:>2:>Nil) == (1:>2:>Nil)+-- > vdrop d4 (1:>2:>Nil) == TYPE ERROR vdrop :: SNat m -> Vec (m + n) a -> Vec n a vdrop n = snd . vsplit n @@ -342,7 +407,8 @@ -- | 'vexact' @n xs@ returns @n@'th element of @xs@, NB: vector elements -- have a descending subscript starting from 'maxIndex' and ending at 0 ----- > vexact (snat :: SNat 1) <1,2,3,4,5> == 4+-- > vexact (snat :: SNat 1) (1:>2:>3:>4:>5:>Nil) == 4+-- > vexact d1 (1:>2:>3:>4:>5:>Nil) == 4 vexact :: SNat m -> Vec (m + (n + 1)) a -> a vexact n xs = vhead $ snd $ vsplit n (vreverse xs) @@ -350,7 +416,8 @@ -- | 'vselect' @f s n xs@ selects @n@ elements with stepsize @s@ and -- offset @f@ from @xs@ ----- vselect (snat :: SNat 1) (snat :: SNat 2) (snat :: SNat 3) <1,2,3,4,5,6,7,8> == <2,4,6>+-- > vselect (snat :: SNat 1) (snat :: SNat 2) (snat :: SNat 3) (1:>2:>3:>4:>5:>6:>7:>8:>Nil) == (2:>4:>6:>Nil)+-- > vselect d1 d2 d3 (1:>2:>3:>4:>5:>6:>7:>8:>Nil) == (2:>4:>6:>Nil) vselect :: ((f + (s * n) + 1) <= i) => SNat f -> SNat s@@ -375,6 +442,9 @@ {-# NOINLINE vcopy #-} -- | 'vcopy' @n a@ returns a vector that has @n@ copies of @a@+--+-- > vcopy (snat :: SNat 3) 6 == (6:>6:>6:>Nil)+-- > vcopy d3 6 == (6:>6:>6:>Nil) vcopy :: SNat n -> a -> Vec n a vcopy n a = vreplicateU (toUNat n) a @@ -383,7 +453,7 @@ vreplicateU (USucc s) x = x :> vreplicateU s x {-# INLINEABLE vcopyI #-}--- | 'vcopy' @a@ creates a vector with as many copies of @a@ as demanded by the+-- | 'vcopyI' @a@ creates a vector with as many copies of @a@ as demanded by the -- context vcopyI :: KnownNat n => a -> Vec n a vcopyI = withSNat vcopy@@ -392,7 +462,8 @@ -- | 'viterate' @n f x@ returns a vector starting with @x@ followed by @n@ -- repeated applications of @f@ to @x@ ----- > viterate (snat :: SNat 4) f x = <x, f x, f (f x), f (f (f x))>+-- > viterate (snat :: SNat 4) f x == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)+-- > viterate d4 f x == (x :> f x :> f (f x) :> f (f (f x)) :> Nil) viterate :: SNat n -> (a -> a) -> a -> Vec n a viterate n f a = viterateU (toUNat n) f a @@ -410,7 +481,8 @@ -- | 'vgenerate' @n f x@ returns a vector with @n@ repeated applications of @f@ -- to @x@ ----- > vgenerate (snat :: SNat 4) f x = <f x, f (f x), f (f (f x)), f (f (f (f x)))>+-- > vgenerate (snat :: SNat 4) f x == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)+-- > vgenerate d4 f x == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil) vgenerate :: SNat n -> (a -> a) -> a -> Vec n a vgenerate n f a = viterate n f (f a) @@ -427,7 +499,53 @@ -- | Create a vector literal from a list literal ----- > $(v [1::Signed 8,2,3,4,5]) == <1,2,3,4,5> :: Vec 5 (Signed 8)+-- > $(v [1::Signed 8,2,3,4,5]) == (8:>2:>3:>4:>5:>Nil) :: Vec 5 (Signed 8) v :: Lift a => [a] -> ExpQ v [] = [| Nil |] v (x:xs) = [| x :> $(v xs) |]++-- | 'Vec'tor as a 'Proxy' for 'Nat'+asNatProxy :: Vec n a -> Proxy n+asNatProxy _ = Proxy++{-# NOINLINE lazyV #-}+-- | For when your vector functions are too strict in their arguments+--+-- For example:+--+-- > -- Bubble sort for 1 iteration+-- > sortV xs = vmap fst sorted <: (snd (vlast sorted))+-- > where+-- > lefts = vhead xs :> vmap snd (vinit sorted)+-- > rights = vtail xs+-- > sorted = vzipWith compareSwapL lefts rights+-- >+-- > -- Compare and swap+-- > compareSwapL a b = if a < b then (a,b)+-- > else (b,a)+--+-- Will not terminate because 'vzipWith' is too strict in its left argument:+--+-- > *Main> sortV (4 :> 1 :> 2 :> 3 :> Nil)+-- > <*** Exception: <<loop>>+--+-- In this case, adding 'lazyV' on 'vzipWith's left argument:+--+-- > sortVL xs = vmap fst sorted <: (snd (vlast sorted))+-- > where+-- > lefts = vhead xs :> vmap snd (vinit sorted)+-- > rights = vtail xs+-- > sorted = vzipWith compareSwapL (lazyV lefts) rights+--+-- Results in a successful computation:+--+-- > *Main> sortVL (4 :> 1 :> 2 :> 3 :> Nil)+-- > <1,2,3,4>+lazyV :: KnownNat n+ => Vec n a+ -> Vec n a+lazyV = lazyV' (vcopyI undefined)+ where+ lazyV' :: Vec n a -> Vec n a -> Vec n a+ lazyV' Nil _ = Nil+ lazyV' (_ :> xs) ys = vhead ys :> lazyV' xs (vtail ys)