packages feed

clash-prelude (empty) → 0.2

raw patch · 14 files changed

+1404/−0 lines, 14 filesdep +basedep +data-defaultdep +template-haskellsetup-changed

Dependencies added: base, data-default, template-haskell, th-lift

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c)2013, University of Twente++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of University of Twente nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,2 @@+= WARNING =+Only works with latest version of GHC-HEAD (https://github.com/ghc/ghc)!
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ clash-prelude.cabal view
@@ -0,0 +1,43 @@+Name:                 clash-prelude+Version:              0.2+Synopsis:             CAES Language for Synchronous Hardware+-- Description:+Homepage:             http://clash.ewi.utwente.nl/+bug-reports:          http://github.com/christiaanb/clash-prelude/issues+License:              BSD3+License-file:         LICENSE+Author:               Christiaan Baaij+Maintainer:           Christiaan Baaij <christiaan.baaij@gmail.com>+Copyright:            Copyright (C) 2013-2014 University of Twente+Category:             Hardware+Build-type:           Simple++Extra-source-files:   README.md++Cabal-version:        >=1.10++source-repository head+  type: git+  location: git://github.com/christiaanb/clash-prelude.git++Library+  HS-Source-Dirs:     src++  default-language:   Haskell2010+  ghc-options:        -Wall -fwarn-tabs++  Exposed-modules:    CLaSH.Bit+                      CLaSH.Class.BitVector+                      CLaSH.Prelude+                      CLaSH.Promoted.Bool+                      CLaSH.Promoted.Nat+                      CLaSH.Promoted.Ord+                      CLaSH.Signal+                      CLaSH.Sized.Signed+                      CLaSH.Sized.Unsigned+                      CLaSH.Sized.Vector++  Build-depends:      base                 >= 4.7.0.0 && < 5,+                      data-default         >= 0.5.3,+                      template-haskell     >= 2.9.0.0,+                      th-lift              >= 0.5.6
+ src/CLaSH/Bit.hs view
@@ -0,0 +1,65 @@+{-# LANGUAGE TemplateHaskell #-}++{-# OPTIONS_GHC -fno-warn-missing-methods #-}++module CLaSH.Bit+  (Bit(..))+where++import Data.Bits+import Data.Default+import Language.Haskell.TH.Lift++data Bit = H | L++instance Eq Bit where+  (==) = eqBit++{-# NOINLINE eqBit #-}+eqBit :: Bit -> Bit -> Bool+eqBit L L = True+eqBit H H = True+eqBit _ _ = False++instance Show Bit where+  show H = "1"+  show L = "0"++instance Default Bit where+  def = L++deriveLift ''Bit++{-# NOINLINE bAnd #-}+bAnd :: Bit -> Bit -> Bit+bAnd H H = H+bAnd _ _ = L++{-# NOINLINE bOr #-}+bOr :: Bit -> Bit -> Bit+bOr L L  = L+bOr _ _  = H++{-# NOINLINE bXor #-}+bXor :: Bit -> Bit -> Bit+bXor L L = L+bXor H H = L+bXor _ _ = H++{-# NOINLINE bNot #-}+bNot :: Bit -> Bit+bNot L = H+bNot H = L++instance Bits Bit where+  (.&.)        = bAnd+  (.|.)        = bOr+  xor          = bXor+  complement   = bNot+  bit          = const H+  testBit H _  = True+  testBit _ _  = False+  bitSizeMaybe = const (Just 1)+  isSigned     = const False+  popCount H   = 1+  popCount _   = 0
+ src/CLaSH/Class/BitVector.hs view
@@ -0,0 +1,13 @@+{-# LANGUAGE DataKinds        #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeFamilies     #-}+module CLaSH.Class.BitVector where++import CLaSH.Bit+import CLaSH.Sized.Vector+import GHC.TypeLits++class BitVector a where+  type BitSize a :: Nat+  toBV   :: KnownNat (BitSize a) => a -> Vec (BitSize a) Bit+  fromBV :: KnownNat (BitSize a) => Vec (BitSize a) Bit -> a
+ src/CLaSH/Prelude.hs view
@@ -0,0 +1,123 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE KindSignatures      #-}+{-# LANGUAGE TypeOperators       #-}++{-# OPTIONS_GHC -O0 -fno-omit-interface-pragmas #-}++module CLaSH.Prelude+  ( module Exported+  , module CLaSH.Prelude+  )+where++import Control.Arrow         as Exported+import Control.Applicative   as Exported+import Control.Category      as Category+import Data.Bits             as Exported+import Data.Default          as Exported+import CLaSH.Class.BitVector as Exported+import CLaSH.Promoted.Bool   as Exported+import CLaSH.Promoted.Nat    as Exported+import CLaSH.Promoted.Ord    as Exported+import CLaSH.Sized.Signed    as Exported+import CLaSH.Sized.Unsigned  as Exported+import CLaSH.Sized.Vector    as Exported+import CLaSH.Bit             as Exported+import CLaSH.Signal          as Exported+import GHC.TypeLits          as Exported++{-# INLINABLE window #-}+window :: (KnownNat (n + 1), Default a)+       => Signal a+       -> Vec ((n + 1) + 1) (Signal a)+window x = x :> prev+  where+    prev = registerP (vcopyI def) next+    next = x +>> prev++{-# INLINABLE windowP #-}+windowP :: (KnownNat (n + 1), Default a)+        => Signal a+        -> Vec (n + 1) (Signal a)+windowP x = prev+  where+    prev = registerP (vcopyI def) next+    next = x +>> prev++{-# INLINABLE (<^>) #-}+(<^>) :: (Pack i, Pack o)+      => (s -> i -> (s,o))+      -> s+      -> (SignalP i -> SignalP o)+f <^> iS = \i -> let (s',o) = unpack $ f <$> s <*> (pack i)+                     s      = register iS s'+                 in unpack o++{-# INLINABLE registerP #-}+registerP :: Pack a => a -> SignalP a -> SignalP a+registerP i = unpack Prelude.. register i Prelude.. pack++{-# NOINLINE blockRam #-}+blockRam :: forall n m a . (KnownNat n, KnownNat m, Pack a)+         => SNat n+         -> Signal (Unsigned m)+         -> Signal (Unsigned m)+         -> Signal Bool+         -> Signal a+         -> Signal a+blockRam n wr rd en din = pack $ (bram' <^> binit) (wr,rd,en,din)+  where+    binit :: (Vec n a,a)+    binit = (vcopy n (error "uninitialized ram"),error "uninitialized ram")++    bram' :: (Vec n a,a) -> (Unsigned m, Unsigned m, Bool, a)+          -> (((Vec n a),a),a)+    bram' (ram,o) (w,r,e,d) = ((ram',o'),o)+      where+        ram' | e         = vreplace ram w d+             | otherwise = ram+        o'               = ram ! r++{-# INLINABLE blockRamPow2 #-}+blockRamPow2 :: (KnownNat n, KnownNat (n^2), Pack a)+             => (SNat ((n^2) :: Nat))+             -> Signal (Unsigned n)+             -> Signal (Unsigned n)+             -> Signal Bool+             -> Signal a+             -> Signal a+blockRamPow2 = blockRam++newtype Comp a b = C { asFunction :: Signal a -> Signal b }++instance Category Comp where+  id            = C Prelude.id+  (C f) . (C g) = C (f Prelude.. g)++infixr 8 ><+(><) :: (a -> b) -> (c -> d) -> (a, c) -> (b, d)+(f >< g) (x,y) = (f x,g y)++instance Arrow Comp where+  arr         = C Prelude.. fmap+  first (C f) = C $ pack Prelude.. (f >< Prelude.id) Prelude.. unpack++instance ArrowLoop Comp where+  loop (C f) = C $ simpleLoop (unpack Prelude.. f Prelude.. pack)+    where+      simpleLoop g b = let ~(c,d) = g (b,d)+                       in c++registerC :: a -> Comp a a+registerC = C Prelude.. register++simulateC :: Comp a b -> [a] -> [b]+simulateC f = simulate (asFunction f)++{-# INLINABLE (^^^) #-}+(^^^) :: (s -> i -> (s,o)) -> s -> Comp i o+f ^^^ sI = C $ \i -> let (s',o) = unpack $ f <$> s <*> i+                         s      = register sI s'+                     in  o
+ src/CLaSH/Promoted/Bool.hs view
@@ -0,0 +1,10 @@+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeFamilies   #-}+{-# LANGUAGE PolyKinds      #-}+module CLaSH.Promoted.Bool where++type family If (x :: Bool) (y :: k) (z :: k) :: k++type instance If True  y z = y+type instance If False y z = z
+ src/CLaSH/Promoted/Nat.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE KindSignatures      #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators       #-}+module CLaSH.Promoted.Nat+  ( SNat, snat, withSNat, fromSNat+  , UNat (..), toUNat, addUNat, multUNat, powUNat+  )+where++import Data.Proxy+import GHC.TypeLits+import Unsafe.Coerce++data SNat (n :: Nat) = KnownNat n => SNat (Proxy n)++snat :: KnownNat n => SNat n+snat = SNat Proxy++withSNat :: KnownNat n => (SNat n -> a) -> a+withSNat f = f (SNat Proxy)++data UNat :: Nat -> * where+  UZero :: UNat 0+  USucc :: UNat n -> UNat (n + 1)++fromSNat :: SNat n -> Integer+fromSNat (SNat p) = natVal p++{-# NOINLINE fromSNat #-}+toUNat :: SNat n -> UNat n+toUNat (SNat p) = fromI (natVal p)+  where+    fromI :: Integer -> UNat m+    fromI 0 = unsafeCoerce UZero+    fromI n = unsafeCoerce (USucc (fromI (n - 1)))++addUNat :: UNat n -> UNat m -> UNat (n + m)+addUNat UZero     y     = y+addUNat x         UZero = x+addUNat (USucc x) y     = unsafeCoerce (USucc (addUNat x y))++multUNat :: UNat n -> UNat m -> UNat (n * m)+multUNat UZero      _     = UZero+multUNat _          UZero = UZero+multUNat (USucc x) y      = unsafeCoerce (addUNat y (multUNat x y))++powUNat :: UNat n -> UNat m -> UNat (n ^ m)+powUNat _ UZero     = USucc UZero+powUNat x (USucc y) = unsafeCoerce (multUNat x (powUNat x y))
+ src/CLaSH/Promoted/Ord.hs view
@@ -0,0 +1,15 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}+module CLaSH.Promoted.Ord where++import GHC.TypeLits++import CLaSH.Promoted.Bool++type family Min (x :: Nat) (y :: Nat) :: Nat+type instance Min x y = If (x <=? y) x y++type family Max (x :: Nat) (y :: Nat) :: Nat+type instance Max x y = If (x <=? y) y x
+ src/CLaSH/Signal.hs view
@@ -0,0 +1,227 @@+{-# LANGUAGE LambdaCase      #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies    #-}++module CLaSH.Signal+  ( Signal+  , fromList+  , signal+  , sample+  , register+  , simulate+  , Pack(..)+  , simulateP+  , (<^), (^>)+  )+where++import Data.Default+import Control.Applicative+import Language.Haskell.TH.Syntax(Lift(..))++import CLaSH.Bit            (Bit)+import CLaSH.Sized.Signed   (Signed)+import CLaSH.Sized.Unsigned (Unsigned)+import CLaSH.Sized.Vector   (Vec(..), vmap, vhead, vtail)++{-# NOINLINE register  #-}+{-# NOINLINE signal    #-}+{-# NOINLINE mapSignal #-}+{-# NOINLINE appSignal #-}++infixr 5 :-+data Signal a = a :- Signal a++fromList :: [a] -> Signal a+fromList []     = error "finite list"+fromList (x:xs) = x :- fromList xs++instance Show a => Show (Signal a) where+  show (x :- xs) = show x ++ " " ++ show xs++instance Lift a => Lift (Signal a) where+  lift ~(x :- _) = [| signal x |]++instance Default a => Default (Signal a) where+  def = signal def++sample :: Int -> Signal a -> [a]+sample 0 _         = []+sample n ~(x :- xs) = x : (sample (n-1) xs)++signal :: a -> Signal a+signal a = a :- signal a++mapSignal :: (a -> b) -> Signal a -> Signal b+mapSignal f (a :- as) = f a :- mapSignal f as++appSignal :: Signal (a -> b) -> Signal a -> Signal b+appSignal (f :- fs) ~(a :- as) = f a :- appSignal fs as++instance Functor Signal where+  fmap = mapSignal++instance Applicative Signal where+  pure  = signal+  (<*>) = appSignal++unSignal :: Signal a -> a+unSignal (a :- _) = a++next :: Signal a -> Signal a+next (_ :- as) = as++diag :: Signal (Signal a) -> Signal a+diag (xs :- xss) = unSignal xs :- diag (fmap next xss)++instance Monad Signal where+  return    = signal+  xs >>= f  = diag (fmap f xs)++register :: a -> Signal a -> Signal a+register i s = i :- s++simulate :: (Signal a -> Signal b) -> [a] -> [b]+simulate f as = sample (length as) (f (fromList as))++class Pack a where+  type SignalP a+  pack   :: SignalP a -> Signal a+  unpack :: Signal a -> SignalP a++simulateP :: (Pack a, Pack b) => (SignalP a -> SignalP b) -> [a] -> [b]+simulateP f = simulate (pack . f . unpack)++instance Pack Bit where+  type SignalP Bit = Signal Bit+  pack   = id+  unpack = id++instance Pack (Signed n) where+  type SignalP (Signed n) = Signal (Signed n)+  pack   = id+  unpack = id++instance Pack (Unsigned n) where+  type SignalP (Unsigned n) = Signal (Unsigned n)+  pack   = id+  unpack = id++instance Pack Bool where+  type SignalP Bool = Signal Bool+  pack   = id+  unpack = id++instance Pack Integer where+  type SignalP Integer = Signal Integer+  pack   = id+  unpack = id++instance Pack Int where+  type SignalP Int = Signal Int+  pack   = id+  unpack = id++instance Pack Float where+  type SignalP Float = Signal Float+  pack   = id+  unpack = id++instance Pack Double where+  type SignalP Double = Signal Double+  pack   = id+  unpack = id++instance Pack () where+  type SignalP () = Signal ()+  pack   = id+  unpack = id++instance Pack (a,b) where+  type SignalP (a,b) = (Signal a, Signal b)+  pack       = uncurry (liftA2 (,))+  unpack tup = (fmap fst tup, fmap snd tup)++instance Pack (a,b,c) where+  type SignalP (a,b,c) = (Signal a, Signal b, Signal c)+  pack (a,b,c) = (,,) <$> a <*> b <*> c+  unpack tup   = (fmap (\(x,_,_) -> x) tup+                ,fmap (\(_,x,_) -> x) tup+                ,fmap (\(_,_,x) -> x) tup+                )++instance Pack (a,b,c,d) where+  type SignalP (a,b,c,d) = (Signal a, Signal b, Signal c, Signal d)+  pack (a,b,c,d) = (,,,) <$> a <*> b <*> c <*> d+  unpack tup     = (fmap (\(x,_,_,_) -> x) tup+                  ,fmap (\(_,x,_,_) -> x) tup+                  ,fmap (\(_,_,x,_) -> x) tup+                  ,fmap (\(_,_,_,x) -> x) tup+                  )++instance Pack (a,b,c,d,e) where+  type SignalP (a,b,c,d,e) = (Signal a, Signal b, Signal c, Signal d, Signal e)+  pack (a,b,c,d,e) = (,,,,) <$> a <*> b <*> c <*> d <*> e+  unpack tup       = (fmap (\(x,_,_,_,_) -> x) tup+                    ,fmap (\(_,x,_,_,_) -> x) tup+                    ,fmap (\(_,_,x,_,_) -> x) tup+                    ,fmap (\(_,_,_,x,_) -> x) tup+                    ,fmap (\(_,_,_,_,x) -> x) tup+                    )++instance Pack (a,b,c,d,e,f) where+  type SignalP (a,b,c,d,e,f) = (Signal a, Signal b, Signal c, Signal d, Signal e, Signal f)+  pack (a,b,c,d,e,f) = (,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f+  unpack tup         = (fmap (\(x,_,_,_,_,_) -> x) tup+                      ,fmap (\(_,x,_,_,_,_) -> x) tup+                      ,fmap (\(_,_,x,_,_,_) -> x) tup+                      ,fmap (\(_,_,_,x,_,_) -> x) tup+                      ,fmap (\(_,_,_,_,x,_) -> x) tup+                      ,fmap (\(_,_,_,_,_,x) -> x) tup+                      )++instance Pack (a,b,c,d,e,f,g) where+  type SignalP (a,b,c,d,e,f,g) = (Signal a, Signal b, Signal c, Signal d, Signal e, Signal f, Signal g)+  pack (a,b,c,d,e,f,g) = (,,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f <*> g+  unpack tup           = (fmap (\(x,_,_,_,_,_,_) -> x) tup+                        ,fmap (\(_,x,_,_,_,_,_) -> x) tup+                        ,fmap (\(_,_,x,_,_,_,_) -> x) tup+                        ,fmap (\(_,_,_,x,_,_,_) -> x) tup+                        ,fmap (\(_,_,_,_,x,_,_) -> x) tup+                        ,fmap (\(_,_,_,_,_,x,_) -> x) tup+                        ,fmap (\(_,_,_,_,_,_,x) -> x) tup+                        )++instance Pack (a,b,c,d,e,f,g,h) where+  type SignalP (a,b,c,d,e,f,g,h) = (Signal a, Signal b, Signal c, Signal d, Signal e, Signal f, Signal g, Signal h)+  pack (a,b,c,d,e,f,g,h) = (,,,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f <*> g <*> h+  unpack tup             = (fmap (\(x,_,_,_,_,_,_,_) -> x) tup+                          ,fmap (\(_,x,_,_,_,_,_,_) -> x) tup+                          ,fmap (\(_,_,x,_,_,_,_,_) -> x) tup+                          ,fmap (\(_,_,_,x,_,_,_,_) -> x) tup+                          ,fmap (\(_,_,_,_,x,_,_,_) -> x) tup+                          ,fmap (\(_,_,_,_,_,x,_,_) -> x) tup+                          ,fmap (\(_,_,_,_,_,_,x,_) -> x) tup+                          ,fmap (\(_,_,_,_,_,_,_,x) -> x) tup+                          )++instance Pack (Vec n a) where+  type SignalP (Vec n a) = Vec n (Signal a)+  pack vs                = vmap unSignal vs :- pack (vmap next vs)+  unpack (Nil :- _)         = Nil+  unpack vs@((_ :> _) :- _) = fmap vhead vs :> (unpack (fmap vtail vs))++(<^) :: Applicative f => f a -> (a -> b -> c) -> f b -> f c+v <^ f = liftA2 f v++(^>) :: Applicative f => (f a -> f b) -> f a -> f b+f ^> v = f v++instance Num a => Num (Signal a) where+  (+)         = liftA2 (+)+  (-)         = liftA2 (-)+  (*)         = liftA2 (*)+  negate      = fmap negate+  abs         = fmap abs+  signum      = fmap signum+  fromInteger = signal . fromInteger
+ src/CLaSH/Sized/Signed.hs view
@@ -0,0 +1,269 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE KindSignatures      #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell     #-}+{-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE TypeOperators       #-}++{-# OPTIONS_GHC -fno-warn-missing-methods #-}++module CLaSH.Sized.Signed+  ( Signed+  , resizeS+  , resizeS_wrap+  )+where++import Data.Bits+import Data.Default+import Language.Haskell.TH+import Language.Haskell.TH.Syntax(Lift(..))+import GHC.TypeLits++import CLaSH.Bit+import CLaSH.Class.BitVector+import CLaSH.Promoted.Nat+import CLaSH.Sized.Vector++newtype Signed (n :: Nat) = S Integer++instance Eq (Signed n) where+  (==) = eqS++{-# NOINLINE eqS #-}+eqS :: (Signed n) -> (Signed n) -> Bool+(S n) `eqS` (S m) = n == m++instance Ord (Signed n) where+  (<)  = ltS+  (>=) = geS+  (>)  = gtS+  (<=) = leS++ltS,geS,gtS,leS :: Signed n -> Signed n -> Bool+{-# NOINLINE ltS #-}+ltS (S n) (S m) = n < m+{-# NOINLINE geS #-}+geS (S n) (S m) = n >= m+{-# NOINLINE gtS #-}+gtS (S n) (S m) = n > m+{-# NOINLINE leS #-}+leS (S n) (S m) = n <= m++instance KnownNat n => Enum (Signed n) where+  succ           = plusS (fromIntegerS 1)+  pred           = minS (fromIntegerS 1)+  toEnum         = fromIntegerS . toInteger+  fromEnum       = fromEnum . toIntegerS++instance KnownNat n => Bounded (Signed n) where+  minBound = minBoundS+  maxBound = maxBoundS++minBoundS,maxBoundS :: forall n . KnownNat n => Signed n+{-# NOINLINE minBoundS #-}+minBoundS = S $ negate $ 2 ^ (fromSNat (snat :: SNat n) -1)+{-# NOINLINE maxBoundS #-}+maxBoundS = S $ 2 ^ (fromSNat (snat :: SNat n) - 1) - 1++instance KnownNat n => Num (Signed n) where+  (+)         = plusS+  (-)         = minS+  (*)         = timesS+  negate      = negateS+  abs         = absS+  signum      = signumS+  fromInteger = fromIntegerS++plusS,minS,timesS :: KnownNat n => Signed n -> Signed n -> Signed n+{-# NOINLINE plusS #-}+plusS (S a) (S b) = fromIntegerS_inlineable $ a + b++{-# NOINLINE minS #-}+minS (S a) (S b) = fromIntegerS_inlineable $ a - b++{-# NOINLINE timesS #-}+timesS (S a) (S b) = fromIntegerS_inlineable $ a * b++negateS,absS,signumS :: KnownNat n => Signed n -> Signed n+{-# NOINLINE negateS #-}+negateS (S n) = fromIntegerS_inlineable (0 - n)++{-# NOINLINE absS #-}+absS (S n) = fromIntegerS_inlineable (abs n)++{-# NOINLINE signumS #-}+signumS (S n) = fromIntegerS_inlineable (signum n)++fromIntegerS,fromIntegerS_inlineable :: forall n . KnownNat n => Integer -> Signed (n :: Nat)+{-# NOINLINE fromIntegerS #-}+fromIntegerS = fromIntegerS_inlineable+{-# INLINABLE fromIntegerS_inlineable #-}+fromIntegerS_inlineable i+    | nS == 0   = S 0+    | otherwise = res+  where+    nS  = fromSNat (snat :: SNat n)+    sz  = 2 ^ (nS - 1)+    res = case divMod i sz of+            (s,i') | even s    -> S i'+                   | otherwise -> S (i' - sz)++instance KnownNat n => Real (Signed n) where+  toRational = toRational . toIntegerS++instance KnownNat n => Integral (Signed n) where+  quot      = quotS+  rem       = remS+  div       = divS+  mod       = modS+  quotRem   = quotRemS+  divMod    = divModS+  toInteger = toIntegerS++quotS,remS,divS,modS :: KnownNat n => Signed n -> Signed n -> Signed n+{-# NOINLINE quotS #-}+quotS = (fst.) . quotRemS_inlineable+{-# NOINLINE remS #-}+remS = (snd.) . quotRemS_inlineable+{-# NOINLINE divS #-}+divS = (fst.) . divModS_inlineable+{-# NOINLINE modS #-}+modS = (snd.) . divModS_inlineable++quotRemS,divModS :: KnownNat n => Signed n -> Signed n -> (Signed n, Signed n)+quotRemS n d = (n `quotS` d,n `remS` d)+divModS n d  = (n `divS` d,n `modS` d)++quotRemS_inlineable,divModS_inlineable :: KnownNat n => Signed n -> Signed n -> (Signed n, Signed n)+{-# INLINEABLE quotRemS_inlineable #-}+(S a) `quotRemS_inlineable` (S b) = let (a',b') = a `quotRem` b+                                    in (fromIntegerS_inlineable a', fromIntegerS_inlineable b')+{-# INLINEABLE divModS_inlineable #-}+(S a) `divModS_inlineable` (S b) = let (a',b') = a `divMod` b+                                   in (fromIntegerS_inlineable a', fromIntegerS_inlineable b')++{-# NOINLINE toIntegerS #-}+toIntegerS :: Signed n -> Integer+toIntegerS (S n) = n++instance KnownNat n => Bits (Signed n) where+  (.&.)          = andS+  (.|.)          = orS+  xor            = xorS+  complement     = complementS+  bit            = bitS+  testBit        = testBitS+  bitSizeMaybe   = Just . finiteBitSizeS+  isSigned       = const True+  shiftL         = shiftLS+  shiftR         = shiftRS+  rotateL        = rotateLS+  rotateR        = rotateRS+  popCount       = popCountS++andS,orS,xorS :: KnownNat n => Signed n -> Signed n -> Signed n+{-# NOINLINE andS #-}+(S a) `andS` (S b) = fromIntegerS_inlineable (a .&. b)+{-# NOINLINE orS #-}+(S a) `orS` (S b)  = fromIntegerS_inlineable (a .|. b)+{-# NOINLINE xorS #-}+(S a) `xorS` (S b) = fromIntegerS_inlineable (xor a b)++{-# NOINLINE complementS #-}+complementS :: KnownNat n => Signed n -> Signed n+complementS = fromBitVector . vmap complement . toBitVector++{-# NOINLINE bitS #-}+bitS :: KnownNat n => Int -> Signed n+bitS = fromIntegerS_inlineable . bit++{-# NOINLINE testBitS #-}+testBitS :: Signed n -> Int -> Bool+testBitS (S n) i = testBit n i++shiftLS,shiftRS,rotateLS,rotateRS :: KnownNat n => Signed n -> Int -> Signed n+{-# NOINLINE shiftLS #-}+shiftLS _ b | b < 0  = error "'shiftL'{Signed} undefined for negative numbers"+shiftLS (S n) b      = fromIntegerS_inlineable (shiftL n b)+{-# NOINLINE shiftRS #-}+shiftRS _ b | b < 0  = error "'shiftR'{Signed} undefined for negative numbers"+shiftRS (S n) b      = fromIntegerS_inlineable (shiftR n b)+{-# NOINLINE rotateLS #-}+rotateLS _ b | b < 0 = error "'shiftL'{Signed} undefined for negative numbers"+rotateLS n b         = let b' = b `mod` finiteBitSizeS n+                       in shiftL n b' .|. shiftR n (finiteBitSizeS n - b')+{-# NOINLINE rotateRS #-}+rotateRS _ b | b < 0 = error "'shiftR'{Signed} undefined for negative numbers"+rotateRS n b         = let b' = b `mod` finiteBitSizeS n+                       in shiftR n b' .|. shiftL n (finiteBitSizeS n - b')++{-# NOINLINE popCountS #-}+popCountS :: Signed n -> Int+popCountS (S n) = popCount n++instance KnownNat n => FiniteBits (Signed n) where+  finiteBitSize = finiteBitSizeS++{-# NOINLINE finiteBitSizeS #-}+finiteBitSizeS :: forall n . KnownNat n => Signed n -> Int+finiteBitSizeS _ = fromInteger $ fromSNat (snat :: SNat n)++instance Show (Signed n) where+  show (S n) = show n++instance KnownNat n => Default (Signed n) where+  def = fromIntegerS 0++instance KnownNat n => Lift (Signed n) where+  lift (S i) = sigE [| fromIntegerS i |] (decSigned $ fromSNat (snat :: (SNat n)))++decSigned :: Integer -> TypeQ+decSigned n = appT (conT ''Signed) (litT $ numTyLit n)++instance BitVector (Signed n) where+  type BitSize (Signed n) = n+  toBV   = toBitVector+  fromBV = fromBitVector++{-# NOINLINE toBitVector #-}+toBitVector :: KnownNat n => Signed n -> Vec n Bit+toBitVector (S m) = vreverse $ vmap (\x -> if odd x then H else L) $ viterateI (`div` 2) m++{-# NOINLINE fromBitVector #-}+fromBitVector :: KnownNat n => Vec n Bit -> Signed n+fromBitVector = fromBitList . reverse . toList++{-# INLINABLE fromBitList #-}+fromBitList :: KnownNat n => [Bit] -> Signed n+fromBitList l = fromIntegerS_inlineable+              $ sum [ n+                    | (n,b) <- zip (iterate (*2) 1) l+                    , b == H+                    ]++{-# NOINLINE resizeS #-}+-- | A sign-preserving resize operation+--+-- 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+                    (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.+--+-- Increasing the size of the number replicates the sign bit to the left.+-- Truncating a number of length N to a length L just removes the leftmost N-L bits.+--+resizeS_wrap :: KnownNat m => Signed n -> Signed m+resizeS_wrap s@(S n) = fromIntegerS_inlineable n
+ src/CLaSH/Sized/Unsigned.hs view
@@ -0,0 +1,227 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE KindSignatures      #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell     #-}+{-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE TypeOperators       #-}++{-# OPTIONS_GHC -fno-warn-missing-methods #-}++module CLaSH.Sized.Unsigned+  ( Unsigned+  , resizeU+  )+where++import Data.Bits+import Data.Default+import Language.Haskell.TH+import Language.Haskell.TH.Syntax(Lift(..))+import GHC.TypeLits++import CLaSH.Bit+import CLaSH.Class.BitVector+import CLaSH.Promoted.Nat+import CLaSH.Sized.Vector++newtype Unsigned (n :: Nat) = U Integer++instance Eq (Unsigned n) where+  (==) = eqU++{-# NOINLINE eqU #-}+eqU :: (Unsigned n) -> (Unsigned n) -> Bool+(U n) `eqU` (U m) = n == m++instance Ord (Unsigned n) where+  (<)  = ltU+  (>=) = geU+  (>)  = gtU+  (<=) = leU++ltU,geU,gtU,leU :: Unsigned n -> Unsigned n -> Bool+{-# NOINLINE ltU #-}+ltU (U n) (U m) = n < m+{-# NOINLINE geU #-}+geU (U n) (U m) = n >= m+{-# NOINLINE gtU #-}+gtU (U n) (U m) = n > m+{-# NOINLINE leU #-}+leU (U n) (U m) = n <= m++instance KnownNat n => Enum (Unsigned n) where+  succ           = plusU (fromIntegerU 1)+  pred           = minU (fromIntegerU 1)+  toEnum         = fromIntegerU . toInteger+  fromEnum       = fromEnum . toIntegerU++instance KnownNat n => Bounded (Unsigned n) where+  minBound = fromIntegerU 0+  maxBound = maxBoundU++{-# NOINLINE maxBoundU #-}+maxBoundU :: forall n . KnownNat n => Unsigned n+maxBoundU = U $ (2 ^ fromSNat (snat :: SNat n)) - 1++instance KnownNat n => Num (Unsigned n) where+  (+)         = plusU+  (-)         = minU+  (*)         = timesU+  negate      = id+  abs         = id+  signum      = signumU+  fromInteger = fromIntegerU++plusU,minU,timesU :: KnownNat n => Unsigned n -> Unsigned n -> Unsigned n+{-# NOINLINE plusU #-}+plusU (U a) (U b) = fromIntegerU_inlineable $ a + b++{-# NOINLINE minU #-}+minU (U a) (U b) = fromIntegerU_inlineable $ a - b++{-# NOINLINE timesU #-}+timesU (U a) (U b) = fromIntegerU_inlineable $ a * b++{-# NOINLINE signumU #-}+signumU :: Unsigned n -> Unsigned n+signumU (U 0) = (U 0)+signumU (U _) = (U 1)++fromIntegerU,fromIntegerU_inlineable :: forall n . KnownNat n => Integer -> Unsigned (n :: Nat)+{-# NOINLINE fromIntegerU #-}+fromIntegerU = fromIntegerU_inlineable+{-# INLINABLE fromIntegerU_inlineable #-}+fromIntegerU_inlineable i = U $ i `mod` (2 ^ fromSNat (snat :: SNat n))++instance KnownNat n => Real (Unsigned n) where+  toRational = toRational . toIntegerU++instance KnownNat n => Integral (Unsigned n) where+  quot      = quotU+  rem       = remU+  div       = quotU+  mod       = modU+  quotRem   = quotRemU+  divMod    = divModU+  toInteger = toIntegerU++quotU,remU,modU :: KnownNat n => Unsigned n -> Unsigned n -> Unsigned n+{-# NOINLINE quotU #-}+quotU = (fst.) . quotRemU_inlineable+{-# NOINLINE remU #-}+remU = (snd.) . quotRemU_inlineable+{-# NOINLINE modU #-}+(U a) `modU` (U b) = fromIntegerU_inlineable (a `mod` b)++quotRemU,divModU :: KnownNat n => Unsigned n -> Unsigned n -> (Unsigned n, Unsigned n)+quotRemU n d = (n `quotU` d,n `remU` d)+divModU n d  = (n `quotU` d,n `modU` d)++{-# INLINEABLE quotRemU_inlineable #-}+quotRemU_inlineable :: KnownNat n => Unsigned n -> Unsigned n -> (Unsigned n, Unsigned n)+(U a) `quotRemU_inlineable` (U b) = let (a',b') = a `quotRem` b+                                    in (fromIntegerU_inlineable a', fromIntegerU_inlineable b')++{-# NOINLINE toIntegerU #-}+toIntegerU :: Unsigned n -> Integer+toIntegerU (U n) = n++instance KnownNat n => Bits (Unsigned n) where+  (.&.)          = andU+  (.|.)          = orU+  xor            = xorU+  complement     = complementU+  bit            = bitU+  testBit        = testBitU+  bitSizeMaybe   = Just . finiteBitSizeU+  isSigned       = const False+  shiftL         = shiftLU+  shiftR         = shiftRU+  rotateL        = rotateLU+  rotateR        = rotateRU+  popCount       = popCountU++andU,orU,xorU :: KnownNat n => Unsigned n -> Unsigned n -> Unsigned n+{-# NOINLINE andU #-}+(U a) `andU` (U b) = fromIntegerU_inlineable (a .&. b)+{-# NOINLINE orU #-}+(U a) `orU` (U b)  = fromIntegerU_inlineable (a .|. b)+{-# NOINLINE xorU #-}+(U a) `xorU` (U b) = fromIntegerU_inlineable (xor a b)++{-# NOINLINE complementU #-}+complementU :: KnownNat n => Unsigned n -> Unsigned n+complementU = fromBitVector . vmap complement . toBitVector++{-# NOINLINE bitU #-}+bitU :: KnownNat n => Int -> Unsigned n+bitU = fromIntegerU_inlineable . bit++{-# NOINLINE testBitU #-}+testBitU :: Unsigned n -> Int -> Bool+testBitU (U n) i = testBit n i++shiftLU,shiftRU,rotateLU,rotateRU :: KnownNat n => Unsigned n -> Int -> Unsigned n+{-# NOINLINE shiftLU #-}+shiftLU _ b | b < 0  = error "'shiftL'{Unsigned} undefined for negative numbers"+shiftLU (U n) b      = fromIntegerU_inlineable (shiftL n b)+{-# NOINLINE shiftRU #-}+shiftRU _ b | b < 0  = error "'shiftR'{Unsigned} undefined for negative numbers"+shiftRU (U n) b      = fromIntegerU_inlineable (shiftR n b)+{-# NOINLINE rotateLU #-}+rotateLU _ b | b < 0 = error "'shiftL'{Unsigned} undefined for negative numbers"+rotateLU n b         = let b' = b `mod` finiteBitSizeU n+                       in shiftL n b' .|. shiftR n (finiteBitSizeU n - b')+{-# NOINLINE rotateRU #-}+rotateRU _ b | b < 0 = error "'shiftR'{Unsigned} undefined for negative numbers"+rotateRU n b         = let b' = b `mod` finiteBitSizeU n+                       in shiftR n b' .|. shiftL n (finiteBitSizeU n - b')++{-# NOINLINE popCountU #-}+popCountU :: Unsigned n -> Int+popCountU (U n) = popCount n++instance KnownNat n => FiniteBits (Unsigned n) where+  finiteBitSize  = finiteBitSizeU++{-# NOINLINE finiteBitSizeU #-}+finiteBitSizeU :: forall n . KnownNat n => Unsigned n -> Int+finiteBitSizeU _ = fromInteger $ fromSNat (snat :: SNat n)++instance forall n . KnownNat n => Lift (Unsigned n) where+  lift (U i) = sigE [| fromIntegerU i |] (decUnsigned $ fromSNat (snat :: (SNat n)))++decUnsigned :: Integer -> TypeQ+decUnsigned n = appT (conT ''Unsigned) (litT $ numTyLit n)++instance Show (Unsigned n) where+  show (U n) = show n++instance KnownNat n => Default (Unsigned n) where+  def = fromIntegerU 0++instance BitVector (Unsigned n) where+  type BitSize (Unsigned n) = n+  toBV   = toBitVector+  fromBV = fromBitVector++{-# NOINLINE toBitVector #-}+toBitVector :: KnownNat n => Unsigned n -> Vec n Bit+toBitVector (U m) = vreverse $ vmap (\x -> if odd x then H else L) $ viterateI (`div` 2) m++{-# NOINLINE fromBitVector #-}+fromBitVector :: KnownNat n => Vec n Bit -> Unsigned n+fromBitVector = fromBitList . reverse . toList++{-# INLINABLE fromBitList #-}+fromBitList :: KnownNat n => [Bit] -> Unsigned n+fromBitList l = fromIntegerU_inlineable+              $ sum [ n+                    | (n,b) <- zip (iterate (*2) 1) l+                    , b == H+                    ]++{-# NOINLINE resizeU #-}+resizeU :: KnownNat m => Unsigned n -> Unsigned m+resizeU (U n) = fromIntegerU_inlineable n
+ src/CLaSH/Sized/Vector.hs view
@@ -0,0 +1,327 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE ExplicitForAll      #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE KindSignatures      #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell     #-}+{-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE TypeOperators       #-}++{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}++module CLaSH.Sized.Vector+  ( Vec(..), (<:)+  , vhead, vtail, vlast, vinit+  , (+>>), (<<+), (<++>), vconcat+  , vsplit, vsplitI, vunconcat, vunconcatI, vmerge+  , vreverse, vmap, vzipWith+  , vfoldr, vfoldl, vfoldr1, vfoldl1+  , vzip, vunzip+  , (!), vreplace+  , vtake, vtakeI, vdrop, vdropI, vexact, vselect, vselectI+  , vcopy, vcopyI, viterate, viterateI, vgenerate, vgenerateI+  , toList, v+  )+where++import Control.Applicative+import Data.Traversable+import Data.Foldable hiding (toList)+import GHC.TypeLits+import Language.Haskell.TH (ExpQ)+import Language.Haskell.TH.Syntax (Lift(..))+import Unsafe.Coerce (unsafeCoerce)++import CLaSH.Promoted.Nat++data Vec :: Nat -> * -> * where+  Nil  :: Vec 0 a+  (:>) :: a -> Vec n a -> Vec (n + 1) a++infixr 5 :>++instance Show a => Show (Vec n a) where+  show vs = "<" ++ punc vs ++ ">"+    where+      punc :: Show a => Vec m a -> String+      punc Nil        = ""+      punc (x :> Nil) = show x+      punc (x :> xs)  = show x ++ "," ++ punc xs++instance Eq a => Eq (Vec n a) where+  v1 == v2 = vfoldr (&&) True (vzipWith (==) v1 v2)++instance KnownNat n => Applicative (Vec n) where+  pure  = vcopyI+  (<*>) = vzipWith ($)++instance Traversable (Vec n) where+  traverse _ Nil       = pure Nil+  traverse f (x :> xs) = (:>) <$> f x <*> traverse f xs++instance Foldable (Vec n) where+  foldMap = foldMapDefault++instance Functor (Vec n) where+  fmap = fmapDefault++{-# NOINLINE vhead #-}+vhead :: Vec (n + 1) a -> a+vhead (x :> _) = x++{-# NOINLINE vtail #-}+vtail :: Vec (n + 1) a -> Vec n a+vtail (_ :> xs) = unsafeCoerce xs++{-# NOINLINE vlast #-}+vlast :: Vec (n + 1) a -> a+vlast (x :> Nil)     = x+vlast (_ :> y :> ys) = vlast (y :> ys)++{-# NOINLINE vinit #-}+vinit :: Vec (n + 1) a -> Vec n a+vinit (_ :> Nil)     = unsafeCoerce Nil+vinit (x :> y :> ys) = unsafeCoerce (x :> vinit (y :> ys))++{-# NOINLINE shiftIntoL #-}+shiftIntoL :: a -> Vec n a -> Vec n a+shiftIntoL _ Nil       = Nil+shiftIntoL s (x :> xs) = s :> (vinit (x:>xs))++infixr 4 +>>+{-# INLINEABLE (+>>) #-}+(+>>) :: a -> Vec n a -> Vec n a+s +>> xs = shiftIntoL s xs++{-# NOINLINE snoc #-}+snoc :: a -> Vec n a -> Vec (n + 1) a+snoc s Nil       = s :> Nil+snoc s (x :> xs) = x :> (snoc s xs)++infixl 5 <:+{-# INLINEABLE (<:) #-}+(<:) :: Vec n a -> a -> Vec (n + 1) a+xs <: s = snoc s xs++{-# NOINLINE shiftIntoR #-}+shiftIntoR :: a -> Vec n a -> Vec n a+shiftIntoR _ Nil     = Nil+shiftIntoR s (x:>xs) = snoc s (vtail (x:>xs))++infixl 4 <<++{-# INLINE (<<+) #-}+(<<+) :: Vec n a -> a -> Vec n a+xs <<+ s = shiftIntoR s xs++{-# NOINLINE vappend #-}+vappend :: Vec n a -> Vec m a -> Vec (n + m) a+vappend Nil       ys = ys+vappend (x :> xs) ys = unsafeCoerce (x :> (vappend xs ys))++infixr 5 <++>+{-# INLINE (<++>) #-}+(<++>) :: Vec n a -> Vec m a -> Vec (n + m) a+xs <++> ys = vappend xs ys++{-# NOINLINE vsplit #-}+vsplit :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)+vsplit n xs = vsplitU (toUNat n) xs++vsplitU :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)+vsplitU UZero     ys        = (Nil,ys)+vsplitU (USucc s) (y :> ys) = let (as,bs) = vsplitU s (unsafeCoerce ys)+                              in  (y :> as, bs)++{-# INLINEABLE vsplitI #-}+vsplitI :: KnownNat m => Vec (m + n) a -> (Vec m a, Vec n a)+vsplitI = withSNat vsplit++{-# NOINLINE vconcat #-}+vconcat :: Vec n (Vec m a) -> Vec (n * m) a+vconcat Nil       = Nil+vconcat (x :> xs) = unsafeCoerce (vappend x (vconcat xs))++{-# NOINLINE vunconcat #-}+vunconcat :: SNat n -> SNat m -> Vec (n * m) a -> Vec n (Vec m a)+vunconcat n m xs = vunconcatU (toUNat n) (toUNat m) xs++vunconcatU :: UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)+vunconcatU UZero      _  _  = Nil+vunconcatU (USucc n') m' ys = let (as,bs) = vsplitU m' (unsafeCoerce ys)+                              in  as :> vunconcatU n' m' bs++{-# INLINEABLE vunconcatI #-}+vunconcatI :: (KnownNat n, KnownNat m) => Vec (n * m) a -> Vec n (Vec m a)+vunconcatI = (withSNat . withSNat) vunconcat++{-# NOINLINE vmerge #-}+vmerge :: Vec n a -> Vec n a -> Vec (n + n) a+vmerge Nil       Nil       = Nil+vmerge (x :> xs) (y :> ys) = unsafeCoerce (x :> y :> (vmerge xs (unsafeCoerce ys)))++{-# NOINLINE vreverse #-}+vreverse :: Vec n a -> Vec n a+vreverse Nil        = Nil+vreverse (x :> xs)  = vreverse xs <: x++{-# NOINLINE vmap #-}+vmap :: (a -> b) -> Vec n a -> Vec n b+vmap _ Nil       = Nil+vmap f (x :> xs) = f x :> vmap f xs++{-# NOINLINE vzipWith #-}+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))++{-# NOINLINE vfoldr #-}+vfoldr :: (a -> b -> b) -> b -> Vec n a -> b+vfoldr _ z Nil       = z+vfoldr f z (x :> xs) = f x (vfoldr f z xs)++{-# NOINLINE vfoldl #-}+vfoldl :: (b -> a -> b) -> b -> Vec n a -> b+vfoldl _ z Nil       = z+vfoldl f z (x :> xs) = vfoldl f (f z x) xs++{-# NOINLINE vfoldr1 #-}+vfoldr1 :: (a -> a -> a) -> Vec (n + 1) a -> a+vfoldr1 _ (x :> Nil)       = x+vfoldr1 f (x :> (y :> ys)) = f x (vfoldr1 f (y :> ys))++{-# INLINEABLE vfoldl1 #-}+vfoldl1 :: (a -> a -> a) -> Vec (n + 1) a -> a+vfoldl1 f xs = vfoldl f (vhead xs) (vtail xs)++{-# NOINLINE vzip #-}+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))++{-# NOINLINE vunzip #-}+vunzip :: Vec n (a,b) -> (Vec n a, Vec n b)+vunzip Nil = (Nil,Nil)+vunzip ((a,b) :> xs) = let (as,bs) = vunzip xs+                       in  (a :> as, b :> bs)++{-# NOINLINE vindexM_integer #-}+vindexM_integer :: Vec n a -> Integer -> Maybe a+vindexM_integer Nil       _ = Nothing+vindexM_integer (x :> _)  0 = Just x+vindexM_integer (_ :> xs) n = vindexM_integer xs (n-1)++{-# NOINLINE vindex_integer #-}+vindex_integer :: KnownNat n => Vec n a -> Integer -> a+vindex_integer xs i = case vindexM_integer xs (maxIndex xs - i) of+    Just a  -> a+    Nothing -> error "index out of bounds"++{-# INLINEABLE (!) #-}+(!) :: (KnownNat n, Integral i) => Vec n a -> i -> a+xs ! i = vindex_integer xs (toInteger i)++{-# NOINLINE maxIndex #-}+maxIndex :: forall n a . KnownNat n => Vec n a -> Integer+maxIndex _ = fromSNat (snat :: SNat n) - 1++{-# NOINLINE vreplaceM_integer #-}+vreplaceM_integer :: Vec n a -> Integer -> a -> Maybe (Vec n a)+vreplaceM_integer Nil       _ _ = Nothing+vreplaceM_integer (_ :> xs) 0 y = Just (y :> xs)+vreplaceM_integer (x :> xs) n y = case vreplaceM_integer xs (n-1) y of+                                    Just xs' -> Just (x :> xs')+                                    Nothing  -> Nothing++{-# NOINLINE vreplace_integer #-}+vreplace_integer :: KnownNat n => Vec n a -> Integer -> a -> Vec n a+vreplace_integer xs i a = case vreplaceM_integer xs (maxIndex xs - i) a of+  Just ys -> ys+  Nothing -> error "index out of bounds"++{-# INLINEABLE vreplace #-}+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 :: SNat m -> Vec (m + n) a -> Vec m a+vtake n = fst . vsplit n++{-# INLINEABLE vtakeI #-}+vtakeI :: KnownNat m => Vec (m + n) a -> Vec m a+vtakeI = withSNat vtake++{-# NOINLINE vdrop #-}+vdrop :: SNat m -> Vec (m + n) a -> Vec n a+vdrop n = snd . vsplit n++{-# INLINEABLE vdropI #-}+vdropI :: KnownNat m => Vec (m + n) a -> Vec n a+vdropI = withSNat vdrop++{-# NOINLINE vexact #-}+vexact :: SNat m -> Vec (m + (n + 1)) a -> a+vexact n xs = vhead $ snd $ vsplit n xs++{-# NOINLINE vselect #-}+vselect ::+  ((f + (s * n) + 1) <= i)+  => SNat f+  -> SNat s+  -> SNat (n + 1)+  -> Vec i a+  -> Vec (n + 1) a+vselect f s n xs = vselect' (toUNat n) $ vdrop f (unsafeCoerce xs)+  where+    vselect' :: UNat n -> Vec m a -> Vec n a+    vselect' UZero      _           = Nil+    vselect' (USucc n') vs@(x :> _) = x :> vselect' n' (vdrop s (unsafeCoerce vs))++{-# NOINLINE vselectI #-}+vselectI ::+  ((f + (s * n) + 1) <= i, KnownNat (n + 1))+  => SNat f+  -> SNat s+  -> Vec i a+  -> Vec (n + 1) a+vselectI f s xs = withSNat (\n -> vselect f s n xs)++{-# NOINLINE vcopy #-}+vcopy :: SNat n -> a -> Vec n a+vcopy n a = vreplicateU (toUNat n) a++vreplicateU :: UNat n -> a -> Vec n a+vreplicateU UZero     _ = Nil+vreplicateU (USucc s) x = x :> vreplicateU s x++{-# INLINEABLE vcopyI #-}+vcopyI :: KnownNat n => a -> Vec n a+vcopyI = withSNat vcopy++{-# NOINLINE viterate #-}+viterate :: SNat n -> (a -> a) -> a -> Vec n a+viterate n f a = viterateU (toUNat n) f a++viterateU :: UNat n -> (a -> a) -> a -> Vec n a+viterateU UZero     _ _ = Nil+viterateU (USucc s) g x = x :> viterateU s g (g x)++{-# INLINEABLE viterateI #-}+viterateI :: KnownNat n => (a -> a) -> a -> Vec n a+viterateI = withSNat viterate++{-# INLINEABLE vgenerate #-}+vgenerate :: SNat n -> (a -> a) -> a -> Vec n a+vgenerate n f a = viterate n f (f a)++{-# INLINEABLE vgenerateI #-}+vgenerateI :: KnownNat n => (a -> a) -> a -> Vec n a+vgenerateI = withSNat vgenerate++{-# NOINLINE toList #-}+toList :: Vec n a -> [a]+toList = vfoldr (:) []++v :: Lift a => [a] -> ExpQ+v []     = [| Nil |]+v (x:xs) = [| x :> $(v xs) |]