{-|
Copyright  :  (C) 2013-2016, University of Twente,
                  2017     , Myrtle Software Ltd
License    :  BSD2 (see the file LICENSE)
Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE Trustworthy #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise       #-}

{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-redundant-constraints #-}

{-# OPTIONS_HADDOCK show-extensions #-}

module Clash.Sized.Vector
  ( -- * 'Vec'tor data type
    Vec(Nil,(:>),(:<),Cons)
    -- * Accessors
    -- ** Length information
  , length, lengthS
    -- ** Indexing
  , (!!), head, last, at
  , indices, indicesI
  , findIndex, elemIndex
    -- ** Extracting sub-vectors (slicing)
  , tail, init
  , take, takeI, drop, dropI
  , select, selectI
    -- *** Splitting
  , splitAt, splitAtI
  , unconcat, unconcatI
    -- * Construction
    -- ** Initialisation
  , singleton
  , replicate, repeat
  , iterate, iterateI, generate, generateI
    -- *** Initialisation from a list
  , listToVecTH
    -- ** Concatenation
  , (++), (+>>), (<<+), concat, concatMap
  , shiftInAt0, shiftInAtN , shiftOutFrom0, shiftOutFromN
  , merge
    -- * Modifying vectors
  , replace
    -- ** Permutations
  , permute, backpermute, scatter, gather
    -- *** Specialised permutations
  , reverse, transpose, interleave
  , rotateLeft, rotateRight, rotateLeftS, rotateRightS
    -- * Element-wise operations
    -- ** Mapping
  , map, imap, smap
    -- ** Zipping
  , zipWith, zipWith3, zipWith4, zipWith5, zipWith6, zipWith7
  , zip, zip3, zip4, zip5, zip6, zip7
  , izipWith
    -- ** Unzipping
  , unzip, unzip3, unzip4, unzip5, unzip6, unzip7
    -- * Folding
  , foldr, foldl, foldr1, foldl1, fold
  , ifoldr, ifoldl
    -- ** Specialised folds
  , dfold, dtfold, vfold
    -- * Prefix sums (scans)
  , scanl, scanr, postscanl, postscanr
  , mapAccumL, mapAccumR
    -- * Stencil computations
  , stencil1d, stencil2d
  , windows1d, windows2d
    -- * Conversions
  , toList
  , bv2v
  , v2bv
    -- * Misc
  , lazyV, VCons, asNatProxy, seqV, forceV, seqVX, forceVX
    -- * Primitives
    -- ** 'Traversable' instance
  , traverse#
    -- ** 'BitPack' instance
  , concatBitVector#
  , unconcatBitVector#
  )
where

import Control.DeepSeq            (NFData (..))
import qualified Control.Lens     as Lens hiding (pattern (:>), pattern (:<))
import Data.Constraint            ((:-)(..), Dict (..))
import Data.Constraint.Nat        (leZero)
import Data.Data
  (Data (..), Constr, DataType, Fixity (..), Typeable, mkConstr, mkDataType)
import Data.Either                (isLeft)
import Data.Default.Class         (Default (..))
import qualified Data.Foldable    as F
import Data.Kind                  (Type)
import Data.Proxy                 (Proxy (..))
import Data.Singletons.Prelude    (TyFun,Apply,type (@@))
import GHC.TypeLits               (CmpNat, KnownNat, Nat, type (+), type (-), type (*),
                                   type (^), type (<=), natVal)
import GHC.Base                   (Int(I#),Int#,isTrue#)
import GHC.Generics               hiding (Fixity (..))
import GHC.Prim                   ((==#),(<#),(-#))
import Language.Haskell.TH        (ExpQ)
import Language.Haskell.TH.Syntax (Lift(..))
import Prelude                    hiding ((++), (!!), concat, concatMap, drop,
                                          foldl, foldl1, foldr, foldr1, head,
                                          init, iterate, last, length, map,
                                          repeat, replicate, reverse, scanl,
                                          scanr, splitAt, tail, take, unzip,
                                          unzip3, zip, zip3, zipWith, zipWith3)
import qualified Prelude          as P
import Test.QuickCheck            (Arbitrary (..), CoArbitrary (..))
import Unsafe.Coerce              (unsafeCoerce)

import Clash.Annotations.Primitive
  (Primitive(InlinePrimitive), HDL(..))
import Clash.Promoted.Nat
  (SNat (..), SNatLE (..), UNat (..), compareSNat, leToPlus, pow2SNat,
   snatProxy, snatToInteger, subSNat, withSNat, toUNat)
import Clash.Promoted.Nat.Literals (d1)
import Clash.Sized.Internal.BitVector (Bit, BitVector, (++#), split#)
import Clash.Sized.Index          (Index)

import Clash.Class.BitPack        (packXWith, BitPack (..))
import Clash.XException
  (ShowX (..), NFDataX (..), showsX, showsPrecXWith, seqX, isX)

{- $setup
>>> :set -XDataKinds
>>> :set -XTypeFamilies
>>> :set -XTypeOperators
>>> :set -XTemplateHaskell
>>> :set -XFlexibleContexts
>>> :set -XTypeApplications
>>> :set -fplugin GHC.TypeLits.Normalise
>>> import Clash.Prelude
>>> import Data.Kind
>>> let compareSwapL a b = if a < b then (a,b) else (b,a)
>>> :{
let sortV xs = map fst sorted :< (snd (last sorted))
      where
        lefts  = head xs :> map snd (init sorted)
        rights = tail xs
        sorted = zipWith compareSwapL lefts rights
:}

>>> :{
let sortVL xs = map fst sorted :< (snd (last sorted))
      where
        lefts  = head xs :> map snd (init sorted)
        rights = tail xs
        sorted = zipWith compareSwapL (lazyV lefts) rights
:}

>>> :{
let sortV_flip xs = map fst sorted :< (snd (last sorted))
      where
        lefts  = head xs :> map snd (init sorted)
        rights = tail xs
        sorted = zipWith (flip compareSwapL) rights lefts
:}

>>> data Append (m :: Nat) (a :: Type) (f :: TyFun Nat Type) :: Type
>>> type instance Apply (Append m a) l = Vec (l + m) a
>>> let append' xs ys = dfold (Proxy :: Proxy (Append m a)) (const (:>)) ys xs
>>> let compareSwap a b = if a > b then (a,b) else (b,a)
>>> let insert y xs     = let (y',xs') = mapAccumL compareSwap y xs in xs' :< y'
>>> let insertionSort   = vfold (const insert)
>>> data IIndex (f :: TyFun Nat Type) :: Type
>>> :set -XUndecidableInstances
>>> type instance Apply IIndex l = Index ((2^l)+1)
>>> :{
let populationCount' :: (KnownNat k, KnownNat (2^k)) => BitVector (2^k) -> Index ((2^k)+1)
    populationCount' bv = dtfold (Proxy @IIndex)
                                 fromIntegral
                                 (\_ x y -> add x y)
                                 (bv2v bv)
:}

-}

infixr 5 `Cons`
-- | Fixed size vectors.
--
-- * Lists with their length encoded in their type
-- * 'Vec'tor elements have an __ASCENDING__ subscript starting from 0 and
--   ending at @'length' - 1@.
data Vec :: Nat -> Type -> Type where
  Nil  :: Vec 0 a
  Cons :: a -> Vec n a -> Vec (n + 1) a

-- | In many cases, this Generic instance only allows generic
-- functions/instances over vectors of at least size 1, due to the
-- /n-1/ in the /Rep (Vec n a)/ definition.
--
-- We'll have to wait for things like
-- https://ryanglscott.github.io/2018/02/11/how-to-derive-generic-for-some-gadts/
-- before we can work around this limitation
instance KnownNat n => Generic (Vec n a) where
  type Rep (Vec n a) =
    D1 ('MetaData "Vec" "Clash.Data.Vector" "clash-prelude" 'False)
      (C1 ('MetaCons "Nil" 'PrefixI 'False) U1 :+:
       C1 ('MetaCons "Cons" 'PrefixI 'False)
        (S1 ('MetaSel 'Nothing
                'NoSourceUnpackedness
                'NoSourceStrictness
                'DecidedLazy)
            (Rec0 a) :*:
         S1 ('MetaSel 'Nothing
                'NoSourceUnpackedness
                'NoSourceStrictness
                'DecidedLazy)
            (Rec0 (Vec (n-1) a))))
  from :: Vec n a -> Rep (Vec n a) x
from Nil         = (:+:)
  (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1)
  (C1
     ('MetaCons "Cons" 'PrefixI 'False)
     (S1
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        (Rec0 a)
      :*: S1
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (Rec0 (Vec (0 - 1) a))))
  x
-> M1
     D
     ('MetaData "Vec" "Clash.Data.Vector" "clash-prelude" 'False)
     (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1
      :+: C1
            ('MetaCons "Cons" 'PrefixI 'False)
            (S1
               ('MetaSel
                  'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
               (Rec0 a)
             :*: S1
                   ('MetaSel
                      'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                   (Rec0 (Vec (0 - 1) a))))
     x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1 x
-> (:+:)
     (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1)
     (C1
        ('MetaCons "Cons" 'PrefixI 'False)
        (S1
           ('MetaSel
              'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
           (Rec0 a)
         :*: S1
               ('MetaSel
                  'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
               (Rec0 (Vec (0 - 1) a))))
     x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (U1 x -> M1 C ('MetaCons "Nil" 'PrefixI 'False) U1 x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 U1 x
forall k (p :: k). U1 p
U1))
  from (Cons x :: a
x xs :: Vec n a
xs) = (:+:)
  (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1)
  (M1
     C
     ('MetaCons "Cons" 'PrefixI 'False)
     (S1
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        (Rec0 a)
      :*: M1
            S
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (K1 R (Vec n a))))
  x
-> M1
     D
     ('MetaData "Vec" "Clash.Data.Vector" "clash-prelude" 'False)
     (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1
      :+: M1
            C
            ('MetaCons "Cons" 'PrefixI 'False)
            (S1
               ('MetaSel
                  'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
               (Rec0 a)
             :*: M1
                   S
                   ('MetaSel
                      'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                   (K1 R (Vec n a))))
     x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (M1
  C
  ('MetaCons "Cons" 'PrefixI 'False)
  (S1
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (Rec0 a)
   :*: M1
         S
         ('MetaSel
            'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
         (K1 R (Vec n a)))
  x
-> (:+:)
     (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1)
     (M1
        C
        ('MetaCons "Cons" 'PrefixI 'False)
        (S1
           ('MetaSel
              'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
           (Rec0 a)
         :*: M1
               S
               ('MetaSel
                  'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
               (K1 R (Vec n a))))
     x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 ((:*:)
  (S1
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (Rec0 a))
  (M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (K1 R (Vec n a)))
  x
-> M1
     C
     ('MetaCons "Cons" 'PrefixI 'False)
     (S1
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        (Rec0 a)
      :*: M1
            S
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (K1 R (Vec n a)))
     x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (K1 R a x
-> M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (Rec0 a)
     x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (a -> K1 R a x
forall k i c (p :: k). c -> K1 i c p
K1 a
x) M1
  S
  ('MetaSel
     'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
  (Rec0 a)
  x
-> M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (K1 R (Vec n a))
     x
-> (:*:)
     (S1
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        (Rec0 a))
     (M1
        S
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        (K1 R (Vec n a)))
     x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: K1 R (Vec n a) x
-> M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (K1 R (Vec n a))
     x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (Vec n a -> K1 R (Vec n a) x
forall k i c (p :: k). c -> K1 i c p
K1 Vec n a
xs))))
  to :: Rep (Vec n a) x -> Vec n a
to (M1 g) = case SNat n -> SNat 0 -> SNatLE n 0
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat @n) (KnownNat 0 => SNat 0
forall (n :: Nat). KnownNat n => SNat n
SNat @0) of
    SNatLE -> case (n <= 0) :- (n ~ 0)
forall (a :: Nat). (a <= 0) :- (a ~ 0)
leZero @n of
      Sub Dict -> Vec n a
forall a. Vec 0 a
Nil
    SNatGT -> case (:+:)
  (M1 C ('MetaCons "Nil" 'PrefixI 'False) U1)
  (C1
     ('MetaCons "Cons" 'PrefixI 'False)
     (S1
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        (Rec0 a)
      :*: S1
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (Rec0 (Vec (n - 1) a))))
  x
g of
      R1 (M1 (M1 (K1 p) :*: M1 (K1 q))) -> a -> Vec (n - 1) a -> Vec ((n - 1) + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
Cons a
p Vec (n - 1) a
q

instance (KnownNat n, Typeable a, Data a) => Data (Vec n a) where
  gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Vec n a)
gunfold k :: forall b r. Data b => c (b -> r) -> c r
k z :: forall r. r -> c r
z _ = case SNat n -> SNat 0 -> SNatLE n 0
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat @n) (KnownNat 0 => SNat 0
forall (n :: Nat). KnownNat n => SNat n
SNat @0) of
    SNatLE -> case (n <= 0) :- (n ~ 0)
forall (a :: Nat). (a <= 0) :- (a ~ 0)
leZero @n of
      Sub Dict -> Vec 0 a -> c (Vec 0 a)
forall r. r -> c r
z Vec 0 a
forall a. Vec 0 a
Nil
    SNatGT -> c (Vec (n - 1) a -> Vec n a) -> c (Vec n a)
forall b r. Data b => c (b -> r) -> c r
k (c (a -> Vec (n - 1) a -> Vec n a) -> c (Vec (n - 1) a -> Vec n a)
forall b r. Data b => c (b -> r) -> c r
k ((a -> Vec (n - 1) a -> Vec n a)
-> c (a -> Vec (n - 1) a -> Vec n a)
forall r. r -> c r
z @(a -> Vec (n-1) a -> Vec n a) a -> Vec (n - 1) a -> Vec n a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
Cons))
  toConstr :: Vec n a -> Constr
toConstr Nil        = Constr
cNil
  toConstr (Cons _ _) = Constr
cCons
  dataTypeOf :: Vec n a -> DataType
dataTypeOf _        = DataType
tVec

  gfoldl
    :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> Vec n a
    -> c (Vec n a)
  gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Vec n a -> c (Vec n a)
gfoldl f :: forall d b. Data d => c (d -> b) -> d -> c b
f z :: forall g. g -> c g
z xs :: Vec n a
xs = case SNat n -> SNat 0 -> SNatLE n 0
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat @n) (KnownNat 0 => SNat 0
forall (n :: Nat). KnownNat n => SNat n
SNat @0) of
    SNatLE -> case (n <= 0) :- (n ~ 0)
forall (a :: Nat). (a <= 0) :- (a ~ 0)
leZero @n of
                  Sub Dict -> Vec 0 a -> c (Vec 0 a)
forall g. g -> c g
z Vec 0 a
forall a. Vec 0 a
Nil
    SNatGT -> let (y :: a
y :> ys :: Vec (n - 1) a
ys) = Vec n a
Vec ((n - 1) + 1) a
xs
              in ((a -> Vec (n - 1) a -> Vec n a)
-> c (a -> Vec (n - 1) a -> Vec n a)
forall g. g -> c g
z @(a -> Vec (n-1) a -> Vec n a) a -> Vec (n - 1) a -> Vec n a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
(:>) c (a -> Vec (n - 1) a -> Vec n a)
-> a -> c (Vec (n - 1) a -> Vec n a)
forall d b. Data d => c (d -> b) -> d -> c b
`f` a
y c (Vec (n - 1) a -> Vec n a) -> Vec (n - 1) a -> c (Vec n a)
forall d b. Data d => c (d -> b) -> d -> c b
`f` Vec (n - 1) a
ys)

tVec :: DataType
tVec :: DataType
tVec = String -> [Constr] -> DataType
mkDataType "Vec" [Constr
cNil, Constr
cCons]

cNil :: Constr
cNil :: Constr
cNil = DataType -> String -> [String] -> Fixity -> Constr
mkConstr DataType
tVec "Nil" [] Fixity
Prefix

cCons :: Constr
cCons :: Constr
cCons = DataType -> String -> [String] -> Fixity -> Constr
mkConstr DataType
tVec "Cons" [] Fixity
Prefix

instance NFData a => NFData (Vec n a) where
  rnf :: Vec n a -> ()
rnf = (() -> a -> ()) -> () -> Vec n a -> ()
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl (\() -> a -> ()
forall a. NFData a => a -> ()
rnf) ()

-- | Add an element to the head of a vector.
--
-- >>> 3:>4:>5:>Nil
-- <3,4,5>
-- >>> let x = 3:>4:>5:>Nil
-- >>> :t x
-- x :: Num a => Vec 3 a
--
-- Can be used as a pattern:
--
-- >>> let f (x :> y :> _) = x + y
-- >>> :t f
-- f :: Num a => Vec ((n + 1) + 1) a -> a
-- >>> f (3:>4:>5:>6:>7:>Nil)
-- 7
--
-- Also in conjunctions with (':<'):
--
-- >>> let g (a :> b :> (_ :< y :< x)) = a + b +  x + y
-- >>> :t g
-- g :: Num a => Vec ((((n + 1) + 1) + 1) + 1) a -> a
-- >>> g (1:>2:>3:>4:>5:>Nil)
-- 12
pattern (:>) :: a -> Vec n a -> Vec (n + 1) a
pattern $b:> :: a -> Vec n a -> Vec (n + 1) a
$m:> :: forall r a (n :: Nat).
Vec (n + 1) a -> (a -> Vec n a -> r) -> (Void# -> r) -> r
(:>) x xs <- ((\ys -> (head ys,tail ys)) -> (x,xs))
  where
    (:>) x :: a
x xs :: Vec n a
xs = a -> Vec n a -> Vec (n + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
Cons a
x Vec n a
xs

infixr 5 :>

instance Show a => Show (Vec n a) where
  showsPrec :: Int -> Vec n a -> ShowS
showsPrec _ vs :: Vec n a
vs = \s :: String
s -> '<'Char -> ShowS
forall a. a -> [a] -> [a]
:Vec n a -> ShowS
forall (m :: Nat). Vec m a -> ShowS
punc Vec n a
vs ('>'Char -> ShowS
forall a. a -> [a] -> [a]
:String
s)
    where
      punc :: Vec m a -> ShowS
      punc :: Vec m a -> ShowS
punc Nil            = ShowS
forall a. a -> a
id
      punc (x :: a
x `Cons` Nil) = a -> ShowS
forall a. Show a => a -> ShowS
shows a
x
      punc (x :: a
x `Cons` xs :: Vec n a
xs)  = \s :: String
s -> a -> ShowS
forall a. Show a => a -> ShowS
shows a
x (','Char -> ShowS
forall a. a -> [a] -> [a]
:Vec n a -> ShowS
forall (m :: Nat). Vec m a -> ShowS
punc Vec n a
xs String
s)

instance ShowX a => ShowX (Vec n a) where
  showsPrecX :: Int -> Vec n a -> ShowS
showsPrecX = (Int -> Vec n a -> ShowS) -> Int -> Vec n a -> ShowS
forall a. (Int -> a -> ShowS) -> Int -> a -> ShowS
showsPrecXWith Int -> Vec n a -> ShowS
go
    where
      go :: Int -> Vec n a -> ShowS
go _ vs :: Vec n a
vs = \s :: String
s -> '<'Char -> ShowS
forall a. a -> [a] -> [a]
: Vec n a -> ShowS
forall (m :: Nat). Vec m a -> ShowS
punc Vec n a
vs ('>'Char -> ShowS
forall a. a -> [a] -> [a]
:String
s)
        where
          punc :: Vec m a -> ShowS
          punc :: Vec m a -> ShowS
punc Nil            = ShowS
forall a. a -> a
id
          punc (x :: a
x `Cons` Nil) = a -> ShowS
forall a. ShowX a => a -> ShowS
showsX a
x
          punc (x :: a
x `Cons` xs :: Vec n a
xs)  = \s :: String
s -> a -> ShowS
forall a. ShowX a => a -> ShowS
showsX a
x (','Char -> ShowS
forall a. a -> [a] -> [a]
:Vec n a -> ShowS
forall (m :: Nat). Vec m a -> ShowS
punc Vec n a
xs String
s)

instance (KnownNat n, Eq a) => Eq (Vec n a) where
  == :: Vec n a -> Vec n a -> Bool
(==) Nil _            = Bool
True
  (==) v1 :: Vec n a
v1@(Cons _ _) v2 :: Vec n a
v2 = (Bool -> Bool -> Bool) -> Vec (n + 1) Bool -> Bool
forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
fold Bool -> Bool -> Bool
(&&) ((a -> a -> Bool) -> Vec n a -> Vec n a -> Vec n Bool
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) Vec n a
v1 Vec n a
v2)

instance (KnownNat n, Ord a) => Ord (Vec n a) where
  compare :: Vec n a -> Vec n a -> Ordering
compare x :: Vec n a
x y :: Vec n a
y = (Ordering -> Ordering -> Ordering)
-> Ordering -> Vec n Ordering -> Ordering
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr Ordering -> Ordering -> Ordering
f Ordering
EQ (Vec n Ordering -> Ordering) -> Vec n Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ (a -> a -> Ordering) -> Vec n a -> Vec n a -> Vec n Ordering
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Vec n a
x Vec n a
y
    where f :: Ordering -> Ordering -> Ordering
f EQ   keepGoing :: Ordering
keepGoing = Ordering
keepGoing
          f done :: Ordering
done _         = Ordering
done

instance KnownNat n => Applicative (Vec n) where
  pure :: a -> Vec n a
pure      = a -> Vec n a
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat
  fs :: Vec n (a -> b)
fs <*> :: Vec n (a -> b) -> Vec n a -> Vec n b
<*> xs :: Vec n a
xs = ((a -> b) -> a -> b) -> Vec n (a -> b) -> Vec n a -> Vec n b
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($) Vec n (a -> b)
fs Vec n a
xs

{-# RULES
"zipWith$map" forall f xs ys. zipWith (\g a -> g a) (map f xs) ys = zipWith f xs ys
  #-}

instance (KnownNat n, 1 <= n) => F.Foldable (Vec n) where
  fold :: Vec n m -> m
fold      = forall r. (1 <= n) => (forall (m :: Nat). (n ~ (1 + m)) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n) =>
(forall (m :: Nat). (n ~ (k + m)) => r) -> r
leToPlus @1 @n ((forall (m :: Nat). (n ~ (1 + m)) => Vec n m -> m)
 -> Vec n m -> m)
-> (forall (m :: Nat). (n ~ (1 + m)) => Vec n m -> m)
-> Vec n m
-> m
forall a b. (a -> b) -> a -> b
$ (m -> m -> m) -> Vec (m + 1) m -> m
forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
fold m -> m -> m
forall a. Monoid a => a -> a -> a
mappend
  foldMap :: (a -> m) -> Vec n a -> m
foldMap f :: a -> m
f = forall r. (1 <= n) => (forall (m :: Nat). (n ~ (1 + m)) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n) =>
(forall (m :: Nat). (n ~ (k + m)) => r) -> r
leToPlus @1 @n ((forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> m)
 -> Vec n a -> m)
-> (forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> m)
-> Vec n a
-> m
forall a b. (a -> b) -> a -> b
$ (m -> m -> m) -> Vec (m + 1) m -> m
forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
fold m -> m -> m
forall a. Monoid a => a -> a -> a
mappend (Vec n m -> m) -> (Vec n a -> Vec n m) -> Vec n a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m) -> Vec n a -> Vec n m
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map a -> m
f
  foldr :: (a -> b -> b) -> b -> Vec n a -> b
foldr     = (a -> b -> b) -> b -> Vec n a -> b
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr
  foldl :: (b -> a -> b) -> b -> Vec n a -> b
foldl     = (b -> a -> b) -> b -> Vec n a -> b
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl
  foldr1 :: (a -> a -> a) -> Vec n a -> a
foldr1 f :: a -> a -> a
f  = forall r. (1 <= n) => (forall (m :: Nat). (n ~ (1 + m)) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n) =>
(forall (m :: Nat). (n ~ (k + m)) => r) -> r
leToPlus @1 @n ((forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
 -> Vec n a -> a)
-> (forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
-> Vec n a
-> a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> Vec (m + 1) a -> a
forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
foldr1 a -> a -> a
f
  foldl1 :: (a -> a -> a) -> Vec n a -> a
foldl1 f :: a -> a -> a
f  = forall r. (1 <= n) => (forall (m :: Nat). (n ~ (1 + m)) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n) =>
(forall (m :: Nat). (n ~ (k + m)) => r) -> r
leToPlus @1 @n ((forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
 -> Vec n a -> a)
-> (forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
-> Vec n a
-> a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> Vec (m + 1) a -> a
forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
foldl1 a -> a -> a
f
  toList :: Vec n a -> [a]
toList    = Vec n a -> [a]
forall (n :: Nat) a. Vec n a -> [a]
toList
  null :: Vec n a -> Bool
null _    = Bool
False
  length :: Vec n a -> Int
length    = Vec n a -> Int
forall (n :: Nat) a. KnownNat n => Vec n a -> Int
length
  maximum :: Vec n a -> a
maximum   = forall r. (1 <= n) => (forall (m :: Nat). (n ~ (1 + m)) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n) =>
(forall (m :: Nat). (n ~ (k + m)) => r) -> r
leToPlus @1 @n ((forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
 -> Vec n a -> a)
-> (forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
-> Vec n a
-> a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> Vec (m + 1) a -> a
forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
fold (\x :: a
x y :: a
y -> if a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y then a
x else a
y)
  minimum :: Vec n a -> a
minimum   = forall r. (1 <= n) => (forall (m :: Nat). (n ~ (1 + m)) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n) =>
(forall (m :: Nat). (n ~ (k + m)) => r) -> r
leToPlus @1 @n ((forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
 -> Vec n a -> a)
-> (forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
-> Vec n a
-> a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> Vec (m + 1) a -> a
forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
fold (\x :: a
x y :: a
y -> if a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y then a
x else a
y)
  sum :: Vec n a -> a
sum       = forall r. (1 <= n) => (forall (m :: Nat). (n ~ (1 + m)) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n) =>
(forall (m :: Nat). (n ~ (k + m)) => r) -> r
leToPlus @1 @n ((forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
 -> Vec n a -> a)
-> (forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
-> Vec n a
-> a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> Vec (m + 1) a -> a
forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
fold a -> a -> a
forall a. Num a => a -> a -> a
(+)
  product :: Vec n a -> a
product   = forall r. (1 <= n) => (forall (m :: Nat). (n ~ (1 + m)) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n) =>
(forall (m :: Nat). (n ~ (k + m)) => r) -> r
leToPlus @1 @n ((forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
 -> Vec n a -> a)
-> (forall (m :: Nat). (n ~ (1 + m)) => Vec n a -> a)
-> Vec n a
-> a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> Vec (m + 1) a -> a
forall a (n :: Nat). (a -> a -> a) -> Vec (n + 1) a -> a
fold a -> a -> a
forall a. Num a => a -> a -> a
(*)

instance Functor (Vec n) where
  fmap :: (a -> b) -> Vec n a -> Vec n b
fmap = (a -> b) -> Vec n a -> Vec n b
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map

instance (KnownNat n, 1 <= n) => Traversable (Vec n) where
  traverse :: (a -> f b) -> Vec n a -> f (Vec n b)
traverse = (a -> f b) -> Vec n a -> f (Vec n b)
forall a (f :: Type -> Type) b (n :: Nat).
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse#

{-# NOINLINE traverse# #-}
traverse# :: forall a f b n . Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)
traverse# :: (a -> f b) -> Vec n a -> f (Vec n b)
traverse# _ Nil           = Vec 0 b -> f (Vec 0 b)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Vec 0 b
forall a. Vec 0 a
Nil
traverse# f :: a -> f b
f (x :: a
x `Cons` xs :: Vec n a
xs) = b -> Vec n b -> Vec n b
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
Cons (b -> Vec n b -> Vec n b) -> f b -> f (Vec n b -> Vec n b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x f (Vec n b -> Vec n b) -> f (Vec n b) -> f (Vec n b)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (a -> f b) -> Vec n a -> f (Vec n b)
forall a (f :: Type -> Type) b (n :: Nat).
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse# a -> f b
f Vec n a
xs

instance (Default a, KnownNat n) => Default (Vec n a) where
  def :: Vec n a
def = a -> Vec n a
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat a
forall a. Default a => a
def

instance (NFDataX a, KnownNat n) => NFDataX (Vec n a) where
  deepErrorX :: String -> Vec n a
deepErrorX x :: String
x = a -> Vec n a
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat (String -> a
forall a. (NFDataX a, HasCallStack) => String -> a
deepErrorX String
x)

  rnfX :: Vec n a -> ()
rnfX v :: Vec n a
v =
    -- foldl will fail if the spine of the vector is undefined, so we need to
    -- seqX the result of it. We need to use foldl so Clash won't treat it as
    -- a recursive function.
    () -> () -> ()
forall a b. a -> b -> b
seqX ((() -> a -> ()) -> () -> Vec n a -> ()
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl (\() -> a -> ()
forall a. NFDataX a => a -> ()
rnfX) () Vec n a
v) ()

  hasUndefined :: Vec n a -> Bool
hasUndefined v :: Vec n a
v =
    if Either String (Vec n a) -> Bool
forall a b. Either a b -> Bool
isLeft (Vec n a -> Either String (Vec n a)
forall a. a -> Either String a
isX Vec n a
v) then Bool
True else Vec n a -> Bool
forall (m :: Nat) b. (NFDataX b, KnownNat m) => Vec m b -> Bool
go Vec n a
v
   where
    go :: forall m b . (NFDataX b, KnownNat m) => Vec m b -> Bool
    go :: Vec m b -> Bool
go Nil = Bool
False
    go (x :: b
x `Cons` xs :: Vec n b
xs) = b -> Bool
forall a. NFDataX a => a -> Bool
hasUndefined b
x Bool -> Bool -> Bool
|| Vec n b -> Bool
forall a. NFDataX a => a -> Bool
hasUndefined Vec n b
xs

  ensureSpine :: Vec n a -> Vec n a
ensureSpine = (a -> a) -> Vec n a -> Vec n a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map a -> a
forall a. NFDataX a => a -> a
ensureSpine (Vec n a -> Vec n a) -> (Vec n a -> Vec n a) -> Vec n a -> Vec n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec n a -> Vec n a
forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
lazyV

{-# INLINE singleton #-}
-- | Create a vector of one element
--
-- >>> singleton 5
-- <5>
singleton :: a -> Vec 1 a
singleton :: a -> Vec 1 a
singleton = (a -> Vec 0 a -> Vec (0 + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Vec 0 a
forall a. Vec 0 a
Nil)

{-# NOINLINE head #-}
-- | Extract the first element of a vector
--
-- >>> head (1:>2:>3:>Nil)
-- 1
-- >>> head Nil
-- <BLANKLINE>
-- <interactive>:...
--     • Couldn't match type ‘1’ with ‘0’
--       Expected type: Vec (0 + 1) a
--         Actual type: Vec 0 a
--     • In the first argument of ‘head’, namely ‘Nil’
--       In the expression: head Nil
--       In an equation for ‘it’: it = head Nil
head :: Vec (n + 1) a -> a
head :: Vec (n + 1) a -> a
head (x :: a
x `Cons` _) = a
x

{-# NOINLINE tail #-}
-- | Extract the elements after the head of a vector
--
-- >>> tail (1:>2:>3:>Nil)
-- <2,3>
-- >>> tail Nil
-- <BLANKLINE>
-- <interactive>:...
--     • Couldn't match type ‘1’ with ‘0’
--       Expected type: Vec (0 + 1) a
--         Actual type: Vec 0 a
--     • In the first argument of ‘tail’, namely ‘Nil’
--       In the expression: tail Nil
--       In an equation for ‘it’: it = tail Nil
tail :: Vec (n + 1) a -> Vec n a
tail :: Vec (n + 1) a -> Vec n a
tail (_ `Cons` xs :: Vec n a
xs) = Vec n a
Vec n a
xs

{-# NOINLINE last #-}
-- | Extract the last element of a vector
--
-- >>> last (1:>2:>3:>Nil)
-- 3
-- >>> last Nil
-- <BLANKLINE>
-- <interactive>:...
--     • Couldn't match type ‘1’ with ‘0’
--       Expected type: Vec (0 + 1) a
--         Actual type: Vec 0 a
--     • In the first argument of ‘last’, namely ‘Nil’
--       In the expression: last Nil
--       In an equation for ‘it’: it = last Nil
last :: Vec (n + 1) a -> a
last :: Vec (n + 1) a -> a
last (x :: a
x `Cons` Nil)         = a
x
last (_ `Cons` y :: a
y `Cons` ys :: Vec n a
ys) = Vec (n + 1) a -> a
forall (n :: Nat) a. Vec (n + 1) a -> a
last (a
y a -> Vec n a -> Vec (n + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Vec n a
ys)

{-# NOINLINE init #-}
-- | Extract all the elements of a vector except the last element
--
-- >>> init (1:>2:>3:>Nil)
-- <1,2>
-- >>> init Nil
-- <BLANKLINE>
-- <interactive>:...
--     • Couldn't match type ‘1’ with ‘0’
--       Expected type: Vec (0 + 1) a
--         Actual type: Vec 0 a
--     • In the first argument of ‘init’, namely ‘Nil’
--       In the expression: init Nil
--       In an equation for ‘it’: it = init Nil
init :: Vec (n + 1) a -> Vec n a
init :: Vec (n + 1) a -> Vec n a
init (_ `Cons` Nil)         = Vec n a
forall a. Vec 0 a
Nil
init (x :: a
x `Cons` y :: a
y `Cons` ys :: Vec n a
ys) = a
x a -> Vec n a -> Vec (n + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Vec (n + 1) a -> Vec n a
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
init (a
y a -> Vec n a -> Vec (n + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Vec n a
ys)

{-# INLINE shiftInAt0 #-}
-- | Shift in elements to the head of a vector, bumping out elements at the
-- tail. The result is a tuple containing:
--
-- * The new vector
-- * The shifted out elements
--
-- >>> shiftInAt0 (1 :> 2 :> 3 :> 4 :> Nil) ((-1) :> 0 :> Nil)
-- (<-1,0,1,2>,<3,4>)
-- >>> shiftInAt0 (1 :> Nil) ((-1) :> 0 :> Nil)
-- (<-1>,<0,1>)
shiftInAt0 :: KnownNat n
           => Vec n a -- ^ The old vector
           -> Vec m a -- ^ The elements to shift in at the head
           -> (Vec n a, Vec m a) -- ^ (The new vector, shifted out elements)
shiftInAt0 :: Vec n a -> Vec m a -> (Vec n a, Vec m a)
shiftInAt0 xs :: Vec n a
xs ys :: Vec m a
ys = Vec (n + m) a -> (Vec n a, Vec m a)
forall (m :: Nat) (n :: Nat) a.
KnownNat m =>
Vec (m + n) a -> (Vec m a, Vec n a)
splitAtI Vec (n + m) a
Vec (m + n) a
zs
  where
    zs :: Vec (m + n) a
zs = Vec m a
ys Vec m a -> Vec n a -> Vec (m + n) a
forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
++ Vec n a
xs

{-# INLINE shiftInAtN #-}
-- | Shift in element to the tail of a vector, bumping out elements at the head.
-- The result is a tuple containing:
--
-- * The new vector
-- * The shifted out elements
--
-- >>> shiftInAtN (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> Nil)
-- (<3,4,5,6>,<1,2>)
-- >>> shiftInAtN (1 :> Nil) (2 :> 3 :> Nil)
-- (<3>,<1,2>)
shiftInAtN :: KnownNat m
           => Vec n a -- ^ The old vector
           -> Vec m a -- ^ The elements to shift in at the tail
           -> (Vec n a,Vec m a) -- ^ (The new vector, shifted out elements)
shiftInAtN :: Vec n a -> Vec m a -> (Vec n a, Vec m a)
shiftInAtN xs :: Vec n a
xs ys :: Vec m a
ys = (Vec n a
zsR, Vec m a
zsL)
  where
    zs :: Vec (n + m) a
zs        = Vec n a
xs Vec n a -> Vec m a -> Vec (n + m) a
forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
++ Vec m a
ys
    (zsL :: Vec m a
zsL,zsR :: Vec n a
zsR) = Vec (m + n) a -> (Vec m a, Vec n a)
forall (m :: Nat) (n :: Nat) a.
KnownNat m =>
Vec (m + n) a -> (Vec m a, Vec n a)
splitAtI Vec (m + n) a
Vec (n + m) a
zs

infixl 5 :<
-- | Add an element to the tail of a vector.
--
-- >>> (3:>4:>5:>Nil) :< 1
-- <3,4,5,1>
-- >>> let x = (3:>4:>5:>Nil) :< 1
-- >>> :t x
-- x :: Num a => Vec 4 a
--
-- Can be used as a pattern:
--
-- >>> let f (_ :< y :< x) = y + x
-- >>> :t f
-- f :: Num a => Vec ((n + 1) + 1) a -> a
-- >>> f (3:>4:>5:>6:>7:>Nil)
-- 13
--
-- Also in conjunctions with (':>'):
--
-- >>> let g (a :> b :> (_ :< y :< x)) = a + b +  x + y
-- >>> :t g
-- g :: Num a => Vec ((((n + 1) + 1) + 1) + 1) a -> a
-- >>> g (1:>2:>3:>4:>5:>Nil)
-- 12
pattern (:<) :: Vec n a -> a -> Vec (n+1) a
pattern $b:< :: Vec n a -> a -> Vec (n + 1) a
$m:< :: forall r (n :: Nat) a.
Vec (n + 1) a -> (Vec n a -> a -> r) -> (Void# -> r) -> r
(:<) xs x <- ((\ys -> (init ys,last ys)) -> (xs,x))
  where
    (:<) xs :: Vec n a
xs x :: a
x = Vec n a
xs Vec n a -> Vec 1 a -> Vec (n + 1) a
forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
++ a -> Vec 1 a
forall a. a -> Vec 1 a
singleton a
x

infixr 4 +>>
-- | Add an element to the head of a vector, and extract all but the last
-- element.
--
-- >>> 1 +>> (3:>4:>5:>Nil)
-- <1,3,4>
-- >>> 1 +>> Nil
-- <>
(+>>) :: KnownNat n => a -> Vec n a -> Vec n a
s :: a
s +>> :: a -> Vec n a -> Vec n a
+>> xs :: Vec n a
xs = (Vec n a, Vec 1 a) -> Vec n a
forall a b. (a, b) -> a
fst (Vec n a -> Vec 1 a -> (Vec n a, Vec 1 a)
forall (n :: Nat) a (m :: Nat).
KnownNat n =>
Vec n a -> Vec m a -> (Vec n a, Vec m a)
shiftInAt0 Vec n a
xs (a -> Vec 1 a
forall a. a -> Vec 1 a
singleton a
s))
{-# INLINE (+>>) #-}


infixl 4 <<+
-- | Add an element to the tail of a vector, and extract all but the first
-- element.
--
-- >>> (3:>4:>5:>Nil) <<+ 1
-- <4,5,1>
-- >>> Nil <<+ 1
-- <>
(<<+) :: Vec n a -> a -> Vec n a
xs :: Vec n a
xs <<+ :: Vec n a -> a -> Vec n a
<<+ s :: a
s = (Vec n a, Vec 1 a) -> Vec n a
forall a b. (a, b) -> a
fst (Vec n a -> Vec 1 a -> (Vec n a, Vec 1 a)
forall (m :: Nat) (n :: Nat) a.
KnownNat m =>
Vec n a -> Vec m a -> (Vec n a, Vec m a)
shiftInAtN Vec n a
xs (a -> Vec 1 a
forall a. a -> Vec 1 a
singleton a
s))
{-# INLINE (<<+) #-}

-- | Shift /m/ elements out from the head of a vector, filling up the tail with
-- 'Default' values. The result is a tuple containing:
--
-- * The new vector
-- * The shifted out values
--
-- >>> shiftOutFrom0 d2 ((1 :> 2 :> 3 :> 4 :> 5 :> Nil) :: Vec 5 Integer)
-- (<3,4,5,0,0>,<1,2>)
shiftOutFrom0 :: (Default a, KnownNat m)
              => SNat m        -- ^ @m@, the number of elements to shift out
              -> Vec (m + n) a -- ^ The old vector
              -> (Vec (m + n) a, Vec m a)
              -- ^ (The new vector, shifted out elements)
shiftOutFrom0 :: SNat m -> Vec (m + n) a -> (Vec (m + n) a, Vec m a)
shiftOutFrom0 m :: SNat m
m xs :: Vec (m + n) a
xs = Vec (m + n) a -> Vec m a -> (Vec (m + n) a, Vec m a)
forall (m :: Nat) (n :: Nat) a.
KnownNat m =>
Vec n a -> Vec m a -> (Vec n a, Vec m a)
shiftInAtN Vec (m + n) a
xs (SNat m -> a -> Vec m a
forall (n :: Nat) a. SNat n -> a -> Vec n a
replicate SNat m
m a
forall a. Default a => a
def)
{-# INLINE shiftOutFrom0 #-}

-- | Shift /m/ elements out from the tail of a vector, filling up the head with
-- 'Default' values. The result is a tuple containing:
--
-- * The new vector
-- * The shifted out values
--
-- >>> shiftOutFromN d2 ((1 :> 2 :> 3 :> 4 :> 5 :> Nil) :: Vec 5 Integer)
-- (<0,0,1,2,3>,<4,5>)
shiftOutFromN :: (Default a, KnownNat n)
              => SNat m        -- ^ @m@, the number of elements to shift out
              -> Vec (m + n) a -- ^ The old vector
              -> (Vec (m + n) a, Vec m a)
              -- ^ (The new vector, shifted out elements)
shiftOutFromN :: SNat m -> Vec (m + n) a -> (Vec (m + n) a, Vec m a)
shiftOutFromN m :: SNat m
m@SNat m
SNat xs :: Vec (m + n) a
xs = Vec (m + n) a -> Vec m a -> (Vec (m + n) a, Vec m a)
forall (n :: Nat) a (m :: Nat).
KnownNat n =>
Vec n a -> Vec m a -> (Vec n a, Vec m a)
shiftInAt0 Vec (m + n) a
xs (SNat m -> a -> Vec m a
forall (n :: Nat) a. SNat n -> a -> Vec n a
replicate SNat m
m a
forall a. Default a => a
def)
{-# INLINE shiftOutFromN #-}

infixr 5 ++
-- | Append two vectors.
--
-- >>> (1:>2:>3:>Nil) ++ (7:>8:>Nil)
-- <1,2,3,7,8>
(++) :: Vec n a -> Vec m a -> Vec (n + m) a
Nil           ++ :: Vec n a -> Vec m a -> Vec (n + m) a
++ ys :: Vec m a
ys = Vec m a
Vec (n + m) a
ys
(x :: a
x `Cons` xs :: Vec n a
xs) ++ ys :: Vec m a
ys = a
x a -> Vec (n + m) a -> Vec ((n + m) + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Vec n a
xs Vec n a -> Vec m a -> Vec (n + m) a
forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
++ Vec m a
ys
{-# NOINLINE (++) #-}

-- | Split a vector into two vectors at the given point.
--
-- >>> splitAt (SNat :: SNat 3) (1:>2:>3:>7:>8:>Nil)
-- (<1,2,3>,<7,8>)
-- >>> splitAt d3 (1:>2:>3:>7:>8:>Nil)
-- (<1,2,3>,<7,8>)
splitAt :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAt :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAt n :: SNat m
n xs :: Vec (m + n) a
xs = UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
forall (m :: Nat) (n :: Nat) a.
UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAtU (SNat m -> UNat m
forall (n :: Nat). SNat n -> UNat n
toUNat SNat m
n) Vec (m + n) a
xs
{-# NOINLINE splitAt #-}

splitAtU :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAtU :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAtU UZero     ys :: Vec (m + n) a
ys            = (Vec m a
forall a. Vec 0 a
Nil,Vec n a
Vec (m + n) a
ys)
splitAtU (USucc s :: UNat n
s) (y :: a
y `Cons` ys :: Vec n a
ys) = let (as :: Vec n a
as,bs :: Vec n a
bs) = UNat n -> Vec (n + n) a -> (Vec n a, Vec n a)
forall (m :: Nat) (n :: Nat) a.
UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAtU UNat n
s Vec n a
Vec (n + n) a
ys
                                   in  (a
y a -> Vec n a -> Vec (n + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Vec n a
as, Vec n a
bs)

-- | Split a vector into two vectors where the length of the two is determined
-- by the context.
--
-- >>> splitAtI (1:>2:>3:>7:>8:>Nil) :: (Vec 2 Int, Vec 3 Int)
-- (<1,2>,<3,7,8>)
splitAtI :: KnownNat m => Vec (m + n) a -> (Vec m a, Vec n a)
splitAtI :: Vec (m + n) a -> (Vec m a, Vec n a)
splitAtI = (SNat m -> Vec (m + n) a -> (Vec m a, Vec n a))
-> Vec (m + n) a -> (Vec m a, Vec n a)
forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
withSNat SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
forall (m :: Nat) (n :: Nat) a.
SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAt
{-# INLINE splitAtI #-}

-- | Concatenate a vector of vectors.
--
-- >>> concat ((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>
concat :: Vec n (Vec m a) -> Vec (n * m) a
concat :: Vec n (Vec m a) -> Vec (n * m) a
concat Nil           = Vec (n * m) a
forall a. Vec 0 a
Nil
concat (x :: Vec m a
x `Cons` xs :: Vec n (Vec m a)
xs) = Vec m a
x Vec m a -> Vec (n * m) a -> Vec (m + (n * m)) a
forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
++ Vec n (Vec m a) -> Vec (n * m) a
forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (n * m) a
concat Vec n (Vec m a)
xs
{-# NOINLINE concat #-}

-- | Map a function over all the elements of a vector and concatentate the resulting vectors.
--
-- >>> concatMap (replicate d3) (1:>2:>3:>Nil)
-- <1,1,1,2,2,2,3,3,3>
concatMap :: (a -> Vec m b) -> Vec n a -> Vec (n * m) b
concatMap :: (a -> Vec m b) -> Vec n a -> Vec (n * m) b
concatMap f :: a -> Vec m b
f xs :: Vec n a
xs = Vec n (Vec m b) -> Vec (n * m) b
forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (n * m) a
concat ((a -> Vec m b) -> Vec n a -> Vec n (Vec m b)
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map a -> Vec m b
f Vec n a
xs)
{-# INLINE concatMap #-}

-- | Split a vector of \(n * m)\ elements into a vector of \"vectors of length
-- /m/\", where the length /m/ is given.
--
-- >>> unconcat d4 (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)
-- <<1,2,3,4>,<5,6,7,8>,<9,10,11,12>>
unconcat :: KnownNat n => SNat m -> Vec (n * m) a -> Vec n (Vec m a)
unconcat :: SNat m -> Vec (n * m) a -> Vec n (Vec m a)
unconcat n :: SNat m
n xs :: Vec (n * m) a
xs = UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
forall (n :: Nat) (m :: Nat) a.
UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
unconcatU ((SNat n -> UNat n) -> UNat n
forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
withSNat SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat) (SNat m -> UNat m
forall (n :: Nat). SNat n -> UNat n
toUNat SNat m
n) Vec (n * m) a
xs
{-# NOINLINE unconcat #-}

unconcatU :: UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
unconcatU :: UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
unconcatU UZero      _ _  = Vec n (Vec m a)
forall a. Vec 0 a
Nil
unconcatU (USucc n' :: UNat n
n') m :: UNat m
m ys :: Vec (n * m) a
ys = let (as :: Vec m a
as,bs :: Vec (n * m) a
bs) = UNat m -> Vec (m + (n * m)) a -> (Vec m a, Vec (n * m) a)
forall (m :: Nat) (n :: Nat) a.
UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAtU UNat m
m Vec (m + (n * m)) a
Vec (n * m) a
ys
                            in  Vec m a
as Vec m a -> Vec n (Vec m a) -> Vec (n + 1) (Vec m a)
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
forall (n :: Nat) (m :: Nat) a.
UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
unconcatU UNat n
n' UNat m
m Vec (n * m) a
bs

-- | Split a vector of /(n * m)/ elements into a vector of \"vectors of length
-- /m/\", where the length /m/ is determined by the context.
--
-- >>> unconcatI (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) :: Vec 2 (Vec 6 Int)
-- <<1,2,3,4,5,6>,<7,8,9,10,11,12>>
unconcatI :: (KnownNat n, KnownNat m) => Vec (n * m) a -> Vec n (Vec m a)
unconcatI :: Vec (n * m) a -> Vec n (Vec m a)
unconcatI = (SNat m -> Vec (n * m) a -> Vec n (Vec m a))
-> Vec (n * m) a -> Vec n (Vec m a)
forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
withSNat SNat m -> Vec (n * m) a -> Vec n (Vec m a)
forall (n :: Nat) (m :: Nat) a.
KnownNat n =>
SNat m -> Vec (n * m) a -> Vec n (Vec m a)
unconcat
{-# INLINE unconcatI #-}

-- | Merge two vectors, alternating their elements, i.e.,
--
-- >>> merge (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> 7 :> 8 :> Nil)
-- <1,5,2,6,3,7,4,8>
merge :: KnownNat n => Vec n a -> Vec n a -> Vec (2 * n) a
merge :: Vec n a -> Vec n a -> Vec (2 * n) a
merge x :: Vec n a
x y :: Vec n a
y = Vec n (Vec 2 a) -> Vec (n * 2) a
forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (n * m) a
concat (Vec 2 (Vec n a) -> Vec n (Vec 2 a)
forall (n :: Nat) (m :: Nat) a.
KnownNat n =>
Vec m (Vec n a) -> Vec n (Vec m a)
transpose (Vec n a
x Vec n a -> Vec 1 (Vec n a) -> Vec (1 + 1) (Vec n a)
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec n a -> Vec 1 (Vec n a)
forall a. a -> Vec 1 a
singleton Vec n a
y))
{-# INLINE merge #-}

-- | The elements in a vector in reverse order.
--
-- >>> reverse (1:>2:>3:>4:>Nil)
-- <4,3,2,1>
reverse :: Vec n a -> Vec n a
reverse :: Vec n a -> Vec n a
reverse Nil           = Vec n a
forall a. Vec 0 a
Nil
reverse (x :: a
x `Cons` xs :: Vec n a
xs) = Vec n a -> Vec n a
forall (n :: Nat) a. Vec n a -> Vec n a
reverse Vec n a
xs Vec n a -> a -> Vec (n + 1) a
forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
:< a
x
{-# NOINLINE reverse #-}

-- | \"'map' @f xs@\" is the vector obtained by applying /f/ to each element
-- of /xs/, i.e.,
--
-- > map f (x1 :> x2 :>  ... :> xn :> Nil) == (f x1 :> f x2 :> ... :> f xn :> Nil)
--
-- and corresponds to the following circuit layout:
--
-- <<doc/map.svg>>
map :: (a -> b) -> Vec n a -> Vec n b
map :: (a -> b) -> Vec n a -> Vec n b
map _ Nil           = Vec n b
forall a. Vec 0 a
Nil
map f :: a -> b
f (x :: a
x `Cons` xs :: Vec n a
xs) = a -> b
f a
x b -> Vec n b -> Vec (n + 1) b
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` (a -> b) -> Vec n a -> Vec n b
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map a -> b
f Vec n a
xs
{-# NOINLINE map #-}

-- | Apply a function of every element of a vector and its index.
--
-- >>> :t imap (+) (2 :> 2 :> 2 :> 2 :> Nil)
-- imap (+) (2 :> 2 :> 2 :> 2 :> Nil) :: Vec 4 (Index 4)
-- >>> imap (+) (2 :> 2 :> 2 :> 2 :> Nil)
-- <2,3,*** Exception: X: Clash.Sized.Index: result 4 is out of bounds: [0..3]
-- ...
-- >>> imap (\i a -> fromIntegral i + a) (2 :> 2 :> 2 :> 2 :> Nil) :: Vec 4 (Unsigned 8)
-- <2,3,4,5>
--
-- \"'imap' @f xs@\" corresponds to the following circuit layout:
--
-- <<doc/imap.svg>>
imap :: forall n a b . KnownNat n => (Index n -> a -> b) -> Vec n a -> Vec n b
imap :: (Index n -> a -> b) -> Vec n a -> Vec n b
imap f :: Index n -> a -> b
f = Index n -> Vec n a -> Vec n b
forall (m :: Nat). Index n -> Vec m a -> Vec m b
go 0
  where
    go :: Index n -> Vec m a -> Vec m b
    go :: Index n -> Vec m a -> Vec m b
go _ Nil           = Vec m b
forall a. Vec 0 a
Nil
    go n :: Index n
n (x :: a
x `Cons` xs :: Vec n a
xs) = Index n -> a -> b
f Index n
n a
x b -> Vec n b -> Vec (n + 1) b
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Index n -> Vec n a -> Vec n b
forall (m :: Nat). Index n -> Vec m a -> Vec m b
go (Index n
nIndex n -> Index n -> Index n
forall a. Num a => a -> a -> a
+1) Vec n a
xs
{-# NOINLINE imap #-}

-- | Zip two vectors with a functions that also takes the elements' indices.
--
-- >>> izipWith (\i a b -> i + a + b) (2 :> 2 :> Nil)  (3 :> 3:> Nil)
-- <*** Exception: X: Clash.Sized.Index: result 3 is out of bounds: [0..1]
-- ...
-- >>> izipWith (\i a b -> fromIntegral i + a + b) (2 :> 2 :> Nil) (3 :> 3 :> Nil) :: Vec 2 (Unsigned 8)
-- <5,6>
--
-- \"'imap' @f xs@\" corresponds to the following circuit layout:
--
-- <<doc/izipWith.svg>>
--
-- __NB:__ 'izipWith' is /strict/ in its second argument, and /lazy/ in its
-- third. This matters when 'izipWith' is used in a recursive setting. See
-- 'lazyV' for more information.
izipWith :: KnownNat n => (Index n -> a -> b -> c) -> Vec n a -> Vec n b
         -> Vec n c
izipWith :: (Index n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith f :: Index n -> a -> b -> c
f xs :: Vec n a
xs ys :: Vec n b
ys = (Index n -> (a, b) -> c) -> Vec n (a, b) -> Vec n c
forall (n :: Nat) a b.
KnownNat n =>
(Index n -> a -> b) -> Vec n a -> Vec n b
imap (\i :: Index n
i -> (a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Index n -> a -> b -> c
f Index n
i)) (Vec n a -> Vec n b -> Vec n (a, b)
forall (n :: Nat) a b. Vec n a -> Vec n b -> Vec n (a, b)
zip Vec n a
xs Vec n b
ys)
{-# INLINE izipWith #-}

-- | Right fold (function applied to each element and its index)
--
-- >>> let findLeftmost x xs = ifoldr (\i a b -> if a == x then Just i else b) Nothing xs
-- >>> findLeftmost 3 (1:>3:>2:>4:>3:>5:>6:>Nil)
-- Just 1
-- >>> findLeftmost 8 (1:>3:>2:>4:>3:>5:>6:>Nil)
-- Nothing
--
-- \"'ifoldr' @f z xs@\" corresponds to the following circuit layout:
--
-- <<doc/ifoldr.svg>>
ifoldr :: KnownNat n => (Index n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr :: (Index n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr f :: Index n -> a -> b -> b
f z :: b
z xs :: Vec n a
xs = Vec (n + 1) b -> b
forall (n :: Nat) a. Vec (n + 1) a -> a
head Vec (n + 1) b
ws
  where
    ws :: Vec (n + 1) b
ws = (Index n -> a -> b -> b) -> Vec n a -> Vec n b -> Vec n b
forall (n :: Nat) a b c.
KnownNat n =>
(Index n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith Index n -> a -> b -> b
f Vec n a
xs ((Vec (n + 1) b -> Vec n b
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
tail Vec (n + 1) b
ws)) Vec n b -> b -> Vec (n + 1) b
forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
:< b
z
{-# INLINE ifoldr #-}

-- | Left fold (function applied to each element and its index)
--
-- >>> let findRightmost x xs = ifoldl (\a i b -> if b == x then Just i else a) Nothing xs
-- >>> findRightmost 3 (1:>3:>2:>4:>3:>5:>6:>Nil)
-- Just 4
-- >>> findRightmost 8 (1:>3:>2:>4:>3:>5:>6:>Nil)
-- Nothing
--
-- \"'ifoldl' @f z xs@\" corresponds to the following circuit layout:
--
-- <<doc/ifoldl.svg>>
ifoldl :: KnownNat n => (a -> Index n -> b -> a) -> a -> Vec n b -> a
ifoldl :: (a -> Index n -> b -> a) -> a -> Vec n b -> a
ifoldl f :: a -> Index n -> b -> a
f z :: a
z xs :: Vec n b
xs = Vec (n + 1) a -> a
forall (n :: Nat) a. Vec (n + 1) a -> a
last Vec (n + 1) a
ws
  where
    ws :: Vec (n + 1) a
ws = a
z a -> Vec n a -> Vec (n + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` (Index n -> b -> a -> a) -> Vec n b -> Vec n a -> Vec n a
forall (n :: Nat) a b c.
KnownNat n =>
(Index n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith (\i :: Index n
i b :: b
b a :: a
a -> a -> Index n -> b -> a
f a
a Index n
i b
b) Vec n b
xs (Vec (n + 1) a -> Vec n a
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
init Vec (n + 1) a
ws)
{-# INLINE ifoldl #-}

-- | Generate a vector of indices.
--
-- >>> indices d4
-- <0,1,2,3>
indices :: KnownNat n => SNat n -> Vec n (Index n)
indices :: SNat n -> Vec n (Index n)
indices _ = Vec n (Index n)
forall (n :: Nat). KnownNat n => Vec n (Index n)
indicesI
{-# INLINE indices #-}

-- | Generate a vector of indices, where the length of the vector is determined
-- by the context.
--
-- >>> indicesI :: Vec 4 (Index 4)
-- <0,1,2,3>
indicesI :: KnownNat n => Vec n (Index n)
indicesI :: Vec n (Index n)
indicesI = (Index n -> () -> Index n) -> Vec n () -> Vec n (Index n)
forall (n :: Nat) a b.
KnownNat n =>
(Index n -> a -> b) -> Vec n a -> Vec n b
imap Index n -> () -> Index n
forall a b. a -> b -> a
const (() -> Vec n ()
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat ())
{-# INLINE indicesI #-}

-- | \"'findIndex' @p xs@\" returns the index of the /first/ element of /xs/
-- satisfying the predicate /p/, or 'Nothing' if there is no such element.
--
-- >>> findIndex (> 3) (1:>3:>2:>4:>3:>5:>6:>Nil)
-- Just 3
-- >>> findIndex (> 8) (1:>3:>2:>4:>3:>5:>6:>Nil)
-- Nothing
findIndex :: KnownNat n => (a -> Bool) -> Vec n a -> Maybe (Index n)
findIndex :: (a -> Bool) -> Vec n a -> Maybe (Index n)
findIndex f :: a -> Bool
f = (Index n -> a -> Maybe (Index n) -> Maybe (Index n))
-> Maybe (Index n) -> Vec n a -> Maybe (Index n)
forall (n :: Nat) a b.
KnownNat n =>
(Index n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr (\i :: Index n
i a :: a
a b :: Maybe (Index n)
b -> if a -> Bool
f a
a then Index n -> Maybe (Index n)
forall a. a -> Maybe a
Just Index n
i else Maybe (Index n)
b) Maybe (Index n)
forall a. Maybe a
Nothing
{-# INLINE findIndex #-}

-- | \"'elemIndex' @a xs@\" returns the index of the /first/ element which is
-- equal (by '==') to the query element /a/, or 'Nothing' if there is no such
-- element.
--
-- >>> elemIndex 3 (1:>3:>2:>4:>3:>5:>6:>Nil)
-- Just 1
-- >>> elemIndex 8 (1:>3:>2:>4:>3:>5:>6:>Nil)
-- Nothing
elemIndex :: (KnownNat n, Eq a) => a -> Vec n a -> Maybe (Index n)
elemIndex :: a -> Vec n a -> Maybe (Index n)
elemIndex x :: a
x = (a -> Bool) -> Vec n a -> Maybe (Index n)
forall (n :: Nat) a.
KnownNat n =>
(a -> Bool) -> Vec n a -> Maybe (Index n)
findIndex (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==)
{-# INLINE elemIndex #-}

-- | 'zipWith' generalizes 'zip' by zipping with the function given
-- as the first argument, instead of a tupling function.
-- For example, \"'zipWith' @(+)@\" applied to two vectors produces the
-- vector of corresponding sums.
--
-- > zipWith f (x1 :> x2 :> ... xn :> Nil) (y1 :> y2 :> ... :> yn :> Nil) == (f x1 y1 :> f x2 y2 :> ... :> f xn yn :> Nil)
--
-- \"'zipWith' @f xs ys@\" corresponds to the following circuit layout:
--
-- <<doc/zipWith.svg>>
--
-- __NB:__ 'zipWith' is /strict/ in its second argument, and /lazy/ in its
-- third. This matters when 'zipWith' is used in a recursive setting. See
-- 'lazyV' for more information.
zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith _ Nil           _  = Vec n c
forall a. Vec 0 a
Nil
zipWith f :: a -> b -> c
f (x :: a
x `Cons` xs :: Vec n a
xs) ys :: Vec n b
ys = a -> b -> c
f a
x (Vec (n + 1) b -> b
forall (n :: Nat) a. Vec (n + 1) a -> a
head Vec n b
Vec (n + 1) b
ys) c -> Vec n c -> Vec (n + 1) c
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith a -> b -> c
f Vec n a
xs (Vec (n + 1) b -> Vec n b
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
tail Vec n b
Vec (n + 1) b
ys)
{-# NOINLINE zipWith #-}

-- | 'zipWith3' generalizes 'zip3' by zipping with the function given
-- as the first argument, instead of a tupling function.
--
-- > zipWith3 f (x1 :> x2 :> ... xn :> Nil) (y1 :> y2 :> ... :> yn :> Nil) (z1 :> z2 :> ... :> zn :> Nil) == (f x1 y1 z1 :> f x2 y2 z2 :> ... :> f xn yn zn :> Nil)
--
-- \"'zipWith3' @f xs ys zs@\" corresponds to the following circuit layout:
--
-- <<doc/zipWith3.svg>>
--
-- __NB:__ 'zipWith3' is /strict/ in its second argument, and /lazy/ in its
-- third and fourth. This matters when 'zipWith3' is used in a recursive setting.
-- See 'lazyV' for more information.
zipWith3 :: (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d
zipWith3 :: (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d
zipWith3 f :: a -> b -> c -> d
f us :: Vec n a
us vs :: Vec n b
vs ws :: Vec n c
ws = (a -> (b, c) -> d) -> Vec n a -> Vec n (b, c) -> Vec n d
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith (\a :: a
a (b :: b
b,c :: c
c) -> a -> b -> c -> d
f a
a b
b c
c) Vec n a
us (Vec n b -> Vec n c -> Vec n (b, c)
forall (n :: Nat) a b. Vec n a -> Vec n b -> Vec n (a, b)
zip Vec n b
vs Vec n c
ws)
{-# INLINE zipWith3 #-}

-- 'zipWith4' is analogous to 'zipWith3', but with four vectors.
--
-- __NB:__ 'zipWith4' is /strict/ in its second argument, and /lazy/ its following
-- arguments. This matters when 'zipWith4' is used in a recursive setting. See
-- 'lazyV' for more information.
zipWith4
  :: (a -> b -> c -> d -> e)
  -> Vec n a
  -> Vec n b
  -> Vec n c
  -> Vec n d
  -> Vec n e
zipWith4 :: (a -> b -> c -> d -> e)
-> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e
zipWith4 f :: a -> b -> c -> d -> e
f us :: Vec n a
us vs :: Vec n b
vs ws :: Vec n c
ws xs :: Vec n d
xs =
  (a -> (b, c, d) -> e) -> Vec n a -> Vec n (b, c, d) -> Vec n e
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith (\a :: a
a (b :: b
b,c :: c
c,d :: d
d) -> a -> b -> c -> d -> e
f a
a b
b c
c d
d) Vec n a
us (Vec n b -> Vec n c -> Vec n d -> Vec n (b, c, d)
forall (n :: Nat) a b c.
Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c)
zip3 Vec n b
vs Vec n c
ws Vec n d
xs)
{-# INLINE zipWith4 #-}

-- 'zipWith5' is analogous to 'zipWith3', but with five vectors.
--
-- __NB:__ 'zipWith5' is /strict/ in its second argument, and /lazy/ its following
-- arguments. This matters when 'zipWith5' is used in a recursive setting. See
-- 'lazyV' for more information.
zipWith5
  :: (a -> b -> c -> d -> e -> f)
  -> Vec n a
  -> Vec n b
  -> Vec n c
  -> Vec n d
  -> Vec n e
  -> Vec n f
zipWith5 :: (a -> b -> c -> d -> e -> f)
-> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f
zipWith5 f :: a -> b -> c -> d -> e -> f
f us :: Vec n a
us vs :: Vec n b
vs ws :: Vec n c
ws xs :: Vec n d
xs ys :: Vec n e
ys =
  (a -> (b, c, d, e) -> f)
-> Vec n a -> Vec n (b, c, d, e) -> Vec n f
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith (\a :: a
a (b :: b
b,c :: c
c,d :: d
d,e :: e
e) -> a -> b -> c -> d -> e -> f
f a
a b
b c
c d
d e
e) Vec n a
us (Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n (b, c, d, e)
forall (n :: Nat) a b c d.
Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n (a, b, c, d)
zip4 Vec n b
vs Vec n c
ws Vec n d
xs Vec n e
ys)
{-# INLINE zipWith5 #-}

-- 'zipWith6' is analogous to 'zipWith3', but with six vectors.
--
-- __NB:__ 'zipWith6' is /strict/ in its second argument, and /lazy/ its following
-- arguments. This matters when 'zipWith6' is used in a recursive setting. See
-- 'lazyV' for more information.
zipWith6
  :: (a -> b -> c -> d -> e -> f -> g)
  -> Vec n a
  -> Vec n b
  -> Vec n c
  -> Vec n d
  -> Vec n e
  -> Vec n f
  -> Vec n g
zipWith6 :: (a -> b -> c -> d -> e -> f -> g)
-> Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n f
-> Vec n g
zipWith6 f :: a -> b -> c -> d -> e -> f -> g
f us :: Vec n a
us vs :: Vec n b
vs ws :: Vec n c
ws xs :: Vec n d
xs ys :: Vec n e
ys zs :: Vec n f
zs =
  (a -> (b, c, d, e, f) -> g)
-> Vec n a -> Vec n (b, c, d, e, f) -> Vec n g
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith (\u :: a
u (v :: b
v,w :: c
w,x :: d
x,y :: e
y,z :: f
z) -> a -> b -> c -> d -> e -> f -> g
f a
u b
v c
w d
x e
y f
z) Vec n a
us (Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n f
-> Vec n (b, c, d, e, f)
forall (n :: Nat) a b c d e.
Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n (a, b, c, d, e)
zip5 Vec n b
vs Vec n c
ws Vec n d
xs Vec n e
ys Vec n f
zs)
{-# INLINE zipWith6 #-}

-- 'zipWith7' is analogous to 'zipWith3', but with seven vectors.
--
-- __NB:__ 'zipWith7' is /strict/ in its second argument, and /lazy/ its following
-- arguments. This matters when 'zipWith7' is used in a recursive setting. See
-- 'lazyV' for more information.
zipWith7
  :: (a -> b -> c -> d -> e -> f -> g -> h)
  -> Vec n a
  -> Vec n b
  -> Vec n c
  -> Vec n d
  -> Vec n e
  -> Vec n f
  -> Vec n g
  -> Vec n h
zipWith7 :: (a -> b -> c -> d -> e -> f -> g -> h)
-> Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n f
-> Vec n g
-> Vec n h
zipWith7 f :: a -> b -> c -> d -> e -> f -> g -> h
f ts :: Vec n a
ts us :: Vec n b
us vs :: Vec n c
vs ws :: Vec n d
ws xs :: Vec n e
xs ys :: Vec n f
ys zs :: Vec n g
zs =
  (a -> (b, c, d, e, f, g) -> h)
-> Vec n a -> Vec n (b, c, d, e, f, g) -> Vec n h
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith (\t :: a
t (u :: b
u,v :: c
v,w :: d
w,x :: e
x,y :: f
y,z :: g
z) -> a -> b -> c -> d -> e -> f -> g -> h
f a
t b
u c
v d
w e
x f
y g
z) Vec n a
ts (Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n f
-> Vec n g
-> Vec n (b, c, d, e, f, g)
forall (n :: Nat) a b c d e f.
Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n f
-> Vec n (a, b, c, d, e, f)
zip6 Vec n b
us Vec n c
vs Vec n d
ws Vec n e
xs Vec n f
ys Vec n g
zs)
{-# INLINE zipWith7 #-}

-- | 'foldr', applied to a binary operator, a starting value (typically
-- the right-identity of the operator), and a vector, reduces the vector
-- using the binary operator, from right to left:
--
-- > foldr f z (x1 :> ... :> xn1 :> xn :> Nil) == x1 `f` (... (xn1 `f` (xn `f` z))...)
-- > foldr r z Nil                             == z
--
-- >>> foldr (/) 1 (5 :> 4 :> 3 :> 2 :> Nil)
-- 1.875
--
-- \"'foldr' @f z xs@\" corresponds to the following circuit layout:
--
-- <<doc/foldr.svg>>
--
-- __NB__: @"'foldr' f z xs"@ produces a linear structure, which has a depth, or
-- delay, of O(@'length' xs@). Use 'fold' if your binary operator @f@ is
-- associative, as @"'fold' f xs"@ produces a structure with a depth of
-- O(log_2(@'length' xs@)).
foldr :: (a -> b -> b) -> b -> Vec n a -> b
foldr :: (a -> b -> b) -> b -> Vec n a -> b
foldr _ z :: b
z Nil           = b
z
foldr f :: a -> b -> b
f z :: b
z (x :: a
x `Cons` xs :: Vec n a
xs) = a -> b -> b
f a
x ((a -> b -> b) -> b -> Vec n a -> b
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr a -> b -> b
f b
z Vec n a
xs)
{-# NOINLINE foldr #-}

-- | 'foldl', applied to a binary operator, a starting value (typically
-- the left-identity of the operator), and a vector, reduces the vector
-- using the binary operator, from left to right:
--
-- > foldl f z (x1 :> x2 :> ... :> xn :> Nil) == (...((z `f` x1) `f` x2) `f`...) `f` xn
-- > foldl f z Nil                            == z
--
-- >>> foldl (/) 1 (5 :> 4 :> 3 :> 2 :> Nil)
-- 8.333333333333333e-3
--
-- \"'foldl' @f z xs@\" corresponds to the following circuit layout:
--
-- <<doc/foldl.svg>>
--
-- __NB__: @"'foldl' f z xs"@ produces a linear structure, which has a depth, or
-- delay, of O(@'length' xs@). Use 'fold' if your binary operator @f@ is
-- associative, as @"'fold' f xs"@ produces a structure with a depth of
-- O(log_2(@'length' xs@)).
foldl :: (b -> a -> b) -> b -> Vec n a -> b
foldl :: (b -> a -> b) -> b -> Vec n a -> b
foldl f :: b -> a -> b
f z :: b
z xs :: Vec n a
xs = Vec (n + 1) b -> b
forall (n :: Nat) a. Vec (n + 1) a -> a
last ((b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
forall b a (n :: Nat).
(b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
scanl b -> a -> b
f b
z Vec n a
xs)
{-# INLINE foldl #-}

-- | 'foldr1' is a variant of 'foldr' that has no starting value argument,
-- and thus must be applied to non-empty vectors.
--
-- > foldr1 f (x1 :> ... :> xn2 :> xn1 :> xn :> Nil) == x1 `f` (... (xn2 `f` (xn1 `f` xn))...)
-- > foldr1 f (x1 :> Nil)                            == x1
-- > foldr1 f Nil                                    == TYPE ERROR
--
-- >>> foldr1 (/) (5 :> 4 :> 3 :> 2 :> 1 :> Nil)
-- 1.875
--
-- \"'foldr1' @f xs@\" corresponds to the following circuit layout:
--
-- <<doc/foldr1.svg>>
--
-- __NB__: @"'foldr1' f z xs"@ produces a linear structure, which has a depth,
-- or delay, of O(@'length' xs@). Use 'fold' if your binary operator @f@ is
-- associative, as @"'fold' f xs"@ produces a structure with a depth of
-- O(log_2(@'length' xs@)).
foldr1 :: (a -> a -> a) -> Vec (n + 1) a -> a
foldr1 :: (a -> a -> a) -> Vec (n + 1) a -> a
foldr1 f :: a -> a -> a
f xs :: Vec (n + 1) a
xs = (a -> a -> a) -> a -> Vec n a -> a
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr a -> a -> a
f (Vec (n + 1) a -> a
forall (n :: Nat) a. Vec (n + 1) a -> a
last Vec (n + 1) a
xs) (Vec (n + 1) a -> Vec n a
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
init Vec (n + 1) a
xs)
{-# INLINE foldr1 #-}

-- | 'foldl1' is a variant of 'foldl' that has no starting value argument,
-- and thus must be applied to non-empty vectors.
--
-- > foldl1 f (x1 :> x2 :> x3 :> ... :> xn :> Nil) == (...((x1 `f` x2) `f` x3) `f`...) `f` xn
-- > foldl1 f (x1 :> Nil)                          == x1
-- > foldl1 f Nil                                  == TYPE ERROR
--
-- >>> foldl1 (/) (1 :> 5 :> 4 :> 3 :> 2 :> Nil)
-- 8.333333333333333e-3
--
-- \"'foldl1' @f xs@\" corresponds to the following circuit layout:
--
-- <<doc/foldl1.svg>>
--
-- __NB__: @"'foldl1' f z xs"@ produces a linear structure, which has a depth,
-- or delay, of O(@'length' xs@). Use 'fold' if your binary operator @f@ is
-- associative, as @"'fold' f xs"@ produces a structure with a depth of
-- O(log_2(@'length' xs@)).
foldl1 :: (a -> a -> a) -> Vec (n + 1) a -> a
foldl1 :: (a -> a -> a) -> Vec (n + 1) a -> a
foldl1 f :: a -> a -> a
f xs :: Vec (n + 1) a
xs = (a -> a -> a) -> a -> Vec n a -> a
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl a -> a -> a
f (Vec (n + 1) a -> a
forall (n :: Nat) a. Vec (n + 1) a -> a
head Vec (n + 1) a
xs) (Vec (n + 1) a -> Vec n a
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
tail Vec (n + 1) a
xs)
{-# INLINE foldl1 #-}

-- | 'fold' is a variant of 'foldr1' and 'foldl1', but instead of reducing from
-- right to left, or left to right, it reduces a vector using a tree-like
-- structure. The depth, or delay, of the structure produced by
-- \"@'fold' f xs@\", is hence @O(log_2('length' xs))@, and not
-- @O('length' xs)@.
--
-- __NB__: The binary operator \"@f@\" in \"@'fold' f xs@\" must be associative.
--
-- > fold f (x1 :> x2 :> ... :> xn1 :> xn :> Nil) == ((x1 `f` x2) `f` ...) `f` (... `f` (xn1 `f` xn))
-- > fold f (x1 :> Nil)                           == x1
-- > fold f Nil                                   == TYPE ERROR
--
-- >>> fold (+) (5 :> 4 :> 3 :> 2 :> 1 :> Nil)
-- 15
--
-- \"'fold' @f xs@\" corresponds to the following circuit layout:
--
-- <<doc/fold.svg>>
fold :: (a -> a -> a) -> Vec (n + 1) a -> a
fold :: (a -> a -> a) -> Vec (n + 1) a -> a
fold f :: a -> a -> a
f vs :: Vec (n + 1) a
vs = [a] -> a
fold' (Vec (n + 1) a -> [a]
forall (n :: Nat) a. Vec n a -> [a]
toList Vec (n + 1) a
vs)
  where
    fold' :: [a] -> a
fold' [x :: a
x] = a
x
    fold' xs :: [a]
xs  = [a] -> a
fold' [a]
ys a -> a -> a
`f` [a] -> a
fold' [a]
zs
      where
        (ys :: [a]
ys,zs :: [a]
zs) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
P.splitAt ([a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
P.length [a]
xs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` 2) [a]
xs
{-# NOINLINE fold #-}
{-# ANN fold (InlinePrimitive [VHDL,Verilog,SystemVerilog] "[ { \"BlackBoxHaskell\" : { \"name\" : \"Clash.Sized.Vector.fold\", \"templateFunction\" : \"Clash.Primitives.Sized.Vector.foldBBF\"}} ]") #-}

-- | 'scanl' is similar to 'foldl', but returns a vector of successive reduced
-- values from the left:
--
-- > scanl f z (x1 :> x2 :> ... :> Nil) == z :> (z `f` x1) :> ((z `f` x1) `f` x2) :> ... :> Nil
--
-- >>> scanl (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
-- <0,5,9,12,14>
--
-- \"'scanl' @f z xs@\" corresponds to the following circuit layout:
--
-- <<doc/scanl.svg>>
--
-- __NB__:
--
-- > last (scanl f z xs) == foldl f z xs
scanl :: (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
scanl :: (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
scanl f :: b -> a -> b
f z :: b
z xs :: Vec n a
xs = Vec (n + 1) b
ws
  where
    ws :: Vec (n + 1) b
ws = b
z b -> Vec n b -> Vec (n + 1) b
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` (a -> b -> b) -> Vec n a -> Vec n b -> Vec n b
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith ((b -> a -> b) -> a -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> a -> b
f) Vec n a
xs (Vec (n + 1) b -> Vec n b
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
init Vec (n + 1) b
ws)
{-# INLINE scanl #-}

-- | 'postscanl' is a variant of 'scanl' where the first result is dropped:
--
-- > postscanl f z (x1 :> x2 :> ... :> Nil) == (z `f` x1) :> ((z `f` x1) `f` x2) :> ... :> Nil
--
-- >>> postscanl (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
-- <5,9,12,14>
--
-- \"'postscanl' @f z xs@\" corresponds to the following circuit layout:
--
-- <<doc/sscanl.svg>>
postscanl :: (b -> a -> b) -> b -> Vec n a -> Vec n b
postscanl :: (b -> a -> b) -> b -> Vec n a -> Vec n b
postscanl f :: b -> a -> b
f z :: b
z xs :: Vec n a
xs = Vec (n + 1) b -> Vec n b
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
tail ((b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
forall b a (n :: Nat).
(b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
scanl b -> a -> b
f b
z Vec n a
xs)
{-# INLINE postscanl #-}

-- | 'scanr' is similar to 'foldr', but returns a vector of successive reduced
-- values from the right:
--
-- > scanr f z (... :> xn1 :> xn :> Nil) == ... :> (xn1 `f` (xn `f` z)) :> (xn `f` z) :> z :> Nil
--
-- >>> scanr (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
-- <14,9,5,2,0>
--
-- \"'scanr' @f z xs@\" corresponds to the following circuit layout:
--
-- <<doc/scanr.svg>>
--
-- __NB__:
--
-- > head (scanr f z xs) == foldr f z xs
scanr :: (a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
scanr :: (a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
scanr f :: a -> b -> b
f z :: b
z xs :: Vec n a
xs = Vec (n + 1) b
ws
  where
    ws :: Vec (n + 1) b
ws = (a -> b -> b) -> Vec n a -> Vec n b -> Vec n b
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith a -> b -> b
f Vec n a
xs ((Vec (n + 1) b -> Vec n b
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
tail Vec (n + 1) b
ws)) Vec n b -> b -> Vec (n + 1) b
forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
:< b
z
{-# INLINE scanr #-}

-- | 'postscanr' is a variant of 'scanr' that where the last result is dropped:
--
-- > postscanr f z (... :> xn1 :> xn :> Nil) == ... :> (xn1 `f` (xn `f` z)) :> (xn `f` z) :> Nil
--
-- >>> postscanr (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
-- <14,9,5,2>
--
-- \"'postscanr' @f z xs@\" corresponds to the following circuit layout:
--
-- <<doc/sscanr.svg>>
postscanr :: (a -> b -> b) -> b -> Vec n a -> Vec n b
postscanr :: (a -> b -> b) -> b -> Vec n a -> Vec n b
postscanr f :: a -> b -> b
f z :: b
z xs :: Vec n a
xs = Vec (n + 1) b -> Vec n b
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
init ((a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
forall a b (n :: Nat).
(a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
scanr a -> b -> b
f b
z Vec n a
xs)
{-# INLINE postscanr #-}

-- | The 'mapAccumL' function behaves like a combination of 'map' and 'foldl';
-- it applies a function to each element of a vector, passing an accumulating
-- parameter from left to right, and returning a final value of this accumulator
-- together with the new vector.
--
-- >>> mapAccumL (\acc x -> (acc + x,acc + 1)) 0 (1 :> 2 :> 3 :> 4 :> Nil)
-- (10,<1,2,4,7>)
--
-- \"'mapAccumL' @f acc xs@\" corresponds to the following circuit layout:
--
-- <<doc/mapAccumL.svg>>
mapAccumL :: (acc -> x -> (acc,y)) -> acc -> Vec n x -> (acc,Vec n y)
mapAccumL :: (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)
mapAccumL f :: acc -> x -> (acc, y)
f acc :: acc
acc xs :: Vec n x
xs = (acc
acc',Vec n y
ys)
  where
    accs :: Vec (n + 1) acc
accs  = acc
acc acc -> Vec n acc -> Vec (n + 1) acc
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Vec n acc
accs'
    ws :: Vec n (acc, y)
ws    = (x -> acc -> (acc, y)) -> Vec n x -> Vec n acc -> Vec n (acc, y)
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith ((acc -> x -> (acc, y)) -> x -> acc -> (acc, y)
forall a b c. (a -> b -> c) -> b -> a -> c
flip acc -> x -> (acc, y)
f) Vec n x
xs (Vec (n + 1) acc -> Vec n acc
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
init Vec (n + 1) acc
accs)
    accs' :: Vec n acc
accs' = ((acc, y) -> acc) -> Vec n (acc, y) -> Vec n acc
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (acc, y) -> acc
forall a b. (a, b) -> a
fst Vec n (acc, y)
ws
    ys :: Vec n y
ys    = ((acc, y) -> y) -> Vec n (acc, y) -> Vec n y
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (acc, y) -> y
forall a b. (a, b) -> b
snd Vec n (acc, y)
ws
    acc' :: acc
acc'  = Vec (n + 1) acc -> acc
forall (n :: Nat) a. Vec (n + 1) a -> a
last Vec (n + 1) acc
accs
{-# INLINE mapAccumL #-}

-- | The 'mapAccumR' function behaves like a combination of 'map' and 'foldr';
-- it applies a function to each element of a vector, passing an accumulating
-- parameter from right to left, and returning a final value of this accumulator
-- together with the new vector.
--
-- >>> mapAccumR (\acc x -> (acc + x,acc + 1)) 0 (1 :> 2 :> 3 :> 4 :> Nil)
-- (10,<10,8,5,1>)
--
-- \"'mapAccumR' @f acc xs@\" corresponds to the following circuit layout:
--
-- <<doc/mapAccumR.svg>>
mapAccumR :: (acc -> x -> (acc,y)) -> acc -> Vec n x -> (acc, Vec n y)
mapAccumR :: (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)
mapAccumR f :: acc -> x -> (acc, y)
f acc :: acc
acc xs :: Vec n x
xs = (acc
acc',Vec n y
ys)
  where
    accs :: Vec (n + 1) acc
accs  = Vec n acc
accs' Vec n acc -> acc -> Vec (n + 1) acc
forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
:< acc
acc
    ws :: Vec n (acc, y)
ws    = (x -> acc -> (acc, y)) -> Vec n x -> Vec n acc -> Vec n (acc, y)
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith ((acc -> x -> (acc, y)) -> x -> acc -> (acc, y)
forall a b c. (a -> b -> c) -> b -> a -> c
flip acc -> x -> (acc, y)
f) Vec n x
xs (Vec (n + 1) acc -> Vec n acc
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
tail Vec (n + 1) acc
accs)
    accs' :: Vec n acc
accs' = ((acc, y) -> acc) -> Vec n (acc, y) -> Vec n acc
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (acc, y) -> acc
forall a b. (a, b) -> a
fst Vec n (acc, y)
ws
    ys :: Vec n y
ys    = ((acc, y) -> y) -> Vec n (acc, y) -> Vec n y
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (acc, y) -> y
forall a b. (a, b) -> b
snd Vec n (acc, y)
ws
    acc' :: acc
acc'  = Vec (n + 1) acc -> acc
forall (n :: Nat) a. Vec (n + 1) a -> a
head Vec (n + 1) acc
accs
{-# INLINE mapAccumR #-}

-- | 'zip' takes two vectors and returns a vector of corresponding pairs.
--
-- >>> zip (1:>2:>3:>4:>Nil) (4:>3:>2:>1:>Nil)
-- <(1,4),(2,3),(3,2),(4,1)>
zip :: Vec n a -> Vec n b -> Vec n (a,b)
zip :: Vec n a -> Vec n b -> Vec n (a, b)
zip = (a -> b -> (a, b)) -> Vec n a -> Vec n b -> Vec n (a, b)
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith (,)
{-# INLINE zip #-}

-- | 'zip3' takes three vectors and returns a vector of corresponding triplets.
--
-- >>> zip3 (1:>2:>3:>4:>Nil) (4:>3:>2:>1:>Nil) (5:>6:>7:>8:>Nil)
-- <(1,4,5),(2,3,6),(3,2,7),(4,1,8)>
zip3 :: Vec n a -> Vec n b -> Vec n c -> Vec n (a,b,c)
zip3 :: Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c)
zip3 = (a -> b -> c -> (a, b, c))
-> Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c)
forall a b c d (n :: Nat).
(a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d
zipWith3 (,,)
{-# INLINE zip3 #-}

-- | 'zip4' takes four vectors and returns a list of quadruples, analogous
-- to 'zip'.
zip4 :: Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n (a,b,c,d)
zip4 :: Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n (a, b, c, d)
zip4 = (a -> b -> c -> d -> (a, b, c, d))
-> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n (a, b, c, d)
forall a b c d e (n :: Nat).
(a -> b -> c -> d -> e)
-> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e
zipWith4 (,,,)
{-# INLINE zip4 #-}

-- | 'zip5' takes five vectors and returns a list of five-tuples, analogous
-- to 'zip'.
zip5 :: Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n (a,b,c,d,e)
zip5 :: Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n (a, b, c, d, e)
zip5 = (a -> b -> c -> d -> e -> (a, b, c, d, e))
-> Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n (a, b, c, d, e)
forall a b c d e f (n :: Nat).
(a -> b -> c -> d -> e -> f)
-> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f
zipWith5 (,,,,)
{-# INLINE zip5 #-}

-- | 'zip6' takes six vectors and returns a list of six-tuples, analogous
-- to 'zip'.
zip6
  :: Vec n a
  -> Vec n b
  -> Vec n c
  -> Vec n d
  -> Vec n e
  -> Vec n f
  -> Vec n (a,b,c,d,e,f)
zip6 :: Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n f
-> Vec n (a, b, c, d, e, f)
zip6 = (a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n f
-> Vec n (a, b, c, d, e, f)
forall a b c d e f g (n :: Nat).
(a -> b -> c -> d -> e -> f -> g)
-> Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n f
-> Vec n g
zipWith6 (,,,,,)
{-# INLINE zip6 #-}

-- | 'zip7' takes seven vectors and returns a list of seven-tuples, analogous
-- to 'zip'.
zip7
  :: Vec n a
  -> Vec n b
  -> Vec n c
  -> Vec n d
  -> Vec n e
  -> Vec n f
  -> Vec n g
  -> Vec n (a,b,c,d,e,f,g)
zip7 :: Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n f
-> Vec n g
-> Vec n (a, b, c, d, e, f, g)
zip7 = (a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n f
-> Vec n g
-> Vec n (a, b, c, d, e, f, g)
forall a b c d e f g h (n :: Nat).
(a -> b -> c -> d -> e -> f -> g -> h)
-> Vec n a
-> Vec n b
-> Vec n c
-> Vec n d
-> Vec n e
-> Vec n f
-> Vec n g
-> Vec n h
zipWith7 (,,,,,,)
{-# INLINE zip7 #-}

-- | 'unzip' transforms a vector of pairs into a vector of first components
-- and a vector of second components.
--
-- >>> unzip ((1,4):>(2,3):>(3,2):>(4,1):>Nil)
-- (<1,2,3,4>,<4,3,2,1>)
unzip :: Vec n (a,b) -> (Vec n a, Vec n b)
unzip :: Vec n (a, b) -> (Vec n a, Vec n b)
unzip xs :: Vec n (a, b)
xs = (((a, b) -> a) -> Vec n (a, b) -> Vec n a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (a, b) -> a
forall a b. (a, b) -> a
fst Vec n (a, b)
xs, ((a, b) -> b) -> Vec n (a, b) -> Vec n b
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (a, b) -> b
forall a b. (a, b) -> b
snd Vec n (a, b)
xs)
{-# INLINE unzip #-}

-- | 'unzip3' transforms a vector of triplets into a vector of first components,
-- a vector of second components, and a vector of third components.
--
-- >>> unzip3 ((1,4,5):>(2,3,6):>(3,2,7):>(4,1,8):>Nil)
-- (<1,2,3,4>,<4,3,2,1>,<5,6,7,8>)
unzip3 :: Vec n (a,b,c) -> (Vec n a, Vec n b, Vec n c)
unzip3 :: Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c)
unzip3 xs :: Vec n (a, b, c)
xs = ( ((a, b, c) -> a) -> Vec n (a, b, c) -> Vec n a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(x :: a
x,_,_) -> a
x) Vec n (a, b, c)
xs
            , ((a, b, c) -> b) -> Vec n (a, b, c) -> Vec n b
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,y :: b
y,_) -> b
y) Vec n (a, b, c)
xs
            , ((a, b, c) -> c) -> Vec n (a, b, c) -> Vec n c
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,z :: c
z) -> c
z) Vec n (a, b, c)
xs
            )
{-# INLINE unzip3 #-}

-- | 'unzip4' takes a vector of quadruples and returns four vectors, analogous
-- to 'unzip'.
unzip4 :: Vec n (a,b,c,d) -> (Vec n a, Vec n b, Vec n c, Vec n d)
unzip4 :: Vec n (a, b, c, d) -> (Vec n a, Vec n b, Vec n c, Vec n d)
unzip4 xs :: Vec n (a, b, c, d)
xs = ( ((a, b, c, d) -> a) -> Vec n (a, b, c, d) -> Vec n a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(w :: a
w,_,_,_) -> a
w) Vec n (a, b, c, d)
xs
            , ((a, b, c, d) -> b) -> Vec n (a, b, c, d) -> Vec n b
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,x :: b
x,_,_) -> b
x) Vec n (a, b, c, d)
xs
            , ((a, b, c, d) -> c) -> Vec n (a, b, c, d) -> Vec n c
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,y :: c
y,_) -> c
y) Vec n (a, b, c, d)
xs
            , ((a, b, c, d) -> d) -> Vec n (a, b, c, d) -> Vec n d
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,_,z :: d
z) -> d
z) Vec n (a, b, c, d)
xs
            )
{-# INLINE unzip4 #-}

-- | 'unzip5' takes a vector of five-tuples and returns five vectors, analogous
-- to 'unzip'.
unzip5 :: Vec n (a,b,c,d,e) -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
unzip5 :: Vec n (a, b, c, d, e)
-> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
unzip5 xs :: Vec n (a, b, c, d, e)
xs = ( ((a, b, c, d, e) -> a) -> Vec n (a, b, c, d, e) -> Vec n a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(v :: a
v,_,_,_,_) -> a
v) Vec n (a, b, c, d, e)
xs
            , ((a, b, c, d, e) -> b) -> Vec n (a, b, c, d, e) -> Vec n b
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,w :: b
w,_,_,_) -> b
w) Vec n (a, b, c, d, e)
xs
            , ((a, b, c, d, e) -> c) -> Vec n (a, b, c, d, e) -> Vec n c
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,x :: c
x,_,_) -> c
x) Vec n (a, b, c, d, e)
xs
            , ((a, b, c, d, e) -> d) -> Vec n (a, b, c, d, e) -> Vec n d
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,_,y :: d
y,_) -> d
y) Vec n (a, b, c, d, e)
xs
            , ((a, b, c, d, e) -> e) -> Vec n (a, b, c, d, e) -> Vec n e
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,_,_,z :: e
z) -> e
z) Vec n (a, b, c, d, e)
xs
            )
{-# INLINE unzip5 #-}

-- | 'unzip6' takes a vector of six-tuples and returns six vectors, analogous
-- to 'unzip'.
unzip6
  :: Vec n (a,b,c,d,e,f)
  -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f)
unzip6 :: Vec n (a, b, c, d, e, f)
-> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f)
unzip6 xs :: Vec n (a, b, c, d, e, f)
xs = ( ((a, b, c, d, e, f) -> a) -> Vec n (a, b, c, d, e, f) -> Vec n a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(u :: a
u,_,_,_,_,_) -> a
u) Vec n (a, b, c, d, e, f)
xs
            , ((a, b, c, d, e, f) -> b) -> Vec n (a, b, c, d, e, f) -> Vec n b
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,v :: b
v,_,_,_,_) -> b
v) Vec n (a, b, c, d, e, f)
xs
            , ((a, b, c, d, e, f) -> c) -> Vec n (a, b, c, d, e, f) -> Vec n c
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,w :: c
w,_,_,_) -> c
w) Vec n (a, b, c, d, e, f)
xs
            , ((a, b, c, d, e, f) -> d) -> Vec n (a, b, c, d, e, f) -> Vec n d
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,_,x :: d
x,_,_) -> d
x) Vec n (a, b, c, d, e, f)
xs
            , ((a, b, c, d, e, f) -> e) -> Vec n (a, b, c, d, e, f) -> Vec n e
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,_,_,y :: e
y,_) -> e
y) Vec n (a, b, c, d, e, f)
xs
            , ((a, b, c, d, e, f) -> f) -> Vec n (a, b, c, d, e, f) -> Vec n f
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,_,_,_,z :: f
z) -> f
z) Vec n (a, b, c, d, e, f)
xs
            )
{-# INLINE unzip6 #-}

-- | 'unzip7' takes a vector of seven-tuples and returns seven vectors, analogous
-- to 'unzip'.
unzip7
  :: Vec n (a,b,c,d,e,f,g)
  -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f, Vec n g)
unzip7 :: Vec n (a, b, c, d, e, f, g)
-> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f, Vec n g)
unzip7 xs :: Vec n (a, b, c, d, e, f, g)
xs = ( ((a, b, c, d, e, f, g) -> a)
-> Vec n (a, b, c, d, e, f, g) -> Vec n a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(t :: a
t,_,_,_,_,_,_) -> a
t) Vec n (a, b, c, d, e, f, g)
xs
            , ((a, b, c, d, e, f, g) -> b)
-> Vec n (a, b, c, d, e, f, g) -> Vec n b
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,u :: b
u,_,_,_,_,_) -> b
u) Vec n (a, b, c, d, e, f, g)
xs
            , ((a, b, c, d, e, f, g) -> c)
-> Vec n (a, b, c, d, e, f, g) -> Vec n c
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,v :: c
v,_,_,_,_) -> c
v) Vec n (a, b, c, d, e, f, g)
xs
            , ((a, b, c, d, e, f, g) -> d)
-> Vec n (a, b, c, d, e, f, g) -> Vec n d
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,_,w :: d
w,_,_,_) -> d
w) Vec n (a, b, c, d, e, f, g)
xs
            , ((a, b, c, d, e, f, g) -> e)
-> Vec n (a, b, c, d, e, f, g) -> Vec n e
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,_,_,x :: e
x,_,_) -> e
x) Vec n (a, b, c, d, e, f, g)
xs
            , ((a, b, c, d, e, f, g) -> f)
-> Vec n (a, b, c, d, e, f, g) -> Vec n f
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,_,_,_,y :: f
y,_) -> f
y) Vec n (a, b, c, d, e, f, g)
xs
            , ((a, b, c, d, e, f, g) -> g)
-> Vec n (a, b, c, d, e, f, g) -> Vec n g
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (\(_,_,_,_,_,_,z :: g
z) -> g
z) Vec n (a, b, c, d, e, f, g)
xs
            )
{-# INLINE unzip7 #-}


index_int :: KnownNat n => Vec n a -> Int -> a
index_int :: Vec n a -> Int -> a
index_int xs :: Vec n a
xs i :: Int
i@(I# n0 :: Int#
n0)
  | Int# -> Bool
isTrue# (Int#
n0 Int# -> Int# -> Int#
<# 0#) = String -> a
forall a. HasCallStack => String -> a
error "Clash.Sized.Vector.(!!): negative index"
  | Bool
otherwise          = Vec n a -> Int# -> a
forall (m :: Nat) a. Vec m a -> Int# -> a
sub Vec n a
xs Int#
n0
  where
    sub :: Vec m a -> Int# -> a
    sub :: Vec m a -> Int# -> a
sub Nil     _ = String -> a
forall a. HasCallStack => String -> a
error ([String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
P.concat [ "Clash.Sized.Vector.(!!): index "
                                    , Int -> String
forall a. Show a => a -> String
show Int
i
                                    , " is larger than maximum index "
                                    , Int -> String
forall a. Show a => a -> String
show ((Vec n a -> Int
forall (n :: Nat) a. KnownNat n => Vec n a -> Int
length Vec n a
xs)Int -> Int -> Int
forall a. Num a => a -> a -> a
-1)
                                    ])
    sub (y :: a
y `Cons` (!Vec n a
ys)) n :: Int#
n = if Int# -> Bool
isTrue# (Int#
n Int# -> Int# -> Int#
==# 0#)
                                then a
y
                                else Vec n a -> Int# -> a
forall (m :: Nat) a. Vec m a -> Int# -> a
sub Vec n a
ys (Int#
n Int# -> Int# -> Int#
-# 1#)
{-# NOINLINE index_int #-}

-- | \"@xs@ '!!' @n@\" returns the /n/'th element of /xs/.
--
-- __NB__: vector elements have an __ASCENDING__ subscript starting from 0 and
-- ending at @'length' - 1@.
--
-- >>> (1:>2:>3:>4:>5:>Nil) !! 4
-- 5
-- >>> (1:>2:>3:>4:>5:>Nil) !! (length (1:>2:>3:>4:>5:>Nil) - 1)
-- 5
-- >>> (1:>2:>3:>4:>5:>Nil) !! 1
-- 2
-- >>> (1:>2:>3:>4:>5:>Nil) !! 14
-- *** Exception: Clash.Sized.Vector.(!!): index 14 is larger than maximum index 4
-- ...
(!!) :: (KnownNat n, Enum i) => Vec n a -> i -> a
xs :: Vec n a
xs !! :: Vec n a -> i -> a
!! i :: i
i = Vec n a -> Int -> a
forall (n :: Nat) a. KnownNat n => Vec n a -> Int -> a
index_int Vec n a
xs (i -> Int
forall a. Enum a => a -> Int
fromEnum i
i)
{-# INLINE (!!) #-}

-- | The length of a 'Vec'tor as an 'Int' value.
--
-- >>> length (6 :> 7 :> 8 :> Nil)
-- 3
length :: KnownNat n => Vec n a -> Int
length :: Vec n a -> Int
length = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> (Vec n a -> Integer) -> Vec n a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer) -> (Vec n a -> Proxy n) -> Vec n a -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec n a -> Proxy n
forall (n :: Nat) a. Vec n a -> Proxy n
asNatProxy
{-# NOINLINE length #-}

replace_int :: KnownNat n => Vec n a -> Int -> a -> Vec n a
replace_int :: Vec n a -> Int -> a -> Vec n a
replace_int xs :: Vec n a
xs i :: Int
i@(I# n0 :: Int#
n0) a :: a
a
  | Int# -> Bool
isTrue# (Int#
n0 Int# -> Int# -> Int#
<# 0#) = String -> Vec n a
forall a. HasCallStack => String -> a
error "Clash.Sized.Vector.replace: negative index"
  | Bool
otherwise          = Vec n a -> Int# -> a -> Vec n a
forall (m :: Nat) b. Vec m b -> Int# -> b -> Vec m b
sub Vec n a
xs Int#
n0 a
a
  where
    sub :: Vec m b -> Int# -> b -> Vec m b
    sub :: Vec m b -> Int# -> b -> Vec m b
sub Nil     _ _ = String -> Vec m b
forall a. HasCallStack => String -> a
error ([String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
P.concat [ "Clash.Sized.Vector.replace: index "
                                      , Int -> String
forall a. Show a => a -> String
show Int
i
                                      , " is larger than maximum index "
                                      , Int -> String
forall a. Show a => a -> String
show (Vec n a -> Int
forall (n :: Nat) a. KnownNat n => Vec n a -> Int
length Vec n a
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)
                                      ])
    sub (y :: b
y `Cons` (!Vec n b
ys)) n :: Int#
n b :: b
b = if Int# -> Bool
isTrue# (Int#
n Int# -> Int# -> Int#
==# 0#)
                                 then b
b b -> Vec n b -> Vec (n + 1) b
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Vec n b
ys
                                 else b
y b -> Vec n b -> Vec (n + 1) b
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Vec n b -> Int# -> b -> Vec n b
forall (m :: Nat) b. Vec m b -> Int# -> b -> Vec m b
sub Vec n b
ys (Int#
n Int# -> Int# -> Int#
-# 1#) b
b
{-# NOINLINE replace_int #-}

-- | \"'replace' @n a xs@\" returns the vector /xs/ where the /n/'th element is
-- replaced by /a/.
--
-- __NB__: vector elements have an __ASCENDING__ subscript starting from 0 and
-- ending at @'length' - 1@.
--
-- >>> replace 3 7 (1:>2:>3:>4:>5:>Nil)
-- <1,2,3,7,5>
-- >>> replace 0 7 (1:>2:>3:>4:>5:>Nil)
-- <7,2,3,4,5>
-- >>> replace 9 7 (1:>2:>3:>4:>5:>Nil)
-- <1,2,3,4,*** Exception: Clash.Sized.Vector.replace: index 9 is larger than maximum index 4
-- ...
replace :: (KnownNat n, Enum i) => i -> a -> Vec n a -> Vec n a
replace :: i -> a -> Vec n a -> Vec n a
replace i :: i
i y :: a
y xs :: Vec n a
xs = Vec n a -> Int -> a -> Vec n a
forall (n :: Nat) a. KnownNat n => Vec n a -> Int -> a -> Vec n a
replace_int Vec n a
xs (i -> Int
forall a. Enum a => a -> Int
fromEnum i
i) a
y
{-# INLINE replace #-}

-- | \"'take' @n xs@\" returns the /n/-length prefix of /xs/.
--
-- >>> take (SNat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
-- <1,2,3>
-- >>> take d3               (1:>2:>3:>4:>5:>Nil)
-- <1,2,3>
-- >>> take d0               (1:>2:>Nil)
-- <>
-- >>> take d4               (1:>2:>Nil)
-- <BLANKLINE>
-- <interactive>:...
--     • Couldn't match type ‘4 + n0’ with ‘2’
--       Expected type: Vec (4 + n0) a
--         Actual type: Vec (1 + 1) a
--       The type variable ‘n0’ is ambiguous
--     • In the second argument of ‘take’, namely ‘(1 :> 2 :> Nil)’
--       In the expression: take d4 (1 :> 2 :> Nil)
--       In an equation for ‘it’: it = take d4 (1 :> 2 :> Nil)
take :: SNat m -> Vec (m + n) a -> Vec m a
take :: SNat m -> Vec (m + n) a -> Vec m a
take n :: SNat m
n = (Vec m a, Vec n a) -> Vec m a
forall a b. (a, b) -> a
fst ((Vec m a, Vec n a) -> Vec m a)
-> (Vec (m + n) a -> (Vec m a, Vec n a))
-> Vec (m + n) a
-> Vec m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
forall (m :: Nat) (n :: Nat) a.
SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAt SNat m
n
{-# INLINE take #-}

-- | \"'takeI' @xs@\" returns the prefix of /xs/ as demanded by the context.
--
-- >>> takeI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
-- <1,2>
takeI :: KnownNat m => Vec (m + n) a -> Vec m a
takeI :: Vec (m + n) a -> Vec m a
takeI = (SNat m -> Vec (m + n) a -> Vec m a) -> Vec (m + n) a -> Vec m a
forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
withSNat SNat m -> Vec (m + n) a -> Vec m a
forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec m a
take
{-# INLINE takeI #-}

-- | \"'drop' @n xs@\" returns the suffix of /xs/ after the first /n/ elements.
--
-- >>> drop (SNat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
-- <4,5>
-- >>> drop d3               (1:>2:>3:>4:>5:>Nil)
-- <4,5>
-- >>> drop d0               (1:>2:>Nil)
-- <1,2>
-- >>> drop d4               (1:>2:>Nil)
-- <BLANKLINE>
-- <interactive>:...: error:
--     • Couldn't match...type ‘4 + n0...
--       The type variable ‘n0’ is ambiguous
--     • In the first argument of ‘print’, namely ‘it’
--       In a stmt of an interactive GHCi command: print it
drop :: SNat m -> Vec (m + n) a -> Vec n a
drop :: SNat m -> Vec (m + n) a -> Vec n a
drop n :: SNat m
n = (Vec m a, Vec n a) -> Vec n a
forall a b. (a, b) -> b
snd ((Vec m a, Vec n a) -> Vec n a)
-> (Vec (m + n) a -> (Vec m a, Vec n a))
-> Vec (m + n) a
-> Vec n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
forall (m :: Nat) (n :: Nat) a.
SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAt SNat m
n
{-# INLINE drop #-}

-- | \"'dropI' @xs@\" returns the suffix of /xs/ as demanded by the context.
--
-- >>> dropI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
-- <4,5>
dropI :: KnownNat m => Vec (m + n) a -> Vec n a
dropI :: Vec (m + n) a -> Vec n a
dropI = (SNat m -> Vec (m + n) a -> Vec n a) -> Vec (m + n) a -> Vec n a
forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
withSNat SNat m -> Vec (m + n) a -> Vec n a
forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec n a
drop
{-# INLINE dropI #-}

-- | \"'at' @n xs@\" returns /n/'th element of /xs/
--
-- __NB__: vector elements have an __ASCENDING__ subscript starting from 0 and
-- ending at @'length' - 1@.
--
-- >>> at (SNat :: SNat 1) (1:>2:>3:>4:>5:>Nil)
-- 2
-- >>> at d1               (1:>2:>3:>4:>5:>Nil)
-- 2
at :: SNat m -> Vec (m + (n + 1)) a -> a
at :: SNat m -> Vec (m + (n + 1)) a -> a
at n :: SNat m
n xs :: Vec (m + (n + 1)) a
xs = Vec (n + 1) a -> a
forall (n :: Nat) a. Vec (n + 1) a -> a
head (Vec (n + 1) a -> a) -> Vec (n + 1) a -> a
forall a b. (a -> b) -> a -> b
$ (Vec m a, Vec (n + 1) a) -> Vec (n + 1) a
forall a b. (a, b) -> b
snd ((Vec m a, Vec (n + 1) a) -> Vec (n + 1) a)
-> (Vec m a, Vec (n + 1) a) -> Vec (n + 1) a
forall a b. (a -> b) -> a -> b
$ SNat m -> Vec (m + (n + 1)) a -> (Vec m a, Vec (n + 1) a)
forall (m :: Nat) (n :: Nat) a.
SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAt SNat m
n Vec (m + (n + 1)) a
xs
{-# INLINE at #-}

-- | \"'select' @f s n xs@\" selects /n/ elements with step-size /s/ and
-- offset @f@ from /xs/.
--
-- >>> select (SNat :: SNat 1) (SNat :: SNat 2) (SNat :: SNat 3) (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
-- <2,4,6>
-- >>> select d1 d2 d3 (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
-- <2,4,6>
select :: (CmpNat (i + s) (s * n) ~ 'GT)
       => SNat f
       -> SNat s
       -> SNat n
       -> Vec (f + i) a
       -> Vec n a
select :: SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a
select f :: SNat f
f s :: SNat s
s n :: SNat n
n xs :: Vec (f + i) a
xs = UNat n -> Vec i a -> Vec n a
forall (n :: Nat) (i :: Nat) a. UNat n -> Vec i a -> Vec n a
select' (SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat SNat n
n) (Vec i a -> Vec n a) -> Vec i a -> Vec n a
forall a b. (a -> b) -> a -> b
$ SNat f -> Vec (f + i) a -> Vec i a
forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec n a
drop SNat f
f Vec (f + i) a
xs
  where
    select' :: UNat n -> Vec i a -> Vec n a
    select' :: UNat n -> Vec i a -> Vec n a
select' UZero      _               = Vec n a
forall a. Vec 0 a
Nil
    select' (USucc n' :: UNat n
n') vs :: Vec i a
vs@(x :: a
x `Cons` _) = a
x a -> Vec n a -> Vec (n + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons`
                                         UNat n -> Vec Any a -> Vec n a
forall (n :: Nat) (i :: Nat) a. UNat n -> Vec i a -> Vec n a
select' UNat n
n' (SNat s -> Vec (s + Any) a -> Vec Any a
forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec n a
drop SNat s
s (Vec i a -> Vec (s + Any) a
forall a b. a -> b
unsafeCoerce Vec i a
vs))
{-# NOINLINE select #-}

-- | \"'selectI' @f s xs@\" selects as many elements as demanded by the context
-- with step-size /s/ and offset /f/ from /xs/.
--
-- >>> selectI d1 d2 (1:>2:>3:>4:>5:>6:>7:>8:>Nil) :: Vec 2 Int
-- <2,4>
selectI :: (CmpNat (i + s) (s * n) ~ 'GT, KnownNat n)
        => SNat f
        -> SNat s
        -> Vec (f + i) a
        -> Vec n a
selectI :: SNat f -> SNat s -> Vec (f + i) a -> Vec n a
selectI f :: SNat f
f s :: SNat s
s xs :: Vec (f + i) a
xs = (SNat n -> Vec n a) -> Vec n a
forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
withSNat (\n :: SNat n
n -> SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a
forall (i :: Nat) (s :: Nat) (n :: Nat) (f :: Nat) a.
(CmpNat (i + s) (s * n) ~ 'GT) =>
SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a
select SNat f
f SNat s
s SNat n
n Vec (f + i) a
xs)
{-# INLINE selectI #-}

-- | \"'replicate' @n a@\" returns a vector that has /n/ copies of /a/.
--
-- >>> replicate (SNat :: SNat 3) 6
-- <6,6,6>
-- >>> replicate d3 6
-- <6,6,6>
replicate :: SNat n -> a -> Vec n a
replicate :: SNat n -> a -> Vec n a
replicate n :: SNat n
n a :: a
a = UNat n -> a -> Vec n a
forall (n :: Nat) a. UNat n -> a -> Vec n a
replicateU (SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat SNat n
n) a
a
{-# NOINLINE replicate #-}

replicateU :: UNat n -> a -> Vec n a
replicateU :: UNat n -> a -> Vec n a
replicateU UZero     _ = Vec n a
forall a. Vec 0 a
Nil
replicateU (USucc s :: UNat n
s) x :: a
x = a
x a -> Vec n a -> Vec (n + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` UNat n -> a -> Vec n a
forall (n :: Nat) a. UNat n -> a -> Vec n a
replicateU UNat n
s a
x

-- | \"'repeat' @a@\" creates a vector with as many copies of /a/ as demanded
-- by the context.
--
-- >>> repeat 6 :: Vec 5 Int
-- <6,6,6,6,6>
repeat :: KnownNat n => a -> Vec n a
repeat :: a -> Vec n a
repeat = (SNat n -> a -> Vec n a) -> a -> Vec n a
forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
withSNat SNat n -> a -> Vec n a
forall (n :: Nat) a. SNat n -> a -> Vec n a
replicate
{-# INLINE repeat #-}

-- | \"'iterate' @n f x@\" returns a vector starting with /x/ followed by
-- /n/ repeated applications of /f/ to /x/.
--
-- > iterate (SNat :: SNat 4) f x == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)
-- > iterate d4 f x               == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)
--
-- >>> iterate d4 (+1) 1
-- <1,2,3,4>
--
-- \"'iterate' @n f z@\" corresponds to the following circuit layout:
--
-- <<doc/iterate.svg>>
iterate :: SNat n -> (a -> a) -> a -> Vec n a
iterate :: SNat n -> (a -> a) -> a -> Vec n a
iterate SNat = (a -> a) -> a -> Vec n a
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI
{-# INLINE iterate #-}

-- | \"'iterate' @f x@\" returns a vector starting with @x@ followed by @n@
-- repeated applications of @f@ to @x@, where @n@ is determined by the context.
--
-- > iterateI f x :: Vec 3 a == (x :> f x :> f (f x) :> Nil)
--
-- >>> iterateI (+1) 1 :: Vec 3 Int
-- <1,2,3>
--
-- \"'iterateI' @f z@\" corresponds to the following circuit layout:
--
-- <<doc/iterate.svg>>
iterateI :: KnownNat n => (a -> a) -> a -> Vec n a
iterateI :: (a -> a) -> a -> Vec n a
iterateI f :: a -> a
f a :: a
a = Vec n a
xs
  where
    xs :: Vec n a
xs = Vec (n + 1) a -> Vec n a
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
init (a
a a -> Vec n a -> Vec (n + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Vec n a
ws)
    ws :: Vec n a
ws = (a -> a) -> Vec n a -> Vec n a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map a -> a
f (Vec n a -> Vec n a
forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
lazyV Vec n a
xs)
{-# INLINE iterateI #-}

-- | \"'generate' @n f x@\" returns a vector with @n@ repeated applications of
-- @f@ to @x@.
--
-- > generate (SNat :: SNat 4) f x == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)
-- > generate d4 f x               == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)
--
-- >>> generate d4 (+1) 1
-- <2,3,4,5>
--
-- \"'generate' @n f z@\" corresponds to the following circuit layout:
--
-- <<doc/generate.svg>>
generate :: SNat n -> (a -> a) -> a -> Vec n a
generate :: SNat n -> (a -> a) -> a -> Vec n a
generate SNat f :: a -> a
f a :: a
a = (a -> a) -> a -> Vec n a
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI a -> a
f (a -> a
f a
a)
{-# INLINE generate #-}

-- | \"'generateI' @f x@\" returns a vector with @n@ repeated applications of
-- @f@ to @x@, where @n@ is determined by the context.
--
-- > generateI f x :: Vec 3 a == (f x :> f (f x) :> f (f (f x)) :> Nil)
--
-- >>> generateI (+1) 1 :: Vec 3 Int
-- <2,3,4>
--
-- \"'generateI' @f z@\" corresponds to the following circuit layout:
--
-- <<doc/generate.svg>>
generateI :: KnownNat n => (a -> a) -> a -> Vec n a
generateI :: (a -> a) -> a -> Vec n a
generateI f :: a -> a
f a :: a
a = (a -> a) -> a -> Vec n a
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI a -> a
f (a -> a
f a
a)
{-# INLINE generateI #-}

-- | Transpose a matrix: go from row-major to column-major
--
-- >>> let xss = (1:>2:>Nil):>(3:>4:>Nil):>(5:>6:>Nil):>Nil
-- >>> xss
-- <<1,2>,<3,4>,<5,6>>
-- >>> transpose xss
-- <<1,3,5>,<2,4,6>>
transpose :: KnownNat n => Vec m (Vec n a) -> Vec n (Vec m a)
transpose :: Vec m (Vec n a) -> Vec n (Vec m a)
transpose = (Vec n a -> Vec n a) -> Vec m (Vec n a) -> Vec n (Vec m a)
forall a (f :: Type -> Type) b (n :: Nat).
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse# Vec n a -> Vec n a
forall a. a -> a
id
{-# NOINLINE transpose #-}

-- | 1-dimensional stencil computations
--
-- \"'stencil1d' @stX f xs@\", where /xs/ has /stX + n/ elements, applies the
-- stencil computation /f/ on: /n + 1/ overlapping (1D) windows of length /stX/,
-- drawn from /xs/. The resulting vector has /n + 1/ elements.
--
-- >>> let xs = (1:>2:>3:>4:>5:>6:>Nil)
-- >>> :t xs
-- xs :: Num a => Vec 6 a
-- >>> :t stencil1d d2 sum xs
-- stencil1d d2 sum xs :: Num b => Vec 5 b
-- >>> stencil1d d2 sum xs
-- <3,5,7,9,11>
stencil1d :: KnownNat n
          => SNat (stX + 1) -- ^ Windows length /stX/, at least size 1
          -> (Vec (stX + 1) a -> b) -- ^ The stencil (function)
          -> Vec ((stX + n) + 1) a
          -> Vec (n + 1) b
stencil1d :: SNat (stX + 1)
-> (Vec (stX + 1) a -> b) -> Vec ((stX + n) + 1) a -> Vec (n + 1) b
stencil1d stX :: SNat (stX + 1)
stX f :: Vec (stX + 1) a -> b
f xs :: Vec ((stX + n) + 1) a
xs = (Vec (stX + 1) a -> b)
-> Vec (n + 1) (Vec (stX + 1) a) -> Vec (n + 1) b
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map Vec (stX + 1) a -> b
f (SNat (stX + 1)
-> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
forall (n :: Nat) (stX :: Nat) a.
KnownNat n =>
SNat (stX + 1)
-> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
windows1d SNat (stX + 1)
stX Vec ((stX + n) + 1) a
xs)
{-# INLINE stencil1d #-}

-- | 2-dimensional stencil computations
--
-- \"'stencil2d' @stY stX f xss@\", where /xss/ is a matrix of /stY + m/ rows
-- of /stX + n/ elements, applies the stencil computation /f/ on:
-- /(m + 1) * (n + 1)/ overlapping (2D) windows of /stY/ rows of /stX/ elements,
-- drawn from /xss/. The result matrix has /m + 1/ rows of /n + 1/ elements.
--
-- >>> let xss = ((1:>2:>3:>4:>Nil):>(5:>6:>7:>8:>Nil):>(9:>10:>11:>12:>Nil):>(13:>14:>15:>16:>Nil):>Nil)
-- >>> :t xss
-- xss :: Num a => Vec 4 (Vec 4 a)
-- >>> :t stencil2d d2 d2 (sum . map sum) xss
-- stencil2d d2 d2 (sum . map sum) xss :: Num b => Vec 3 (Vec 3 b)
-- >>> stencil2d d2 d2 (sum . map sum) xss
-- <<14,18,22>,<30,34,38>,<46,50,54>>
stencil2d :: (KnownNat n, KnownNat m)
          => SNat (stY + 1) -- ^ Window hight /stY/, at least size 1
          -> SNat (stX + 1) -- ^ Window width /stX/, at least size 1
          -> (Vec (stY + 1) (Vec (stX + 1) a) -> b) -- ^ The stencil (function)
          -> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
          -> Vec (m + 1) (Vec (n + 1) b)
stencil2d :: SNat (stY + 1)
-> SNat (stX + 1)
-> (Vec (stY + 1) (Vec (stX + 1) a) -> b)
-> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
-> Vec (m + 1) (Vec (n + 1) b)
stencil2d stY :: SNat (stY + 1)
stY stX :: SNat (stX + 1)
stX f :: Vec (stY + 1) (Vec (stX + 1) a) -> b
f xss :: Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
xss = ((Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)) -> Vec (n + 1) b)
-> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
-> Vec (m + 1) (Vec (n + 1) b)
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map((Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)) -> Vec (n + 1) b)
 -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
 -> Vec (m + 1) (Vec (n + 1) b))
-> ((Vec (stY + 1) (Vec (stX + 1) a) -> b)
    -> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)) -> Vec (n + 1) b)
-> (Vec (stY + 1) (Vec (stX + 1) a) -> b)
-> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
-> Vec (m + 1) (Vec (n + 1) b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Vec (stY + 1) (Vec (stX + 1) a) -> b)
-> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)) -> Vec (n + 1) b
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map) Vec (stY + 1) (Vec (stX + 1) a) -> b
f (SNat (stY + 1)
-> SNat (stX + 1)
-> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
-> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
forall (n :: Nat) (m :: Nat) (stY :: Nat) (stX :: Nat) a.
(KnownNat n, KnownNat m) =>
SNat (stY + 1)
-> SNat (stX + 1)
-> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
-> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
windows2d SNat (stY + 1)
stY SNat (stX + 1)
stX Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
xss)
{-# INLINE stencil2d #-}

-- | \"'windows1d' @stX xs@\", where the vector /xs/ has /stX + n/ elements,
-- returns a vector of /n + 1/ overlapping (1D) windows of /xs/ of length /stX/.
--
-- >>> let xs = (1:>2:>3:>4:>5:>6:>Nil)
-- >>> :t xs
-- xs :: Num a => Vec 6 a
-- >>> :t windows1d d2 xs
-- windows1d d2 xs :: Num a => Vec 5 (Vec 2 a)
-- >>> windows1d d2 xs
-- <<1,2>,<2,3>,<3,4>,<4,5>,<5,6>>
windows1d :: KnownNat n
          => SNat (stX + 1) -- ^ Length of the window, at least size 1
          -> Vec ((stX + n) + 1) a
          -> Vec (n + 1) (Vec (stX + 1) a)
windows1d :: SNat (stX + 1)
-> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
windows1d stX :: SNat (stX + 1)
stX xs :: Vec ((stX + n) + 1) a
xs = (Vec ((stX + 1) + n) a -> Vec (stX + 1) a)
-> Vec (n + 1) (Vec ((stX + 1) + n) a)
-> Vec (n + 1) (Vec (stX + 1) a)
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (SNat (stX + 1) -> Vec ((stX + 1) + n) a -> Vec (stX + 1) a
forall (m :: Nat) (n :: Nat) a. SNat m -> Vec (m + n) a -> Vec m a
take SNat (stX + 1)
stX) (Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec ((stX + n) + 1) a)
forall (n :: Nat) (n :: Nat) a.
KnownNat n =>
Vec (n + 1) a -> Vec n (Vec (n + 1) a)
rotations Vec ((stX + n) + 1) a
xs)
  where
    rotateL :: Vec (n + 1) a -> Vec (n + 1) a
rotateL ys :: Vec (n + 1) a
ys   = Vec (n + 1) a -> Vec n a
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
tail Vec (n + 1) a
ys Vec n a -> a -> Vec (n + 1) a
forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
:< Vec (n + 1) a -> a
forall (n :: Nat) a. Vec (n + 1) a -> a
head Vec (n + 1) a
ys
    rotations :: Vec (n + 1) a -> Vec n (Vec (n + 1) a)
rotations ys :: Vec (n + 1) a
ys = (Vec (n + 1) a -> Vec (n + 1) a)
-> Vec (n + 1) a -> Vec n (Vec (n + 1) a)
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI Vec (n + 1) a -> Vec (n + 1) a
forall (n :: Nat) a. Vec (n + 1) a -> Vec (n + 1) a
rotateL Vec (n + 1) a
ys
{-# INLINE windows1d #-}

-- | \"'windows2d' @stY stX xss@\", where matrix /xss/ has /stY + m/ rows of
-- /stX + n/, returns a matrix of /m+1/ rows of /n+1/ elements. The elements
-- of this new matrix are the overlapping (2D) windows of /xss/, where every
-- window has /stY/ rows of /stX/ elements.
--
-- >>> let xss = ((1:>2:>3:>4:>Nil):>(5:>6:>7:>8:>Nil):>(9:>10:>11:>12:>Nil):>(13:>14:>15:>16:>Nil):>Nil)
-- >>> :t xss
-- xss :: Num a => Vec 4 (Vec 4 a)
-- >>> :t windows2d d2 d2 xss
-- windows2d d2 d2 xss :: Num a => Vec 3 (Vec 3 (Vec 2 (Vec 2 a)))
-- >>> windows2d d2 d2 xss
-- <<<<1,2>,<5,6>>,<<2,3>,<6,7>>,<<3,4>,<7,8>>>,<<<5,6>,<9,10>>,<<6,7>,<10,11>>,<<7,8>,<11,12>>>,<<<9,10>,<13,14>>,<<10,11>,<14,15>>,<<11,12>,<15,16>>>>
windows2d :: (KnownNat n,KnownNat m)
          => SNat (stY + 1) -- ^ Window hight /stY/, at least size 1
          -> SNat (stX + 1) -- ^ Window width /stX/, at least size 1
          -> Vec ((stY + m) + 1) (Vec (stX + n + 1) a)
          -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
windows2d :: SNat (stY + 1)
-> SNat (stX + 1)
-> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
-> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
windows2d stY :: SNat (stY + 1)
stY stX :: SNat (stX + 1)
stX xss :: Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
xss = (Vec (stY + 1) (Vec ((stX + n) + 1) a)
 -> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
-> Vec (m + 1) (Vec (stY + 1) (Vec ((stX + n) + 1) a))
-> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (Vec (stY + 1) (Vec (n + 1) (Vec (stX + 1) a))
-> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a))
forall (n :: Nat) (m :: Nat) a.
KnownNat n =>
Vec m (Vec n a) -> Vec n (Vec m a)
transpose (Vec (stY + 1) (Vec (n + 1) (Vec (stX + 1) a))
 -> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
-> (Vec (stY + 1) (Vec ((stX + n) + 1) a)
    -> Vec (stY + 1) (Vec (n + 1) (Vec (stX + 1) a)))
-> Vec (stY + 1) (Vec ((stX + n) + 1) a)
-> Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a))
-> Vec (stY + 1) (Vec ((stX + n) + 1) a)
-> Vec (stY + 1) (Vec (n + 1) (Vec (stX + 1) a))
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (SNat (stX + 1)
-> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
forall (n :: Nat) (stX :: Nat) a.
KnownNat n =>
SNat (stX + 1)
-> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
windows1d SNat (stX + 1)
stX))) (SNat (stY + 1)
-> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
-> Vec (m + 1) (Vec (stY + 1) (Vec ((stX + n) + 1) a))
forall (n :: Nat) (stX :: Nat) a.
KnownNat n =>
SNat (stX + 1)
-> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
windows1d SNat (stY + 1)
stY Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)
xss)
{-# INLINE windows2d #-}

-- | Forward permutation specified by an index mapping, /ix/. The result vector
-- is initialized by the given defaults, /def/, and an further values that are
-- permuted into the result are added to the current value using the given
-- combination function, /f/.
--
-- The combination function must be /associative/ and /commutative/.
permute :: (Enum i, KnownNat n, KnownNat m)
        => (a -> a -> a)  -- ^ Combination function, /f/
        -> Vec n a        -- ^ Default values, /def/
        -> Vec m i        -- ^ Index mapping, /is/
        -> Vec (m + k) a  -- ^ Vector to be permuted, /xs/
        -> Vec n a
permute :: (a -> a -> a) -> Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
permute f :: a -> a -> a
f defs :: Vec n a
defs is :: Vec m i
is xs :: Vec (m + k) a
xs = Vec n a
ys
  where
    ixs :: Vec m (i, a)
ixs = Vec m i -> Vec m a -> Vec m (i, a)
forall (n :: Nat) a b. Vec n a -> Vec n b -> Vec n (a, b)
zip Vec m i
is (Vec (m + k) a -> Vec m a
forall (m :: Nat) (n :: Nat) a.
KnownNat m =>
Vec (m + n) a -> Vec m a
takeI Vec (m + k) a
xs)
    ys :: Vec n a
ys  = (Vec n a -> (i, a) -> Vec n a)
-> Vec n a -> Vec m (i, a) -> Vec n a
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl (\ks :: Vec n a
ks (i :: i
i,x :: a
x) -> let ki :: a
ki = Vec n a
ksVec n a -> i -> a
forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
!!i
i in i -> a -> Vec n a -> Vec n a
forall (n :: Nat) i a.
(KnownNat n, Enum i) =>
i -> a -> Vec n a -> Vec n a
replace i
i (a -> a -> a
f a
x a
ki) Vec n a
ks) Vec n a
defs Vec m (i, a)
ixs
{-# INLINE permute #-}

-- | Backwards permutation specified by an index mapping, /is/, from the
-- destination vector specifying which element of the source vector /xs/ to
-- read.
--
-- \"'backpermute' @xs is@\" is equivalent to \"'map' @(xs '!!') is@\".
--
-- For example:
--
-- >>> let input = 1:>9:>6:>4:>4:>2:>0:>1:>2:>Nil
-- >>> let from  = 1:>3:>7:>2:>5:>3:>Nil
-- >>> backpermute input from
-- <9,4,1,6,2,4>
backpermute :: (Enum i, KnownNat n)
            => Vec n a  -- ^ Source vector, /xs/
            -> Vec m i  -- ^ Index mapping, /is/
            -> Vec m a
backpermute :: Vec n a -> Vec m i -> Vec m a
backpermute xs :: Vec n a
xs = (i -> a) -> Vec m i -> Vec m a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (Vec n a
xsVec n a -> i -> a
forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
!!)
{-# INLINE backpermute #-}

-- | Copy elements from the source vector, /xs/, to the destination vector
-- according to an index mapping /is/. This is a forward permute operation where
-- a /to/ vector encodes an input to output index mapping. Output elements for
-- indices that are not mapped assume the value in the default vector /def/.
--
-- For example:
--
-- >>> let defVec = 0:>0:>0:>0:>0:>0:>0:>0:>0:>Nil
-- >>> let to = 1:>3:>7:>2:>5:>8:>Nil
-- >>> let input = 1:>9:>6:>4:>4:>2:>5:>Nil
-- >>> scatter defVec to input
-- <0,1,4,9,0,4,0,6,2>
--
-- __NB__: If the same index appears in the index mapping more than once, the
-- latest mapping is chosen.
scatter :: (Enum i, KnownNat n, KnownNat m)
        => Vec n a       -- ^ Default values, /def/
        -> Vec m i       -- ^ Index mapping, /is/
        -> Vec (m + k) a -- ^ Vector to be scattered, /xs/
        -> Vec n a
scatter :: Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
scatter = (a -> a -> a) -> Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
forall i (n :: Nat) (m :: Nat) a (k :: Nat).
(Enum i, KnownNat n, KnownNat m) =>
(a -> a -> a) -> Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
permute a -> a -> a
forall a b. a -> b -> a
const
{-# INLINE scatter #-}

-- | Backwards permutation specified by an index mapping, /is/, from the
-- destination vector specifying which element of the source vector /xs/ to
-- read.
--
-- \"'gather' @xs is@\" is equivalent to \"'map' @(xs '!!') is@\".
--
-- For example:
--
-- >>> let input = 1:>9:>6:>4:>4:>2:>0:>1:>2:>Nil
-- >>> let from  = 1:>3:>7:>2:>5:>3:>Nil
-- >>> gather input from
-- <9,4,1,6,2,4>
gather :: (Enum i, KnownNat n)
       => Vec n a  -- ^ Source vector, /xs/
       -> Vec m i  -- ^ Index mapping, /is/
       -> Vec m a
gather :: Vec n a -> Vec m i -> Vec m a
gather xs :: Vec n a
xs = (i -> a) -> Vec m i -> Vec m a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (Vec n a
xsVec n a -> i -> a
forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
!!)
{-# INLINE gather #-}

-- | \"'interleave' @d xs@\" creates a vector:
--
-- @
-- \<x_0,x_d,x_(2d),...,x_1,x_(d+1),x_(2d+1),...,x_(d-1),x_(2d-1),x_(3d-1)\>
-- @
--
-- >>> let xs = 1 :> 2 :> 3 :> 4 :> 5 :> 6 :> 7 :> 8 :> 9 :> Nil
-- >>> interleave d3 xs
-- <1,4,7,2,5,8,3,6,9>
interleave :: (KnownNat n, KnownNat d)
           => SNat d -- ^ Interleave step, /d/
           -> Vec (n * d) a
           -> Vec (d * n) a
interleave :: SNat d -> Vec (n * d) a -> Vec (d * n) a
interleave d :: SNat d
d = Vec d (Vec n a) -> Vec (d * n) a
forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (n * m) a
concat (Vec d (Vec n a) -> Vec (d * n) a)
-> (Vec (n * d) a -> Vec d (Vec n a))
-> Vec (n * d) a
-> Vec (d * n) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec n (Vec d a) -> Vec d (Vec n a)
forall (n :: Nat) (m :: Nat) a.
KnownNat n =>
Vec m (Vec n a) -> Vec n (Vec m a)
transpose (Vec n (Vec d a) -> Vec d (Vec n a))
-> (Vec (n * d) a -> Vec n (Vec d a))
-> Vec (n * d) a
-> Vec d (Vec n a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat d -> Vec (n * d) a -> Vec n (Vec d a)
forall (n :: Nat) (m :: Nat) a.
KnownNat n =>
SNat m -> Vec (n * m) a -> Vec n (Vec m a)
unconcat SNat d
d
{-# INLINE interleave #-}

-- | /Dynamically/ rotate a 'Vec'tor to the left:
--
-- >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
-- >>> rotateLeft xs 1
-- <2,3,4,1>
-- >>> rotateLeft xs 2
-- <3,4,1,2>
-- >>> rotateLeft xs (-1)
-- <4,1,2,3>
--
-- __NB:__ use `rotateLeftS` if you want to rotate left by a /static/ amount.
rotateLeft :: (Enum i, KnownNat n)
           => Vec n a
           -> i
           -> Vec n a
rotateLeft :: Vec n a -> i -> Vec n a
rotateLeft xs :: Vec n a
xs i :: i
i = (Int -> a) -> Vec n Int -> Vec n a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map ((Vec n a
xs Vec n a -> Int -> a
forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
!!) (Int -> a) -> (Int -> Int) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
len)) ((Int -> Int) -> Int -> Vec n Int
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI (Int -> Int -> Int
forall a. Num a => a -> a -> a
+1) Int
i')
  where
    i' :: Int
i'  = i -> Int
forall a. Enum a => a -> Int
fromEnum i
i
    len :: Int
len = Vec n a -> Int
forall (n :: Nat) a. KnownNat n => Vec n a -> Int
length Vec n a
xs
{-# INLINE rotateLeft #-}

-- | /Dynamically/ rotate a 'Vec'tor to the right:
--
-- >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
-- >>> rotateRight xs 1
-- <4,1,2,3>
-- >>> rotateRight xs 2
-- <3,4,1,2>
-- >>> rotateRight xs (-1)
-- <2,3,4,1>
--
-- __NB:__ use `rotateRightS` if you want to rotate right by a /static/ amount.
rotateRight :: (Enum i, KnownNat n)
            => Vec n a
            -> i
            -> Vec n a
rotateRight :: Vec n a -> i -> Vec n a
rotateRight xs :: Vec n a
xs i :: i
i = (Int -> a) -> Vec n Int -> Vec n a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map ((Vec n a
xs Vec n a -> Int -> a
forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
!!) (Int -> a) -> (Int -> Int) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
len)) ((Int -> Int) -> Int -> Vec n Int
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI (Int -> Int -> Int
forall a. Num a => a -> a -> a
+1) Int
i')
  where
    i' :: Int
i'  = Int -> Int
forall a. Num a => a -> a
negate (i -> Int
forall a. Enum a => a -> Int
fromEnum i
i)
    len :: Int
len = Vec n a -> Int
forall (n :: Nat) a. KnownNat n => Vec n a -> Int
length Vec n a
xs
{-# INLINE rotateRight #-}

-- | /Statically/ rotate a 'Vec'tor to the left:
--
-- >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
-- >>> rotateLeftS xs d1
-- <2,3,4,1>
--
-- __NB:__ use `rotateLeft` if you want to rotate left by a /dynamic/ amount.
rotateLeftS :: KnownNat n
            => Vec n a
            -> SNat d
            -> Vec n a
rotateLeftS :: Vec n a -> SNat d -> Vec n a
rotateLeftS xs :: Vec n a
xs d :: SNat d
d = Integer -> Vec n a -> Vec n a
forall (k :: Nat) a. Integer -> Vec k a -> Vec k a
go (SNat d -> Integer
forall (n :: Nat). SNat n -> Integer
snatToInteger SNat d
d Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Vec n a -> Proxy n
forall (n :: Nat) a. Vec n a -> Proxy n
asNatProxy Vec n a
xs)) Vec n a
xs
  where
    go :: Integer -> Vec k a -> Vec k a
    go :: Integer -> Vec k a -> Vec k a
go _ Nil           = Vec k a
forall a. Vec 0 a
Nil
    go 0 ys :: Vec k a
ys            = Vec k a
ys
    go n :: Integer
n (y :: a
y `Cons` ys :: Vec n a
ys) = Integer -> Vec k a -> Vec k a
forall (k :: Nat) a. Integer -> Vec k a -> Vec k a
go (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-1) (Vec n a
ys Vec n a -> a -> Vec (n + 1) a
forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
:< a
y)
{-# NOINLINE rotateLeftS #-}

-- | /Statically/ rotate a 'Vec'tor to the right:
--
-- >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
-- >>> rotateRightS xs d1
-- <4,1,2,3>
--
-- __NB:__ use `rotateRight` if you want to rotate right by a /dynamic/ amount.
rotateRightS :: KnownNat n
             => Vec n a
             -> SNat d
             -> Vec n a
rotateRightS :: Vec n a -> SNat d -> Vec n a
rotateRightS xs :: Vec n a
xs d :: SNat d
d = Integer -> Vec n a -> Vec n a
forall a (a :: Nat) b. (Eq a, Num a) => a -> Vec a b -> Vec a b
go (SNat d -> Integer
forall (n :: Nat). SNat n -> Integer
snatToInteger SNat d
d Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Vec n a -> Proxy n
forall (n :: Nat) a. Vec n a -> Proxy n
asNatProxy Vec n a
xs)) Vec n a
xs
  where
    go :: a -> Vec a b -> Vec a b
go _ Nil            = Vec a b
forall a. Vec 0 a
Nil
    go 0 ys :: Vec a b
ys             = Vec a b
ys
    go n :: a
n ys :: Vec a b
ys@(Cons _ _)  = a -> Vec a b -> Vec a b
go (a
na -> a -> a
forall a. Num a => a -> a -> a
-1) (Vec (n + 1) b -> b
forall (n :: Nat) a. Vec (n + 1) a -> a
last Vec a b
Vec (n + 1) b
ys b -> Vec n b -> Vec (n + 1) b
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec (n + 1) b -> Vec n b
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
init Vec a b
Vec (n + 1) b
ys)
{-# NOINLINE rotateRightS #-}

-- | Convert a vector to a list.
--
-- >>> toList (1:>2:>3:>Nil)
-- [1,2,3]
toList :: Vec n a -> [a]
toList :: Vec n a -> [a]
toList = (a -> [a] -> [a]) -> [a] -> Vec n a -> [a]
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr (:) []
{-# INLINE toList #-}

-- | Create a vector literal from a list literal.
--
-- > $(listToVecTH [1::Signed 8,2,3,4,5]) == (8:>2:>3:>4:>5:>Nil) :: Vec 5 (Signed 8)
--
-- >>> [1 :: Signed 8,2,3,4,5]
-- [1,2,3,4,5]
-- >>> $(listToVecTH [1::Signed 8,2,3,4,5])
-- <1,2,3,4,5>
listToVecTH :: Lift a => [a] -> ExpQ
listToVecTH :: [a] -> ExpQ
listToVecTH []     = [| Nil |]
listToVecTH (x :: a
x:xs :: [a]
xs) = [| x :> $(listToVecTH xs) |]

-- | 'Vec'tor as a 'Proxy' for 'Nat'
asNatProxy :: Vec n a -> Proxy n
asNatProxy :: Vec n a -> Proxy n
asNatProxy _ = Proxy n
forall k (t :: k). Proxy t
Proxy

-- | Length of a 'Vec'tor as an 'SNat' value
lengthS :: KnownNat n => Vec n a -> SNat n
lengthS :: Vec n a -> SNat n
lengthS _ = SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat
{-# INLINE lengthS #-}

-- | What you should use when your vector functions are too strict in their
-- arguments.
--
-- For example:
--
-- @
-- -- Bubble sort for 1 iteration
-- sortV xs = 'map' fst sorted ':<' (snd ('last' sorted))
--  where
--    lefts  = 'head' xs :> 'map' snd ('init' sorted)
--    rights = 'tail' xs
--    sorted = 'zipWith' compareSwapL lefts rights
--
-- -- Compare and swap
-- compareSwapL a b = if a < b then (a,b)
--                             else (b,a)
-- @
--
-- Will not terminate because 'zipWith' is too strict in its second argument.
--
-- In this case, adding 'lazyV' on 'zipWith's second argument:
--
-- @
-- sortVL xs = 'map' fst sorted ':<' (snd ('last' sorted))
--  where
--    lefts  = 'head' xs :> map snd ('init' sorted)
--    rights = 'tail' xs
--    sorted = 'zipWith' compareSwapL ('lazyV' lefts) rights
-- @
--
-- Results in a successful computation:
--
-- >>> sortVL (4 :> 1 :> 2 :> 3 :> Nil)
-- <1,2,3,4>
--
-- __NB__: There is also a solution using 'flip', but it slightly obfuscates the
-- meaning of the code:
--
-- @
-- sortV_flip xs = 'map' fst sorted ':<' (snd ('last' sorted))
--  where
--    lefts  = 'head' xs :> 'map' snd ('init' sorted)
--    rights = 'tail' xs
--    sorted = 'zipWith' ('flip' compareSwapL) rights lefts
-- @
--
-- >>> sortV_flip (4 :> 1 :> 2 :> 3 :> Nil)
-- <1,2,3,4>
lazyV :: KnownNat n
      => Vec n a
      -> Vec n a
lazyV :: Vec n a -> Vec n a
lazyV = Vec n () -> Vec n a -> Vec n a
forall (n :: Nat) a. Vec n () -> Vec n a -> Vec n a
lazyV' (() -> Vec n ()
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat ())
  where
    lazyV' :: Vec n () -> Vec n a -> Vec n a
    lazyV' :: Vec n () -> Vec n a -> Vec n a
lazyV' Nil           _  = Vec n a
forall a. Vec 0 a
Nil
    lazyV' (_ `Cons` xs :: Vec n ()
xs) ys :: Vec n a
ys = Vec (n + 1) a -> a
forall (n :: Nat) a. Vec (n + 1) a -> a
head Vec n a
Vec (n + 1) a
ys a -> Vec n a -> Vec (n + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
`Cons` Vec n () -> Vec n a -> Vec n a
forall (n :: Nat) a. Vec n () -> Vec n a -> Vec n a
lazyV' Vec n ()
xs (Vec (n + 1) a -> Vec n a
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
tail Vec n a
Vec (n + 1) a
ys)
{-# NOINLINE lazyV #-}

-- | A /dependently/ typed fold.
--
-- Using lists, we can define /append/ (a.k.a. @Data.List.@'Data.List.++') in
-- terms of @Data.List.@'Data.List.foldr':
--
-- >>> import qualified Data.List
-- >>> let append xs ys = Data.List.foldr (:) ys xs
-- >>> append [1,2] [3,4]
-- [1,2,3,4]
--
-- However, when we try to do the same for 'Vec', by defining /append'/ in terms
-- of @Clash.Sized.Vector.@'foldr':
--
-- @
-- append' xs ys = 'foldr' (:>) ys xs
-- @
--
-- we get a type error:
--
-- @
-- __>>> let append' xs ys = foldr (:>) ys xs__
--
-- \<interactive\>:...
--     • Occurs check: cannot construct the infinite type: ... ~ ... + 1
--       Expected type: a -> Vec ... a -> Vec ... a
--         Actual type: a -> Vec ... a -> Vec (... + 1) a
--     • In the first argument of ‘foldr’, namely ‘(:>)’
--       In the expression: foldr (:>) ys xs
--       In an equation for ‘append'’: append' xs ys = foldr (:>) ys xs
--     • Relevant bindings include
--         ys :: Vec ... a (bound at ...)
--         append' :: Vec n a -> Vec ... a -> Vec ... a
--           (bound at ...)
-- @
--
-- The reason is that the type of 'foldr' is:
--
-- >>> :t foldr
-- foldr :: (a -> b -> b) -> b -> Vec n a -> b
--
-- While the type of (':>') is:
--
-- >>> :t (:>)
-- (:>) :: a -> Vec n a -> Vec (n + 1) a
--
-- We thus need a @fold@ function that can handle the growing vector type:
-- 'dfold'. Compared to 'foldr', 'dfold' takes an extra parameter, called the
-- /motive/, that allows the folded function to have an argument and result type
-- that /depends/ on the current length of the vector. Using 'dfold', we can
-- now correctly define /append'/:
--
-- @
-- import Data.Singletons.Prelude
-- import Data.Proxy
--
-- data Append (m :: Nat) (a :: *) (f :: 'TyFun' Nat *) :: *
-- type instance 'Apply' (Append m a) l = 'Vec' (l + m) a
--
-- append' xs ys = 'dfold' (Proxy :: Proxy (Append m a)) (const (':>')) ys xs
-- @
--
-- We now see that /append'/ has the appropriate type:
--
-- >>> :t append'
-- append' :: KnownNat k => Vec k a -> Vec m a -> Vec (k + m) a
--
-- And that it works:
--
-- >>> append' (1 :> 2 :> Nil) (3 :> 4 :> Nil)
-- <1,2,3,4>
--
-- __NB__: \"@'dfold' m f z xs@\" creates a linear structure, which has a depth,
-- or delay, of O(@'length' xs@). Look at 'dtfold' for a /dependently/ typed
-- fold that produces a structure with a depth of O(log_2(@'length' xs@)).
dfold :: forall p k a . KnownNat k
      => Proxy (p :: TyFun Nat Type -> Type) -- ^ The /motive/
      -> (forall l . SNat l -> a -> (p @@ l) -> (p @@ (l + 1)))
      -- ^ Function to fold.
      --
      -- __NB__: The @SNat l@ is __not__ the index (see (`!!`)) to the
      -- element /a/. @SNat l@ is the number of elements that occur to the
      -- right of /a/.
      -> (p @@ 0) -- ^ Initial element
      -> Vec k a -- ^ Vector to fold over
      -> (p @@ k)
dfold :: Proxy p
-> (forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1))
-> (p @@ 0)
-> Vec k a
-> p @@ k
dfold _ f :: forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1)
f z :: p @@ 0
z xs :: Vec k a
xs = SNat k -> Vec k a -> p @@ k
forall (n :: Nat). SNat n -> Vec n a -> p @@ n
go (Proxy k -> SNat k
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> SNat n
snatProxy (Vec k a -> Proxy k
forall (n :: Nat) a. Vec n a -> Proxy n
asNatProxy Vec k a
xs)) Vec k a
xs
  where
    go :: SNat n -> Vec n a -> (p @@ n)
    go :: SNat n -> Vec n a -> p @@ n
go _ Nil                        = p @@ n
p @@ 0
z
    go s :: SNat n
s (y :: a
y `Cons` (Vec n a
ys :: Vec z a)) =
      let s' :: SNat n
s' = SNat n
SNat (n + 1)
s SNat (n + 1) -> SNat 1 -> SNat n
forall (a :: Nat) (b :: Nat). SNat (a + b) -> SNat b -> SNat a
`subSNat` SNat 1
d1
      in  SNat n -> a -> (p @@ n) -> p @@ (n + 1)
forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1)
f SNat n
s' a
y (SNat n -> Vec n a -> p @@ n
forall (n :: Nat). SNat n -> Vec n a -> p @@ n
go SNat n
s' Vec n a
ys)
{-# NOINLINE dfold #-}

-- | A combination of 'dfold' and 'fold': a /dependently/ typed fold that
-- reduces a vector in a tree-like structure.
--
-- As an example of when you might want to use 'dtfold' we will build a
-- population counter: a circuit that counts the number of bits set to '1' in
-- a 'BitVector'. Given a vector of /n/ bits, we only need we need a data type
-- that can represent the number /n/: 'Index' @(n+1)@. 'Index' @k@ has a range
-- of @[0 .. k-1]@ (using @ceil(log2(k))@ bits), hence we need 'Index' @n+1@.
-- As an initial attempt we will use 'sum', because it gives a nice (@log2(n)@)
-- tree-structure of adders:
--
-- @
-- populationCount :: (KnownNat (n+1), KnownNat (n+2))
--                 => 'BitVector' (n+1) -> 'Index' (n+2)
-- populationCount = sum . map fromIntegral . 'bv2v'
-- @
--
-- The \"problem\" with this description is that all adders have the same
-- bit-width, i.e. all adders are of the type:
--
-- @
-- (+) :: 'Index' (n+2) -> 'Index' (n+2) -> 'Index' (n+2).
-- @
--
-- This is a \"problem\" because we could have a more efficient structure:
-- one where each layer of adders is /precisely/ wide enough to count the number
-- of bits at that layer. That is, at height /d/ we want the adder to be of
-- type:
--
-- @
-- 'Index' ((2^d)+1) -> 'Index' ((2^d)+1) -> 'Index' ((2^(d+1))+1)
-- @
--
-- We have such an adder in the form of the 'Clash.Class.Num.add' function, as
-- defined in the instance 'Clash.Class.Num.ExtendingNum' instance of 'Index'.
-- However, we cannot simply use 'fold' to create a tree-structure of
-- 'Clash.Class.Num.add'es:
--
-- >>> :{
-- let populationCount' :: (KnownNat (n+1), KnownNat (n+2))
--                      => BitVector (n+1) -> Index (n+2)
--     populationCount' = fold add . map fromIntegral . bv2v
-- :}
-- <BLANKLINE>
-- <interactive>:...
--     • Couldn't match type ‘((n + 2) + (n + 2)) - 1’ with ‘n + 2’
--       Expected type: Index (n + 2) -> Index (n + 2) -> Index (n + 2)
--         Actual type: Index (n + 2)
--                      -> Index (n + 2) -> AResult (Index (n + 2)) (Index (n + 2))
--     • In the first argument of ‘fold’, namely ‘add’
--       In the first argument of ‘(.)’, namely ‘fold add’
--       In the expression: fold add . map fromIntegral . bv2v
--     • Relevant bindings include
--         populationCount' :: BitVector (n + 1) -> Index (n + 2)
--           (bound at ...)
--
-- because 'fold' expects a function of type \"@a -> a -> a@\", i.e. a function
-- where the arguments and result all have exactly the same type.
--
-- In order to accommodate the type of our 'Clash.Class.Num.add', where the
-- result is larger than the arguments, we must use a dependently typed fold in
-- the form of 'dtfold':
--
-- @
-- {\-\# LANGUAGE UndecidableInstances \#-\}
-- import Data.Singletons.Prelude
-- import Data.Proxy
--
-- data IIndex (f :: 'TyFun' Nat *) :: *
-- type instance 'Apply' IIndex l = 'Index' ((2^l)+1)
--
-- populationCount' :: (KnownNat k, KnownNat (2^k))
--                  => BitVector (2^k) -> Index ((2^k)+1)
-- populationCount' bv = 'dtfold' (Proxy @IIndex)
--                              fromIntegral
--                              (\\_ x y -> 'Clash.Class.Num.add' x y)
--                              ('bv2v' bv)
-- @
--
-- And we can test that it works:
--
-- >>> :t populationCount' (7 :: BitVector 16)
-- populationCount' (7 :: BitVector 16) :: Index 17
-- >>> populationCount' (7 :: BitVector 16)
-- 3
--
-- Some final remarks:
--
--   * By using 'dtfold' instead of 'fold', we had to restrict our 'BitVector'
--     argument to have bit-width that is a power of 2.
--   * Even though our original /populationCount/ function specified a structure
--     where all adders had the same width. Most VHDL/(System)Verilog synthesis
--     tools will create a more efficient circuit, i.e. one where the adders
--     have an increasing bit-width for every layer, from the
--     VHDL/(System)Verilog produced by the Clash compiler.
--
-- __NB__: The depth, or delay, of the structure produced by
-- \"@'dtfold' m f g xs@\" is O(log_2(@'length' xs@)).
dtfold :: forall p k a . KnownNat k
       => Proxy (p :: TyFun Nat Type -> Type) -- ^ The /motive/
       -> (a -> (p @@ 0)) -- ^ Function to apply to every element
       -> (forall l . SNat l -> (p @@ l) -> (p @@ l) -> (p @@ (l + 1)))
       -- ^ Function to combine results.
       --
       -- __NB__: The @SNat l@ indicates the depth/height of the node in the
       -- tree that is created by applying this function. The leafs of the tree
       -- have depth\/height /0/, and the root of the tree has height /k/.
       -> Vec (2^k) a
       -- ^ Vector to fold over.
       --
       -- __NB__: Must have a length that is a power of 2.
       -> (p @@ k)
dtfold :: Proxy p
-> (a -> p @@ 0)
-> (forall (l :: Nat).
    SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1))
-> Vec (2 ^ k) a
-> p @@ k
dtfold _ f :: a -> p @@ 0
f g :: forall (l :: Nat). SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1)
g = SNat k -> Vec (2 ^ k) a -> p @@ k
forall (n :: Nat). SNat n -> Vec (2 ^ n) a -> p @@ n
go (SNat k
forall (n :: Nat). KnownNat n => SNat n
SNat :: SNat k)
  where
    go :: forall n . SNat n -> Vec (2^n) a -> (p @@ n)
    go :: SNat n -> Vec (2 ^ n) a -> p @@ n
go _  (x :: a
x `Cons` Nil) = a -> p @@ 0
f a
x
    go sn :: SNat n
sn xs :: Vec (2 ^ n) a
xs@(Cons _ (Cons _ _)) =
      let sn' :: SNat (n - 1)
          sn' :: SNat (n - 1)
sn'       = SNat n
SNat ((n - 1) + 1)
sn SNat ((n - 1) + 1) -> SNat 1 -> SNat (n - 1)
forall (a :: Nat) (b :: Nat). SNat (a + b) -> SNat b -> SNat a
`subSNat` SNat 1
d1
          (xsL :: Vec (2 ^ (n - 1)) a
xsL,xsR :: Vec (2 ^ (n - 1)) a
xsR) = SNat (2 ^ (n - 1))
-> Vec ((2 ^ (n - 1)) + (2 ^ (n - 1))) a
-> (Vec (2 ^ (n - 1)) a, Vec (2 ^ (n - 1)) a)
forall (m :: Nat) (n :: Nat) a.
SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAt (SNat (n - 1) -> SNat (2 ^ (n - 1))
forall (a :: Nat). SNat a -> SNat (2 ^ a)
pow2SNat SNat (n - 1)
sn') Vec ((2 ^ (n - 1)) + (2 ^ (n - 1))) a
Vec (2 ^ n) a
xs
      in  SNat (n - 1)
-> (p @@ (n - 1)) -> (p @@ (n - 1)) -> p @@ ((n - 1) + 1)
forall (l :: Nat). SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1)
g SNat (n - 1)
sn' (SNat (n - 1) -> Vec (2 ^ (n - 1)) a -> p @@ (n - 1)
forall (n :: Nat). SNat n -> Vec (2 ^ n) a -> p @@ n
go SNat (n - 1)
sn' Vec (2 ^ (n - 1)) a
xsL) (SNat (n - 1) -> Vec (2 ^ (n - 1)) a -> p @@ (n - 1)
forall (n :: Nat). SNat n -> Vec (2 ^ n) a -> p @@ n
go SNat (n - 1)
sn' Vec (2 ^ (n - 1)) a
xsR)
{-# NOINLINE dtfold #-}

-- | To be used as the motive /p/ for 'dfold', when the /f/ in \"'dfold' @p f@\"
-- is a variation on (':>'), e.g.:
--
-- @
-- map' :: forall n a b . KnownNat n => (a -> b) -> Vec n a -> Vec n b
-- map' f = 'dfold' (Proxy @('VCons' b)) (\_ x xs -> f x :> xs)
-- @
data VCons (a :: Type) (f :: TyFun Nat Type) :: Type
type instance Apply (VCons a) l = Vec l a

-- | Specialised version of 'dfold' that builds a triangular computational
-- structure.
--
-- Example:
--
-- @
-- compareSwap a b = if a > b then (a,b) else (b,a)
-- insert y xs     = let (y',xs') = 'mapAccumL' compareSwap y xs in xs' ':<' y'
-- insertionSort   = 'vfold' (const insert)
-- @
--
-- Builds a triangular structure of compare and swaps to sort a row.
--
-- >>> insertionSort (7 :> 3 :> 9 :> 1 :> Nil)
-- <1,3,7,9>
--
-- The circuit layout of @insertionSort@, build using 'vfold', is:
--
-- <<doc/csSort.svg>>
vfold :: forall k a b . KnownNat k
      => (forall l . SNat l -> a -> Vec l b -> Vec (l + 1) b)
      -> Vec k a
      -> Vec k b
vfold :: (forall (l :: Nat). SNat l -> a -> Vec l b -> Vec (l + 1) b)
-> Vec k a -> Vec k b
vfold f :: forall (l :: Nat). SNat l -> a -> Vec l b -> Vec (l + 1) b
f xs :: Vec k a
xs = Proxy (VCons b)
-> (forall (l :: Nat).
    SNat l -> a -> (VCons b @@ l) -> VCons b @@ (l + 1))
-> (VCons b @@ 0)
-> Vec k a
-> VCons b @@ k
forall (p :: TyFun Nat Type -> Type) (k :: Nat) a.
KnownNat k =>
Proxy p
-> (forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1))
-> (p @@ 0)
-> Vec k a
-> p @@ k
dfold (Proxy (VCons b)
forall k (t :: k). Proxy t
Proxy @(VCons b)) forall (l :: Nat).
SNat l -> a -> (VCons b @@ l) -> VCons b @@ (l + 1)
forall (l :: Nat). SNat l -> a -> Vec l b -> Vec (l + 1) b
f VCons b @@ 0
forall a. Vec 0 a
Nil Vec k a
xs
{-# INLINE vfold #-}

-- | Apply a function to every element of a vector and the element's position
-- (as an 'SNat' value) in the vector.
--
-- >>> let rotateMatrix = smap (flip rotateRightS)
-- >>> let xss = (1:>2:>3:>Nil):>(1:>2:>3:>Nil):>(1:>2:>3:>Nil):>Nil
-- >>> xss
-- <<1,2,3>,<1,2,3>,<1,2,3>>
-- >>> rotateMatrix xss
-- <<1,2,3>,<3,1,2>,<2,3,1>>
smap :: forall k a b . KnownNat k => (forall l . SNat l -> a -> b) -> Vec k a -> Vec k b
smap :: (forall (l :: Nat). SNat l -> a -> b) -> Vec k a -> Vec k b
smap f :: forall (l :: Nat). SNat l -> a -> b
f xs :: Vec k a
xs = Vec k b -> Vec k b
forall (n :: Nat) a. Vec n a -> Vec n a
reverse
          (Vec k b -> Vec k b) -> Vec k b -> Vec k b
forall a b. (a -> b) -> a -> b
$ Proxy (VCons b)
-> (forall (l :: Nat).
    SNat l -> a -> (VCons b @@ l) -> VCons b @@ (l + 1))
-> (VCons b @@ 0)
-> Vec k a
-> VCons b @@ k
forall (p :: TyFun Nat Type -> Type) (k :: Nat) a.
KnownNat k =>
Proxy p
-> (forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1))
-> (p @@ 0)
-> Vec k a
-> p @@ k
dfold (Proxy (VCons b)
forall k (t :: k). Proxy t
Proxy @(VCons b))
                  (\sn :: SNat l
sn x :: a
x xs' :: VCons b @@ l
xs' -> SNat l -> a -> b
forall (l :: Nat). SNat l -> a -> b
f SNat l
sn a
x b -> Vec l b -> Vec (l + 1) b
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> VCons b @@ l
Vec l b
xs')
                  VCons b @@ 0
forall a. Vec 0 a
Nil (Vec k a -> Vec k a
forall (n :: Nat) a. Vec n a -> Vec n a
reverse Vec k a
xs)
{-# INLINE smap #-}

instance (KnownNat n, BitPack a) => BitPack (Vec n a) where
  type BitSize (Vec n a) = n * (BitSize a)
  pack :: Vec n a -> BitVector (BitSize (Vec n a))
pack   = (Vec n a -> BitVector (n * BitSize a))
-> Vec n a -> BitVector (n * BitSize a)
forall (n :: Nat) a.
KnownNat n =>
(a -> BitVector n) -> a -> BitVector n
packXWith (Vec n (BitVector (BitSize a)) -> BitVector (n * BitSize a)
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Vec n (BitVector m) -> BitVector (n * m)
concatBitVector# (Vec n (BitVector (BitSize a)) -> BitVector (n * BitSize a))
-> (Vec n a -> Vec n (BitVector (BitSize a)))
-> Vec n a
-> BitVector (n * BitSize a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> BitVector (BitSize a))
-> Vec n a -> Vec n (BitVector (BitSize a))
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map a -> BitVector (BitSize a)
forall a. BitPack a => a -> BitVector (BitSize a)
pack)
  unpack :: BitVector (BitSize (Vec n a)) -> Vec n a
unpack = (BitVector (BitSize a) -> a)
-> Vec n (BitVector (BitSize a)) -> Vec n a
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map BitVector (BitSize a) -> a
forall a. BitPack a => BitVector (BitSize a) -> a
unpack (Vec n (BitVector (BitSize a)) -> Vec n a)
-> (BitVector (n * BitSize a) -> Vec n (BitVector (BitSize a)))
-> BitVector (n * BitSize a)
-> Vec n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector (n * BitSize a) -> Vec n (BitVector (BitSize a))
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
BitVector (n * m) -> Vec n (BitVector m)
unconcatBitVector#

concatBitVector#
  :: (KnownNat n, KnownNat m)
  => Vec n (BitVector m)
  -> BitVector (n * m)
concatBitVector# :: Vec n (BitVector m) -> BitVector (n * m)
concatBitVector# Nil           = 0
concatBitVector# (x :: BitVector m
x `Cons` xs :: Vec n (BitVector m)
xs) = BitVector m
x BitVector m -> BitVector (n * m) -> BitVector (m + (n * m))
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# Vec n (BitVector m) -> BitVector (n * m)
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Vec n (BitVector m) -> BitVector (n * m)
concatBitVector# Vec n (BitVector m)
xs
{-# NOINLINE concatBitVector# #-}

unconcatBitVector#
  :: forall n m
   . (KnownNat n, KnownNat m)
  => BitVector (n * m)
  -> Vec n (BitVector m)
unconcatBitVector# :: BitVector (n * m) -> Vec n (BitVector m)
unconcatBitVector# = UNat n -> BitVector (n * m) -> Vec n (BitVector m)
forall (x :: Nat).
KnownNat x =>
UNat x -> BitVector (x * m) -> Vec x (BitVector m)
go (SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat @ n))
  where
    go :: KnownNat x => UNat x -> BitVector (x * m) -> Vec x (BitVector m)
    go :: UNat x -> BitVector (x * m) -> Vec x (BitVector m)
go UZero     _  = Vec x (BitVector m)
forall a. Vec 0 a
Nil
    go (USucc n :: UNat n
n) bv :: BitVector (x * m)
bv = let (BitVector m
x :: BitVector m,bv' :: BitVector (n * m)
bv') = BitVector (m + (n * m)) -> (BitVector m, BitVector (n * m))
forall (n :: Nat) (m :: Nat).
KnownNat n =>
BitVector (m + n) -> (BitVector m, BitVector n)
split# BitVector (m + (n * m))
BitVector (x * m)
bv
                      in  BitVector m
x BitVector m -> Vec n (BitVector m) -> Vec (n + 1) (BitVector m)
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> UNat n -> BitVector (n * m) -> Vec n (BitVector m)
forall (x :: Nat).
KnownNat x =>
UNat x -> BitVector (x * m) -> Vec x (BitVector m)
go UNat n
n BitVector (n * m)
bv'
{-# NOINLINE unconcatBitVector# #-}

-- | Convert a 'BitVector' to a 'Vec' of 'Bit's.
--
-- >>> let x = 6 :: BitVector 8
-- >>> x
-- 0000_0110
-- >>> bv2v x
-- <0,0,0,0,0,1,1,0>
bv2v :: KnownNat n => BitVector n -> Vec n Bit
bv2v :: BitVector n -> Vec n Bit
bv2v = BitVector n -> Vec n Bit
forall a. BitPack a => BitVector (BitSize a) -> a
unpack

-- | Convert a 'Vec' of 'Bit's to a 'BitVector'.
--
-- >>> let x = (0:>0:>0:>1:>0:>0:>1:>0:>Nil) :: Vec 8 Bit
-- >>> x
-- <0,0,0,1,0,0,1,0>
-- >>> v2bv x
-- 0001_0010
v2bv :: KnownNat n => Vec n Bit -> BitVector n
v2bv :: Vec n Bit -> BitVector n
v2bv = Vec n Bit -> BitVector n
forall a. BitPack a => a -> BitVector (BitSize a)
pack

-- | Evaluate all elements of a vector to WHNF, returning the second argument
seqV
  :: KnownNat n
  => Vec n a
  -> b
  -> b
seqV :: Vec n a -> b -> b
seqV v :: Vec n a
v b :: b
b =
  let s :: () -> a -> ()
s () e :: a
e = a -> () -> ()
forall a b. a -> b -> b
seq a
e () in
  (() -> a -> ()) -> () -> Vec n a -> ()
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl () -> a -> ()
forall a. () -> a -> ()
s () Vec n a
v () -> b -> b
forall a b. a -> b -> b
`seq` b
b
{-# NOINLINE seqV #-}
infixr 0 `seqV`

-- | Evaluate all elements of a vector to WHNF
forceV
  :: KnownNat n
  => Vec n a
  -> Vec n a
forceV :: Vec n a -> Vec n a
forceV v :: Vec n a
v =
  Vec n a
v Vec n a -> Vec n a -> Vec n a
forall (n :: Nat) a b. KnownNat n => Vec n a -> b -> b
`seqV` Vec n a
v
{-# INLINE forceV #-}

-- | Evaluate all elements of a vector to WHNF, returning the second argument.
-- Does not propagate 'XException's.
seqVX
  :: KnownNat n
  => Vec n a
  -> b
  -> b
seqVX :: Vec n a -> b -> b
seqVX v :: Vec n a
v b :: b
b =
  let s :: () -> a -> ()
s () e :: a
e = a -> () -> ()
forall a b. a -> b -> b
seqX a
e () in
  (() -> a -> ()) -> () -> Vec n a -> ()
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl () -> a -> ()
forall a. () -> a -> ()
s () Vec n a
v () -> b -> b
forall a b. a -> b -> b
`seqX` b
b
{-# NOINLINE seqVX #-}
infixr 0 `seqVX`

-- | Evaluate all elements of a vector to WHNF. Does not propagate 'XException's.
forceVX
  :: KnownNat n
  => Vec n a
  -> Vec n a
forceVX :: Vec n a -> Vec n a
forceVX v :: Vec n a
v =
  Vec n a
v Vec n a -> Vec n a -> Vec n a
forall (n :: Nat) a b. KnownNat n => Vec n a -> b -> b
`seqVX` Vec n a
v
{-# INLINE forceVX #-}

instance Lift a => Lift (Vec n a) where
  lift :: Vec n a -> ExpQ
lift Nil           = [| Nil |]
  lift (x :: a
x `Cons` xs :: Vec n a
xs) = [| x `Cons` $(lift xs) |]

instance (KnownNat n, Arbitrary a) => Arbitrary (Vec n a) where
  arbitrary :: Gen (Vec n a)
arbitrary = (Gen a -> Gen a) -> Vec n (Gen a) -> Gen (Vec n a)
forall a (f :: Type -> Type) b (n :: Nat).
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse# Gen a -> Gen a
forall a. a -> a
id (Vec n (Gen a) -> Gen (Vec n a)) -> Vec n (Gen a) -> Gen (Vec n a)
forall a b. (a -> b) -> a -> b
$ Gen a -> Vec n (Gen a)
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat Gen a
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: Vec n a -> [Vec n a]
shrink    = ([a] -> [a]) -> Vec n [a] -> [Vec n a]
forall a (f :: Type -> Type) b (n :: Nat).
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse# [a] -> [a]
forall a. a -> a
id (Vec n [a] -> [Vec n a])
-> (Vec n a -> Vec n [a]) -> Vec n a -> [Vec n a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> [a]) -> Vec n a -> Vec n [a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> [a]
forall a. Arbitrary a => a -> [a]
shrink

instance CoArbitrary a => CoArbitrary (Vec n a) where
  coarbitrary :: Vec n a -> Gen b -> Gen b
coarbitrary = [a] -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary ([a] -> Gen b -> Gen b)
-> (Vec n a -> [a]) -> Vec n a -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec n a -> [a]
forall (n :: Nat) a. Vec n a -> [a]
toList

type instance Lens.Index   (Vec n a) = Index n
type instance Lens.IxValue (Vec n a) = a
instance KnownNat n => Lens.Ixed (Vec n a) where
  ix :: Index (Vec n a) -> Traversal' (Vec n a) (IxValue (Vec n a))
ix i :: Index (Vec n a)
i f :: IxValue (Vec n a) -> f (IxValue (Vec n a))
f xs :: Vec n a
xs = Vec n a -> Int -> a -> Vec n a
forall (n :: Nat) a. KnownNat n => Vec n a -> Int -> a -> Vec n a
replace_int Vec n a
xs (Index n -> Int
forall a. Enum a => a -> Int
fromEnum Index (Vec n a)
Index n
i) (a -> Vec n a) -> f a -> f (Vec n a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IxValue (Vec n a) -> f (IxValue (Vec n a))
f (Vec n a -> Int -> a
forall (n :: Nat) a. KnownNat n => Vec n a -> Int -> a
index_int Vec n a
xs (Index n -> Int
forall a. Enum a => a -> Int
fromEnum Index (Vec n a)
Index n
i))