{-# Language GADTs, DataKinds, TypeOperators, BangPatterns #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# Language PatternGuards #-}
{-# Language PolyKinds #-}
{-# Language TypeApplications, ScopedTypeVariables #-}
{-# Language TupleSections #-}
{-# Language Rank2Types, RoleAnnotations #-}
{-# Language CPP #-}
#if __GLASGOW_HASKELL__ >= 805
{-# Language NoStarIsType #-}
#endif
{-|
Copyright        : (c) Galois, Inc 2014-2019

A fixed-size vector of typed elements.

NB: This module contains an orphan instance. It will be included in GHC 8.10,
see https://gitlab.haskell.org/ghc/ghc/merge_requests/273.
-}
module Data.Parameterized.Vector
  ( Vector
    -- * Lists
  , fromList
  , toList

    -- * Assignments
  , fromAssignment
  , toAssignment

    -- * Length
  , length
  , nonEmpty
  , lengthInt

    -- * Indexing
  , elemAt
  , elemAtMaybe
  , elemAtUnsafe

    -- * Indexing with Fin
  , indicesUpTo
  , indicesOf

    -- * Update
  , insertAt
  , insertAtMaybe

    -- * Sub sequences
  , uncons
  , unsnoc
  , slice
  , Data.Parameterized.Vector.take
  , replace
  , mapAt
  , mapAtM

    -- * Zipping
  , zipWith
  , zipWithM
  , zipWithM_
  , interleave

    -- * Reorder
  , shuffle
  , reverse
  , rotateL
  , rotateR
  , shiftL
  , shiftR

    -- * Construction
  , singleton
  , cons
  , snoc
  , generate
  , generateM
  -- ** Unfolding
  , unfoldr
  , unfoldrM
  , unfoldrWithIndex
  , unfoldrWithIndexM
  , iterateN
  , iterateNM

    -- * Splitting and joining
    -- ** General
  , joinWithM
  , joinWith
  , splitWith
  , splitWithA

    -- ** Vectors
  , split
  , join
  , append

  ) where

import qualified Data.Vector as Vector
import Data.Coerce
import Data.Foldable.WithIndex (FoldableWithIndex(ifoldMap))
import Data.Functor.Compose
import Data.Functor.WithIndex (FunctorWithIndex(imap))
import Data.Vector.Mutable (MVector)
import qualified Data.Vector.Mutable as MVector
import Control.Monad.ST
import Data.Functor.Identity
import Data.Parameterized.Fin
import Data.Parameterized.NatRepr
import Data.Parameterized.NatRepr.Internal
import Data.Proxy
import Data.Traversable.WithIndex (TraversableWithIndex(itraverse))
import Prelude hiding (length,reverse,zipWith)
import Numeric.Natural

import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Utils.Endian

-- | Fixed-size non-empty vectors.
data Vector n a where
  Vector :: (1 <= n) => !(Vector.Vector a) -> Vector n a

type role Vector nominal representational

instance Eq a => Eq (Vector n a) where
  (Vector Vector a
x) == :: Vector n a -> Vector n a -> Bool
== (Vector Vector a
y) = Vector a
x forall a. Eq a => a -> a -> Bool
== Vector a
y

instance Show a => Show (Vector n a) where
  show :: Vector n a -> String
show (Vector Vector a
x) = forall a. Show a => a -> String
show Vector a
x

-- | Get the elements of the vector as a list, lowest index first.
toList :: Vector n a -> [a]
toList :: forall (n :: Natural) a. Vector n a -> [a]
toList (Vector Vector a
v) = forall a. Vector a -> [a]
Vector.toList Vector a
v
{-# Inline toList #-}

-- NOTE: We are using the raw 'NatRepr' constructor here, which is unsafe.
-- | Length of the vector.
-- @O(1)@
length :: Vector n a -> NatRepr n
length :: forall (n :: Natural) a. Vector n a -> NatRepr n
length (Vector Vector a
xs) = forall (n :: Natural). Natural -> NatRepr n
NatRepr (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Vector a -> Int
Vector.length Vector a
xs) :: Natural)
{-# INLINE length #-}

-- | The length of the vector as an "Int".
lengthInt :: Vector n a -> Int
lengthInt :: forall (n :: Natural) a. Vector n a -> Int
lengthInt (Vector Vector a
xs) = forall a. Vector a -> Int
Vector.length Vector a
xs
{-# Inline lengthInt #-}

elemAt :: ((i+1) <= n) => NatRepr i -> Vector n a -> a
elemAt :: forall (i :: Natural) (n :: Natural) a.
((i + 1) <= n) =>
NatRepr i -> Vector n a -> a
elemAt NatRepr i
n (Vector Vector a
xs) = Vector a
xs forall a. Vector a -> Int -> a
Vector.! forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr i
n

-- | Get the element at the given index.
-- @O(1)@
elemAtMaybe :: Int -> Vector n a -> Maybe a
elemAtMaybe :: forall (n :: Natural) a. Int -> Vector n a -> Maybe a
elemAtMaybe Int
n (Vector Vector a
xs) = Vector a
xs forall a. Vector a -> Int -> Maybe a
Vector.!? Int
n
{-# INLINE elemAt #-}

-- | Get the element at the given index.
-- Raises an exception if the element is not in the vector's domain.
-- @O(1)@
elemAtUnsafe :: Int -> Vector n a -> a
elemAtUnsafe :: forall (n :: Natural) a. Int -> Vector n a -> a
elemAtUnsafe Int
n (Vector Vector a
xs) = Vector a
xs forall a. Vector a -> Int -> a
Vector.! Int
n
{-# INLINE elemAtUnsafe #-}

--------------------------------------------------------------------------------

indicesUpTo :: NatRepr n -> Vector (n + 1) (Fin (n + 1))
indicesUpTo :: forall (n :: Natural). NatRepr n -> Vector (n + 1) (Fin (n + 1))
indicesUpTo NatRepr n
n =
  forall (n :: Natural) a.
NatRepr n -> (a -> a) -> a -> Vector (n + 1) a
iterateN
    NatRepr n
n
    (forall (n :: Natural) r.
(forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r)
-> Fin n -> r
viewFin
      (\NatRepr i
x ->
        case forall (m :: Natural) (n :: Natural).
(m <= n) =>
NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)
testStrictLeq (forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat NatRepr i
x) (forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat NatRepr n
n) of
          Left LeqProof ((i + 1) + 1) (n + 1)
LeqProof -> forall (i :: Natural) (n :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
mkFin (forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat NatRepr i
x)
          Right (i + 1) :~: (n + 1)
Refl -> forall (i :: Natural) (n :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
mkFin NatRepr n
n))
    (case forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> LeqProof n (m + n)
addPrefixIsLeq NatRepr n
n (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) of
       LeqProof 1 (n + 1)
LeqProof -> forall (i :: Natural) (n :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
mkFin (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0))

indicesOf :: Vector n a -> Vector n (Fin n)
indicesOf :: forall (n :: Natural) a. Vector n a -> Vector n (Fin n)
indicesOf v :: Vector n a
v@(Vector Vector a
_) = -- Pattern match to bring 1 <= n into scope
  case forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel (forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector n a
v) (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) of
    ((n - 1) + 1) :~: n
Refl -> forall (n :: Natural). NatRepr n -> Vector (n + 1) (Fin (n + 1))
indicesUpTo (forall (n :: Natural). (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat (forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector n a
v))

instance FunctorWithIndex (Fin n) (Vector n) where
  imap :: forall a b. (Fin n -> a -> b) -> Vector n a -> Vector n b
imap Fin n -> a -> b
f Vector n a
v = forall a b c (n :: Natural).
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipWith Fin n -> a -> b
f (forall (n :: Natural) a. Vector n a -> Vector n (Fin n)
indicesOf Vector n a
v) Vector n a
v

instance FoldableWithIndex (Fin n) (Vector n) where
  ifoldMap :: forall m a. Monoid m => (Fin n -> a -> m) -> Vector n a -> m
ifoldMap Fin n -> a -> m
f Vector n a
v = forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Fin n -> a -> m
f) (forall i (f :: Type -> Type) a b.
FunctorWithIndex i f =>
(i -> a -> b) -> f a -> f b
imap (,) Vector n a
v)

instance TraversableWithIndex (Fin n) (Vector n) where
  itraverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vector n a -> f (Vector n b)
itraverse Fin n -> a -> f b
f Vector n a
v = forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Fin n -> a -> f b
f) (forall i (f :: Type -> Type) a b.
FunctorWithIndex i f =>
(i -> a -> b) -> f a -> f b
imap (,) Vector n a
v)

--------------------------------------------------------------------------------

-- | Insert an element at the given index.
-- @O(n)@.
insertAt :: ((i + 1) <= n) => NatRepr i -> a -> Vector n a -> Vector n a
insertAt :: forall (i :: Natural) (n :: Natural) a.
((i + 1) <= n) =>
NatRepr i -> a -> Vector n a -> Vector n a
insertAt NatRepr i
n a
a (Vector Vector a
xs) = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall a. Vector a -> [(Int, a)] -> Vector a
Vector.unsafeUpd Vector a
xs [(forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr i
n,a
a)])

-- | Insert an element at the given index.
-- Return 'Nothing' if the element is outside the vector bounds.
-- @O(n)@.
insertAtMaybe :: Int -> a -> Vector n a -> Maybe (Vector n a)
insertAtMaybe :: forall a (n :: Natural).
Int -> a -> Vector n a -> Maybe (Vector n a)
insertAtMaybe Int
n a
a (Vector Vector a
xs)
  | Int
0 forall a. Ord a => a -> a -> Bool
<= Int
n Bool -> Bool -> Bool
&& Int
n forall a. Ord a => a -> a -> Bool
< forall a. Vector a -> Int
Vector.length Vector a
xs = forall a. a -> Maybe a
Just (forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall a. Vector a -> [(Int, a)] -> Vector a
Vector.unsafeUpd Vector a
xs [(Int
n,a
a)]))
  | Bool
otherwise = forall a. Maybe a
Nothing


-- | Proof that the length of this vector is not 0.
nonEmpty :: Vector n a -> LeqProof 1 n
nonEmpty :: forall (n :: Natural) a. Vector n a -> LeqProof 1 n
nonEmpty (Vector Vector a
_) = forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof
{-# Inline nonEmpty #-}


-- | Remove the first element of the vector, and return the rest, if any.
uncons :: forall n a.  Vector n a -> (a, Either (n :~: 1) (Vector (n-1) a))
uncons :: forall (n :: Natural) a.
Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))
uncons v :: Vector n a
v@(Vector Vector a
xs) = (forall a. Vector a -> a
Vector.head Vector a
xs, Either (n :~: 1) (Vector (n - 1) a)
mbTail)
  where
  mbTail :: Either (n :~: 1) (Vector (n - 1) a)
  mbTail :: Either (n :~: 1) (Vector (n - 1) a)
mbTail = case forall (m :: Natural) (n :: Natural).
(m <= n) =>
NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)
testStrictLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) (forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector n a
v) of
             Left LeqProof (1 + 1) n
n2_leq_n ->
               do LeqProof (2 - 1) (n - 1)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
leqSub2 LeqProof (1 + 1) n
n2_leq_n (forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
leqRefl (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1)))
                  forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall a. Vector a -> Vector a
Vector.tail Vector a
xs))
             Right 1 :~: n
Refl    -> forall a b. a -> Either a b
Left forall {k} (a :: k). a :~: a
Refl
{-# Inline uncons #-}

-- | Remove the last element of the vector, and return the rest, if any.
unsnoc :: forall n a.  Vector n a -> (a, Either (n :~: 1) (Vector (n-1) a))
unsnoc :: forall (n :: Natural) a.
Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))
unsnoc v :: Vector n a
v@(Vector Vector a
xs) = (forall a. Vector a -> a
Vector.last Vector a
xs, Either (n :~: 1) (Vector (n - 1) a)
mbTail)
  where
  mbTail :: Either (n :~: 1) (Vector (n - 1) a)
  mbTail :: Either (n :~: 1) (Vector (n - 1) a)
mbTail = case forall (m :: Natural) (n :: Natural).
(m <= n) =>
NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)
testStrictLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) (forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector n a
v) of
             Left LeqProof (1 + 1) n
n2_leq_n ->
               do LeqProof (2 - 1) (n - 1)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
leqSub2 LeqProof (1 + 1) n
n2_leq_n (forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
leqRefl (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1)))
                  forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall a. Int -> Int -> Vector a -> Vector a
Vector.slice Int
0 (forall a. Vector a -> Int
Vector.length Vector a
xs forall a. Num a => a -> a -> a
- Int
1) Vector a
xs))
             Right 1 :~: n
Refl    -> forall a b. a -> Either a b
Left forall {k} (a :: k). a :~: a
Refl
{-# Inline unsnoc #-}


--------------------------------------------------------------------------------

-- | Make a vector of the given length and element type.
-- Returns "Nothing" if the input list does not have the right number of
-- elements.
-- @O(n)@.
fromList :: (1 <= n) => NatRepr n -> [a] -> Maybe (Vector n a)
fromList :: forall (n :: Natural) a.
(1 <= n) =>
NatRepr n -> [a] -> Maybe (Vector n a)
fromList NatRepr n
n [a]
xs
  | forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr n
n forall a. Eq a => a -> a -> Bool
== forall a. Vector a -> Int
Vector.length Vector a
v = forall a. a -> Maybe a
Just (forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector Vector a
v)
  | Bool
otherwise                     = forall a. Maybe a
Nothing
  where
  v :: Vector a
v = forall a. [a] -> Vector a
Vector.fromList [a]
xs
{-# INLINE fromList #-}

-- | Convert a non-empty 'Ctx.Assignment' to a fixed-size 'Vector'.
--
-- This function uses the same ordering convention as 'Ctx.toVector'.
fromAssignment ::
  forall f ctx tp e.
  (forall tp'. f tp' -> e) ->
  Ctx.Assignment f (ctx Ctx.::> tp) ->
  Vector (Ctx.CtxSize (ctx Ctx.::> tp)) e
fromAssignment :: forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k) e.
(forall (tp' :: k). f tp' -> e)
-> Assignment f (ctx ::> tp) -> Vector (CtxSize (ctx ::> tp)) e
fromAssignment forall (tp' :: k). f tp' -> e
f Assignment f (ctx ::> tp)
assign =
  case forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
Ctx.viewAssign Assignment f (ctx ::> tp)
assign of
    Ctx.AssignExtend Assignment f ctx
assign' f tp
_ ->
      case forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
leqRefl (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1)) (forall {k} (items :: Ctx k). Size items -> NatRepr (CtxSize items)
Ctx.sizeToNatRepr (forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment f ctx
assign')) of
        LeqProof 1 (1 + CtxSize ctx)
LeqProof -> forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall {k} (f :: k -> Type) (tps :: Ctx k) e.
Assignment f tps -> (forall (tp :: k). f tp -> e) -> Vector e
Ctx.toVector Assignment f (ctx ::> tp)
assign forall (tp' :: k). f tp' -> e
f)

-- | Convert a 'Vector' into a 'Ctx.Assignment'.
--
-- This function uses the same ordering convention as 'Ctx.toVector'.
toAssignment ::
  Ctx.Size ctx ->
  (forall tp. Ctx.Index ctx tp -> e -> f tp) ->
  Vector (Ctx.CtxSize ctx) e ->
  Ctx.Assignment f ctx
toAssignment :: forall {k} (ctx :: Ctx k) e (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> e -> f tp)
-> Vector (CtxSize ctx) e
-> Assignment f ctx
toAssignment Size ctx
sz forall (tp :: k). Index ctx tp -> e -> f tp
g Vector (CtxSize ctx) e
vec =
  -- The unsafe indexing here relies on the safety of the rest of the Vector
  -- API, specifically the inability to construct vectors that have an
  -- underlying size that differs from the size in their type.
  forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
Ctx.generate Size ctx
sz (\Index ctx tp
idx -> forall (tp :: k). Index ctx tp -> e -> f tp
g Index ctx tp
idx (forall (n :: Natural) a. Int -> Vector n a -> a
elemAtUnsafe (forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal Index ctx tp
idx) Vector (CtxSize ctx) e
vec))

-- | Extract a subvector of the given vector.
slice :: (i + w <= n, 1 <= w) =>
            NatRepr i {- ^ Start index -} ->
            NatRepr w {- ^ Width of sub-vector -} ->
            Vector n a -> Vector w a
slice :: forall (i :: Natural) (w :: Natural) (n :: Natural) a.
((i + w) <= n, 1 <= w) =>
NatRepr i -> NatRepr w -> Vector n a -> Vector w a
slice NatRepr i
i NatRepr w
w (Vector Vector a
xs) = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall a. Int -> Int -> Vector a -> Vector a
Vector.slice (forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr i
i) (forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr w
w) Vector a
xs)
{-# INLINE slice #-}

-- | Take the front (lower-indexes) part of the vector.
take :: forall n x a. (1 <= n) => NatRepr n -> Vector (n + x) a -> Vector n a
take :: forall (n :: Natural) (x :: Natural) a.
(1 <= n) =>
NatRepr n -> Vector (n + x) a -> Vector n a
take | LeqProof n (n + x)
LeqProof <- LeqProof n (n + x)
prf = forall (i :: Natural) (w :: Natural) (n :: Natural) a.
((i + w) <= n, 1 <= w) =>
NatRepr i -> NatRepr w -> Vector n a -> Vector w a
slice (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0)
  where
  prf :: LeqProof n (n + x)
prf = forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
leqRefl (forall {k} (t :: k). Proxy t
Proxy @n)) (forall {k} (t :: k). Proxy t
Proxy @x)

-- | Scope a monadic function to a sub-section of the given vector.
mapAtM :: Monad m => (i + w <= n, 1 <= w) =>
            NatRepr i {- ^ Start index -} ->
            NatRepr w {- ^ Section width -} ->
            (Vector w a -> m (Vector w a)) {-^ map for the sub-vector -} ->
            Vector n a -> m (Vector n a)
mapAtM :: forall (m :: Type -> Type) (i :: Natural) (w :: Natural)
       (n :: Natural) a.
(Monad m, (i + w) <= n, 1 <= w) =>
NatRepr i
-> NatRepr w
-> (Vector w a -> m (Vector w a))
-> Vector n a
-> m (Vector n a)
mapAtM NatRepr i
i NatRepr w
w Vector w a -> m (Vector w a)
f (Vector Vector a
vn) =
  let
    (Vector a
vhead, Vector a
vtail) = forall a. Int -> Vector a -> (Vector a, Vector a)
Vector.splitAt (forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr i
i) Vector a
vn
    (Vector a
vsect, Vector a
vend) = forall a. Int -> Vector a -> (Vector a, Vector a)
Vector.splitAt (forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr w
w) Vector a
vtail
  in do
    Vector Vector a
vsect' <- Vector w a -> m (Vector w a)
f (forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector Vector a
vsect)
    forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector forall a b. (a -> b) -> a -> b
$ Vector a
vhead forall a. Vector a -> Vector a -> Vector a
Vector.++ Vector a
vsect' forall a. Vector a -> Vector a -> Vector a
Vector.++ Vector a
vend

-- | Scope a function to a sub-section of the given vector.
mapAt :: (i + w <= n, 1 <= w) =>
            NatRepr i {- ^ Start index -} ->
            NatRepr w {- ^ Section width -} ->
            (Vector w a -> Vector w a) {-^ map for the sub-vector -} ->
            Vector n a -> Vector n a
mapAt :: forall (i :: Natural) (w :: Natural) (n :: Natural) a.
((i + w) <= n, 1 <= w) =>
NatRepr i
-> NatRepr w
-> (Vector w a -> Vector w a)
-> Vector n a
-> Vector n a
mapAt NatRepr i
i NatRepr w
w Vector w a -> Vector w a
f Vector n a
vn = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) (i :: Natural) (w :: Natural)
       (n :: Natural) a.
(Monad m, (i + w) <= n, 1 <= w) =>
NatRepr i
-> NatRepr w
-> (Vector w a -> m (Vector w a))
-> Vector n a
-> m (Vector n a)
mapAtM NatRepr i
i NatRepr w
w (forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector w a -> Vector w a
f) Vector n a
vn

-- | Replace a sub-section of a vector with the given sub-vector.
replace :: (i + w <= n, 1 <= w) =>
              NatRepr i {- ^ Start index -} ->
              Vector w a {- ^ sub-vector -} ->
              Vector n a -> Vector n a
replace :: forall (i :: Natural) (w :: Natural) (n :: Natural) a.
((i + w) <= n, 1 <= w) =>
NatRepr i -> Vector w a -> Vector n a -> Vector n a
replace NatRepr i
i Vector w a
vw Vector n a
vn = forall (i :: Natural) (w :: Natural) (n :: Natural) a.
((i + w) <= n, 1 <= w) =>
NatRepr i
-> NatRepr w
-> (Vector w a -> Vector w a)
-> Vector n a
-> Vector n a
mapAt NatRepr i
i (forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector w a
vw) (forall a b. a -> b -> a
const Vector w a
vw) Vector n a
vn

--------------------------------------------------------------------------------

instance Functor (Vector n) where
  fmap :: forall a b. (a -> b) -> Vector n a -> Vector n b
fmap a -> b
f (Vector Vector a
xs) = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall a b. (a -> b) -> Vector a -> Vector b
Vector.map a -> b
f Vector a
xs)
  {-# Inline fmap #-}

instance Foldable (Vector n) where
  foldMap :: forall m a. Monoid m => (a -> m) -> Vector n a -> m
foldMap a -> m
f (Vector Vector a
xs) = forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f Vector a
xs

instance Traversable (Vector n) where
  traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector n a -> f (Vector n b)
traverse a -> f b
f (Vector Vector a
xs) = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f Vector a
xs
  {-# Inline traverse #-}

-- | Zip two vectors, potentially changing types.
-- @O(n)@
zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipWith :: forall a b c (n :: Natural).
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipWith a -> b -> c
f (Vector Vector a
xs) (Vector Vector b
ys) = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
Vector.zipWith a -> b -> c
f Vector a
xs Vector b
ys)
{-# Inline zipWith #-}

zipWithM :: Monad m => (a -> b -> m c) ->
                       Vector n a -> Vector n b -> m (Vector n c)
zipWithM :: forall (m :: Type -> Type) a b c (n :: Natural).
Monad m =>
(a -> b -> m c) -> Vector n a -> Vector n b -> m (Vector n c)
zipWithM a -> b -> m c
f (Vector Vector a
xs) (Vector Vector b
ys) = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> m c) -> Vector a -> Vector b -> m (Vector c)
Vector.zipWithM a -> b -> m c
f Vector a
xs Vector b
ys
{-# Inline zipWithM #-}

zipWithM_ :: Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m ()
zipWithM_ :: forall (m :: Type -> Type) a b (n :: Natural).
Monad m =>
(a -> b -> m ()) -> Vector n a -> Vector n b -> m ()
zipWithM_ a -> b -> m ()
f (Vector Vector a
xs) (Vector Vector b
ys) = forall (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> m c) -> Vector a -> Vector b -> m ()
Vector.zipWithM_ a -> b -> m ()
f Vector a
xs Vector b
ys
{-# Inline zipWithM_ #-}

{- | Interleave two vectors.  The elements of the first vector are
at even indexes in the result, the elements of the second are at odd indexes. -}
interleave ::
  forall n a. (1 <= n) => Vector n a -> Vector n a -> Vector (2 * n) a
interleave :: forall (n :: Natural) a.
(1 <= n) =>
Vector n a -> Vector n a -> Vector (2 * n) a
interleave (Vector Vector a
xs) (Vector Vector a
ys)
  | LeqProof 1 (2 * n)
LeqProof <- forall (p :: Natural -> Type) (q :: Natural -> Type) (x :: Natural)
       (y :: Natural).
(1 <= x, 1 <= y) =>
p x -> q y -> LeqProof 1 (x * y)
leqMulPos (forall {k} (t :: k). Proxy t
Proxy @2) (forall {k} (t :: k). Proxy t
Proxy @n) = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector Vector a
zs
  where
  len :: Int
len = forall a. Vector a -> Int
Vector.length Vector a
xs forall a. Num a => a -> a -> a
+ forall a. Vector a -> Int
Vector.length Vector a
ys
  zs :: Vector a
zs  = forall a. Int -> (Int -> a) -> Vector a
Vector.generate Int
len (\Int
i -> let v :: Vector a
v = if forall a. Integral a => a -> Bool
even Int
i then Vector a
xs else Vector a
ys
                                   in Vector a
v forall a. Vector a -> Int -> a
Vector.! (Int
i forall a. Integral a => a -> a -> a
`div` Int
2))

--------------------------------------------------------------------------------

{- | Move the elements around, as specified by the given function.
  * Note: the reindexing function says where each of the elements
          in the new vector come from.
  * Note: it is OK for the same input element to end up in mulitple places
          in the result.
@O(n)@
-}
shuffle :: (Int -> Int) -> Vector n a -> Vector n a
shuffle :: forall (n :: Natural) a. (Int -> Int) -> Vector n a -> Vector n a
shuffle Int -> Int
f (Vector Vector a
xs) = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector Vector a
ys
  where
  ys :: Vector a
ys = forall a. Int -> (Int -> a) -> Vector a
Vector.generate (forall a. Vector a -> Int
Vector.length Vector a
xs) (\Int
i -> Vector a
xs forall a. Vector a -> Int -> a
Vector.! Int -> Int
f Int
i)
{-# Inline shuffle #-}

-- | Reverse the vector.
reverse :: forall a n. (1 <= n) => Vector n a -> Vector n a
reverse :: forall a (n :: Natural). (1 <= n) => Vector n a -> Vector n a
reverse Vector n a
x = forall (n :: Natural) a. (Int -> Int) -> Vector n a -> Vector n a
shuffle (\Int
i -> forall (n :: Natural) a. Vector n a -> Int
lengthInt Vector n a
x forall a. Num a => a -> a -> a
- Int
i forall a. Num a => a -> a -> a
- Int
1) Vector n a
x

-- | Rotate "left".  The first element of the vector is on the "left", so
-- rotate left moves all elemnts toward the corresponding smaller index.
-- Elements that fall off the beginning end up at the end.
rotateL :: Int -> Vector n a -> Vector n a
rotateL :: forall (n :: Natural) a. Int -> Vector n a -> Vector n a
rotateL !Int
n Vector n a
xs = forall (n :: Natural) a. (Int -> Int) -> Vector n a -> Vector n a
shuffle Int -> Int
rotL Vector n a
xs
  where
  !len :: Int
len   = forall (n :: Natural) a. Vector n a -> Int
lengthInt Vector n a
xs
  rotL :: Int -> Int
rotL Int
i = (Int
i forall a. Num a => a -> a -> a
+ Int
n) forall a. Integral a => a -> a -> a
`mod` Int
len          -- `len` is known to be >= 1
{-# Inline rotateL #-}

-- | Rotate "right".  The first element of the vector is on the "left", so
-- rotate right moves all elemnts toward the corresponding larger index.
-- Elements that fall off the end, end up at the beginning.
rotateR :: Int -> Vector n a -> Vector n a
rotateR :: forall (n :: Natural) a. Int -> Vector n a -> Vector n a
rotateR !Int
n Vector n a
xs = forall (n :: Natural) a. (Int -> Int) -> Vector n a -> Vector n a
shuffle Int -> Int
rotR Vector n a
xs
  where
  !len :: Int
len   = forall (n :: Natural) a. Vector n a -> Int
lengthInt Vector n a
xs
  rotR :: Int -> Int
rotR Int
i = (Int
i forall a. Num a => a -> a -> a
- Int
n) forall a. Integral a => a -> a -> a
`mod` Int
len        -- `len` is known to be >= 1
{-# Inline rotateR #-}

{- | Move all elements towards smaller indexes.
Elements that fall off the front are ignored.
Empty slots are filled in with the given element.
@O(n)@. -}
shiftL :: Int -> a -> Vector n a -> Vector n a
shiftL :: forall a (n :: Natural). Int -> a -> Vector n a -> Vector n a
shiftL !Int
x a
a (Vector Vector a
xs) = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector Vector a
ys
  where
  !len :: Int
len = forall a. Vector a -> Int
Vector.length Vector a
xs
  ys :: Vector a
ys   = forall a. Int -> (Int -> a) -> Vector a
Vector.generate Int
len (\Int
i -> let j :: Int
j = Int
i forall a. Num a => a -> a -> a
+ Int
x
                                    in if Int
j forall a. Ord a => a -> a -> Bool
>= Int
len then a
a else Vector a
xs forall a. Vector a -> Int -> a
Vector.! Int
j)
{-# Inline shiftL #-}

{- | Move all elements towards the larger indexes.
Elements that "fall" off the end are ignored.
Empty slots are filled in with the given element.
@O(n)@. -}
shiftR :: Int -> a -> Vector n a -> Vector n a
shiftR :: forall a (n :: Natural). Int -> a -> Vector n a -> Vector n a
shiftR !Int
x a
a (Vector Vector a
xs) = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector Vector a
ys
  where
  !len :: Int
len = forall a. Vector a -> Int
Vector.length Vector a
xs
  ys :: Vector a
ys   = forall a. Int -> (Int -> a) -> Vector a
Vector.generate Int
len (\Int
i -> let j :: Int
j = Int
i forall a. Num a => a -> a -> a
- Int
x
                                    in if Int
j forall a. Ord a => a -> a -> Bool
< Int
0 then a
a else Vector a
xs forall a. Vector a -> Int -> a
Vector.! Int
j)
{-# Inline shiftR #-}

-------------------------------------------------------------------------------i

-- | Append two vectors. The first one is at lower indexes in the result.
append :: Vector m a -> Vector n a -> Vector (m + n) a
append :: forall (m :: Natural) a (n :: Natural).
Vector m a -> Vector n a -> Vector (m + n) a
append v1 :: Vector m a
v1@(Vector Vector a
xs) v2 :: Vector n a
v2@(Vector Vector a
ys) =
  case forall (m :: Natural) (n :: Natural) (p :: Natural -> Type)
       (q :: Natural -> Type).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos (forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector m a
v1) (forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector n a
v2) of { LeqProof 1 (m + n)
LeqProof ->
    forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (Vector a
xs forall a. Vector a -> Vector a -> Vector a
Vector.++ Vector a
ys)
  }
{-# Inline append #-}

--------------------------------------------------------------------------------
-- Constructing Vectors

-- | Vector with exactly one element
singleton :: forall a. a -> Vector 1 a
singleton :: forall a. a -> Vector 1 a
singleton a
a = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall a. a -> Vector a
Vector.singleton a
a)

leqLen :: forall n a. Vector n a -> LeqProof 1 (n + 1)
leqLen :: forall (n :: Natural) a. Vector n a -> LeqProof 1 (n + 1)
leqLen Vector n a
v = forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (forall (n :: Natural) a. Vector n a -> LeqProof 1 n
nonEmpty Vector n a
v :: LeqProof 1 n) (forall (f :: Natural -> Type) (z :: Natural).
f z -> LeqProof z (z + 1)
leqSucc (forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector n a
v))

-- | Add an element to the head of a vector
cons :: forall n a. a -> Vector n a -> Vector (n+1) a
cons :: forall (n :: Natural) a. a -> Vector n a -> Vector (n + 1) a
cons a
a v :: Vector n a
v@(Vector Vector a
x) = case forall (n :: Natural) a. Vector n a -> LeqProof 1 (n + 1)
leqLen Vector n a
v of LeqProof 1 (n + 1)
LeqProof -> (forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall a. a -> Vector a -> Vector a
Vector.cons a
a Vector a
x))

-- | Add an element to the tail of a vector
snoc :: forall n a. Vector n a -> a -> Vector (n+1) a
snoc :: forall (n :: Natural) a. Vector n a -> a -> Vector (n + 1) a
snoc v :: Vector n a
v@(Vector Vector a
x) a
a = case forall (n :: Natural) a. Vector n a -> LeqProof 1 (n + 1)
leqLen Vector n a
v of LeqProof 1 (n + 1)
LeqProof -> (forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall a. Vector a -> a -> Vector a
Vector.snoc Vector a
x a
a))

-- | This newtype wraps Vector so that we can curry it in the call to
-- @natRecBounded@. It adds 1 to the length so that the base case is
-- a @Vector@ of non-zero length.
newtype Vector' a n = MkVector' (Vector (n+1) a)

unVector' :: Vector' a n -> Vector (n+1) a
unVector' :: forall a (n :: Natural). Vector' a n -> Vector (n + 1) a
unVector' (MkVector' Vector (n + 1) a
v) = Vector (n + 1) a
v

generate' :: forall h a
           . NatRepr h
          -> (forall n. (n <= h) => NatRepr n -> a)
          -> Vector' a h
generate' :: forall (h :: Natural) a.
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> a)
-> Vector' a h
generate' NatRepr h
h forall (n :: Natural). (n <= h) => NatRepr n -> a
gen =
  forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) (h :: Natural) a b.
Monad m =>
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> b -> m (a, b))
-> b
-> m (Vector' a h)
unfoldrWithIndexM' NatRepr h
h (\NatRepr n
n ()
_last -> forall a. a -> Identity a
Identity (forall (n :: Natural). (n <= h) => NatRepr n -> a
gen NatRepr n
n, ())) ()

-- | Apply a function to each element in a range starting at zero;
-- return the a vector of values obtained.
-- cf. both @natFromZero@ and @Data.Vector.generate@
generate :: forall h a
          . NatRepr h
         -> (forall n. (n <= h) => NatRepr n -> a)
         -> Vector (h + 1) a
generate :: forall (h :: Natural) a.
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> a)
-> Vector (h + 1) a
generate NatRepr h
h forall (n :: Natural). (n <= h) => NatRepr n -> a
gen = forall a (n :: Natural). Vector' a n -> Vector (n + 1) a
unVector' (forall (h :: Natural) a.
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> a)
-> Vector' a h
generate' NatRepr h
h forall (n :: Natural). (n <= h) => NatRepr n -> a
gen)

-- | Since @Vector@ is traversable, we can pretty trivially sequence
-- @natFromZeroVec@ inside a monad.
generateM :: forall m h a. (Monad m)
          => NatRepr h
          -> (forall n. (n <= h) => NatRepr n -> m a)
          -> m (Vector (h + 1) a)
generateM :: forall (m :: Type -> Type) (h :: Natural) a.
Monad m =>
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> m a)
-> m (Vector (h + 1) a)
generateM NatRepr h
h forall (n :: Natural). (n <= h) => NatRepr n -> m a
gen = forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ forall (h :: Natural) a.
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> a)
-> Vector (h + 1) a
generate NatRepr h
h forall (n :: Natural). (n <= h) => NatRepr n -> m a
gen

newtype Compose3 m f g a = Compose3 { forall {k} {k} {k} (m :: k -> Type) (f :: k -> k) (g :: k -> k)
       (a :: k).
Compose3 m f g a -> m (f (g a))
getCompose3 :: m (f (g a)) }

unfoldrWithIndexM' :: forall m h a b. (Monad m)
                  => NatRepr h
                  -> (forall n. (n <= h) => NatRepr n -> b -> m (a, b))
                  -> b
                  -> m (Vector' a h)
unfoldrWithIndexM' :: forall (m :: Type -> Type) (h :: Natural) a b.
Monad m =>
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> b -> m (a, b))
-> b
-> m (Vector' a h)
unfoldrWithIndexM' NatRepr h
h forall (n :: Natural). (n <= h) => NatRepr n -> b -> m (a, b)
gen b
start =
  case forall (n :: Natural). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr h
h of
    Left h :~: 0
Refl -> forall a b. (a, b) -> b
snd forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} {k} {k} (m :: k -> Type) (f :: k -> k) (g :: k -> k)
       (a :: k).
Compose3 m f g a -> m (f (g a))
getCompose3 Compose3 m ((,) b) (Vector' a) 0
base
    Right LeqProof 1 h
LeqProof ->
      case (forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr h
h (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) :: h - 1 + 1 :~: h) of { ((h - 1) + 1) :~: h
Refl ->
        forall a b. (a, b) -> b
snd forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} {k} {k} (m :: k -> Type) (f :: k -> k) (g :: k -> k)
       (a :: k).
Compose3 m f g a -> m (f (g a))
getCompose3 (forall (m :: Natural) (h :: Natural) (f :: Natural -> Type).
(m <= h) =>
NatRepr m
-> NatRepr h
-> f 0
-> (forall (n :: Natural).
    (n <= h) =>
    NatRepr n -> f n -> f (n + 1))
-> f (m + 1)
natRecBounded (forall (n :: Natural). (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat NatRepr h
h) (forall (n :: Natural). (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat NatRepr h
h) Compose3 m ((,) b) (Vector' a) 0
base forall (p :: Natural).
(1 <= h, p <= (h - 1)) =>
NatRepr p
-> Compose3 m ((,) b) (Vector' a) p
-> Compose3 m ((,) b) (Vector' a) (p + 1)
step)
      }
  where base :: Compose3 m ((,) b) (Vector' a) 0
        base :: Compose3 m ((,) b) (Vector' a) 0
base =
          case forall (n :: Natural). LeqProof 0 n
leqZero @h of { LeqProof 0 h
LeqProof ->
          forall {k} {k} {k} (m :: k -> Type) (f :: k -> k) (g :: k -> k)
       (a :: k).
m (f (g a)) -> Compose3 m f g a
Compose3 forall a b. (a -> b) -> a -> b
$ (\(a
hd, b
b) -> (b
b, forall a (n :: Natural). Vector (n + 1) a -> Vector' a n
MkVector' (forall a. a -> Vector 1 a
singleton a
hd))) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (n :: Natural). (n <= h) => NatRepr n -> b -> m (a, b)
gen (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0) b
start
          }
        step :: forall p. (1 <= h, p <= h - 1)
             => NatRepr p
             -> Compose3 m ((,) b) (Vector' a) p
             -> Compose3 m ((,) b) (Vector' a) (p + 1)
        step :: forall (p :: Natural).
(1 <= h, p <= (h - 1)) =>
NatRepr p
-> Compose3 m ((,) b) (Vector' a) p
-> Compose3 m ((,) b) (Vector' a) (p + 1)
step NatRepr p
p (Compose3 m (b, Vector' a p)
mv) =
          case forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr h
h (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) :: h - 1 + 1 :~: h of { ((h - 1) + 1) :~: h
Refl ->
          case (forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof p (h-1))
                        (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 1) :: LeqProof (p+1) h) of { LeqProof (p + 1) h
LeqProof ->
            forall {k} {k} {k} (m :: k -> Type) (f :: k -> k) (g :: k -> k)
       (a :: k).
m (f (g a)) -> Compose3 m f g a
Compose3 forall a b. (a -> b) -> a -> b
$
              do (b
seed, MkVector' Vector (p + 1) a
v) <- m (b, Vector' a p)
mv
                 (a
next, b
nextSeed) <- forall (n :: Natural). (n <= h) => NatRepr n -> b -> m (a, b)
gen (forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat NatRepr p
p) b
seed
                 forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (b
nextSeed, forall a (n :: Natural). Vector (n + 1) a -> Vector' a n
MkVector' forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) a. Vector n a -> a -> Vector (n + 1) a
snoc Vector (p + 1) a
v a
next)
          }}

-- | Monadically unfold a vector, with access to the current index.
--
-- c.f. @Data.Vector.unfoldrExactNM@
unfoldrWithIndexM :: forall m h a b. (Monad m)
                 => NatRepr h
                 -> (forall n. (n <= h) => NatRepr n -> b -> m (a, b))
                 -> b
                 -> m (Vector (h + 1) a)
unfoldrWithIndexM :: forall (m :: Type -> Type) (h :: Natural) a b.
Monad m =>
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> b -> m (a, b))
-> b
-> m (Vector (h + 1) a)
unfoldrWithIndexM NatRepr h
h forall (n :: Natural). (n <= h) => NatRepr n -> b -> m (a, b)
gen b
start = forall a (n :: Natural). Vector' a n -> Vector (n + 1) a
unVector' forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type) (h :: Natural) a b.
Monad m =>
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> b -> m (a, b))
-> b
-> m (Vector' a h)
unfoldrWithIndexM' NatRepr h
h forall (n :: Natural). (n <= h) => NatRepr n -> b -> m (a, b)
gen b
start

-- | Unfold a vector, with access to the current index.
--
-- c.f. @Data.Vector.unfoldrExactN@
unfoldrWithIndex :: forall h a b
                . NatRepr h
                -> (forall n. (n <= h) => NatRepr n -> b -> (a, b))
                -> b
                -> Vector (h + 1) a
unfoldrWithIndex :: forall (h :: Natural) a b.
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> b -> (a, b))
-> b
-> Vector (h + 1) a
unfoldrWithIndex NatRepr h
h forall (n :: Natural). (n <= h) => NatRepr n -> b -> (a, b)
gen b
start =
  forall a (n :: Natural). Vector' a n -> Vector (n + 1) a
unVector' forall a b. (a -> b) -> a -> b
$ forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) (h :: Natural) a b.
Monad m =>
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> b -> m (a, b))
-> b
-> m (Vector' a h)
unfoldrWithIndexM' NatRepr h
h (\NatRepr n
n b
v -> forall a. a -> Identity a
Identity (forall (n :: Natural). (n <= h) => NatRepr n -> b -> (a, b)
gen NatRepr n
n b
v)) b
start

-- | Monadically construct a vector with exactly @h + 1@ elements by repeatedly
-- applying a generator function to a seed value.
--
-- c.f. @Data.Vector.unfoldrExactNM@
unfoldrM :: forall m h a b. (Monad m)
        => NatRepr h
        -> (b -> m (a, b))
        -> b
        -> m (Vector (h + 1) a)
unfoldrM :: forall (m :: Type -> Type) (h :: Natural) a b.
Monad m =>
NatRepr h -> (b -> m (a, b)) -> b -> m (Vector (h + 1) a)
unfoldrM NatRepr h
h b -> m (a, b)
gen b
start = forall (m :: Type -> Type) (h :: Natural) a b.
Monad m =>
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> b -> m (a, b))
-> b
-> m (Vector (h + 1) a)
unfoldrWithIndexM NatRepr h
h (\NatRepr n
_ b
v -> b -> m (a, b)
gen b
v) b
start

-- | Construct a vector with exactly @h + 1@ elements by repeatedly applying a
-- generator function to a seed value.
--
-- c.f. @Data.Vector.unfoldrExactN@
unfoldr :: forall h a b
        . NatRepr h
       -> (b -> (a, b))
       -> b
       -> Vector (h + 1) a
unfoldr :: forall (h :: Natural) a b.
NatRepr h -> (b -> (a, b)) -> b -> Vector (h + 1) a
unfoldr NatRepr h
h b -> (a, b)
gen b
start = forall (h :: Natural) a b.
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> b -> (a, b))
-> b
-> Vector (h + 1) a
unfoldrWithIndex NatRepr h
h (\NatRepr n
_ b
v -> b -> (a, b)
gen b
v) b
start

-- | Build a vector by repeatedly applying a monadic function to a seed value.
--
-- Compare to 'Vector.iterateNM'.
iterateNM :: Monad m => NatRepr n -> (a -> m a) -> a -> m (Vector (n + 1) a)
iterateNM :: forall (m :: Type -> Type) (n :: Natural) a.
Monad m =>
NatRepr n -> (a -> m a) -> a -> m (Vector (n + 1) a)
iterateNM NatRepr n
h a -> m a
f a
start =
  case forall (n :: Natural). NatRepr n -> IsZeroNat n
isZeroNat NatRepr n
h of
    IsZeroNat n
ZeroNat -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall a. a -> Vector 1 a
singleton a
start)
    IsZeroNat n
NonZeroNat -> forall (n :: Natural) a. a -> Vector n a -> Vector (n + 1) a
cons a
start forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type) (h :: Natural) a b.
Monad m =>
NatRepr h -> (b -> m (a, b)) -> b -> m (Vector (h + 1) a)
unfoldrM (forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
predNat NatRepr n
h) (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {b}. b -> (b, b)
dup forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m a
f) a
start
  where dup :: b -> (b, b)
dup b
x = (b
x, b
x)

-- | Build a vector by repeatedly applying a function to a seed value.
--
-- Compare to 'Vector.iterateN'
iterateN :: NatRepr n -> (a -> a) -> a -> Vector (n + 1) a
iterateN :: forall (n :: Natural) a.
NatRepr n -> (a -> a) -> a -> Vector (n + 1) a
iterateN NatRepr n
h a -> a
f a
start = forall a. Identity a -> a
runIdentity (forall (m :: Type -> Type) (n :: Natural) a.
Monad m =>
NatRepr n -> (a -> m a) -> a -> m (Vector (n + 1) a)
iterateNM NatRepr n
h (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
f) a
start)

--------------------------------------------------------------------------------

coerceVec :: Coercible a b => Vector n a -> Vector n b
coerceVec :: forall a b (n :: Natural).
Coercible a b =>
Vector n a -> Vector n b
coerceVec = coerce :: forall a b. Coercible a b => a -> b
coerce

-- | Monadically join a vector of values, using the given function.
-- This functionality can sometimes be reproduced by creating a newtype
-- wrapper and using @joinWith@, this implementation is provided for
-- convenience.
joinWithM ::
  forall m f n w.
  (1 <= w, Monad m) =>
  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> m (f (w + l)))
  {- ^ A function for joining contained elements.  The first argument is
       the size of the accumulated third term, and the second argument
       is the element to join to the accumulated term.  The function
       can use any join strategy desired (prepending/"BigEndian",
       appending/"LittleEndian", etc.). -}
  -> NatRepr w
  -> Vector n (f w)
  -> m (f (n * w))

joinWithM :: forall (m :: Type -> Type) (f :: Natural -> Type) (n :: Natural)
       (w :: Natural).
(1 <= w, Monad m) =>
(forall (l :: Natural).
 (1 <= l) =>
 NatRepr l -> f w -> f l -> m (f (w + l)))
-> NatRepr w -> Vector n (f w) -> m (f (n * w))
joinWithM forall (l :: Natural).
(1 <= l) =>
NatRepr l -> f w -> f l -> m (f (w + l))
jn NatRepr w
w = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (l :: Natural).
Vector l (f w) -> m (f (l * w), NatRepr (l * w))
go
  where
  go :: forall l. Vector l (f w) -> m (f (l * w), NatRepr (l * w))
  go :: forall (l :: Natural).
Vector l (f w) -> m (f (l * w), NatRepr (l * w))
go Vector l (f w)
exprs =
    case forall (n :: Natural) a.
Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))
uncons Vector l (f w)
exprs of
      (f w
a, Left l :~: 1
Refl) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (f w
a, NatRepr w
w)
      (f w
a, Right Vector (l - 1) (f w)
rest) ->
        case forall (n :: Natural) a. Vector n a -> LeqProof 1 n
nonEmpty Vector (l - 1) (f w)
rest                of { LeqProof 1 (l - 1)
LeqProof ->
        case forall (p :: Natural -> Type) (q :: Natural -> Type) (x :: Natural)
       (y :: Natural).
(1 <= x, 1 <= y) =>
p x -> q y -> LeqProof 1 (x * y)
leqMulPos (forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector (l - 1) (f w)
rest) NatRepr w
w    of { LeqProof 1 ((l - 1) * w)
LeqProof ->
        case forall (n :: Natural) a. Vector n a -> LeqProof 1 n
nonEmpty Vector l (f w)
exprs               of { LeqProof 1 l
LeqProof ->
        case forall (n :: Natural) (p :: Natural -> Type) (w :: Natural)
       (q :: Natural -> Type).
(1 <= n) =>
p w -> q n -> (w + ((n - 1) * w)) :~: (n * w)
lemmaMul NatRepr w
w (forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector l (f w)
exprs)    of { (w + ((l - 1) * w)) :~: (l * w)
Refl -> do
          -- @siddharthist: This could probably be written applicatively?
          (f ((l - 1) * w)
res, NatRepr ((l - 1) * w)
sz) <- forall (l :: Natural).
Vector l (f w) -> m (f (l * w), NatRepr (l * w))
go Vector (l - 1) (f w)
rest
          f (w + ((l - 1) * w))
joined <- forall (l :: Natural).
(1 <= l) =>
NatRepr l -> f w -> f l -> m (f (w + l))
jn NatRepr ((l - 1) * w)
sz f w
a f ((l - 1) * w)
res
          forall (m :: Type -> Type) a. Monad m => a -> m a
return (f (w + ((l - 1) * w))
joined, forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr ((l - 1) * w)
sz)
        }}}}

-- | Join a vector of vectors, using the given function to combine the
-- sub-vectors.
joinWith ::
  forall f n w.
  (1 <= w) =>
  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> f (w + l))
  {- ^ A function for joining contained elements.  The first argument is
       the size of the accumulated third term, and the second argument
       is the element to join to the accumulated term.  The function
       can use any join strategy desired (prepending/"BigEndian",
       appending/"LittleEndian", etc.). -}
  -> NatRepr w
  -> Vector n (f w)
  -> f (n * w)
joinWith :: forall (f :: Natural -> Type) (n :: Natural) (w :: Natural).
(1 <= w) =>
(forall (l :: Natural).
 (1 <= l) =>
 NatRepr l -> f w -> f l -> f (w + l))
-> NatRepr w -> Vector n (f w) -> f (n * w)
joinWith forall (l :: Natural).
(1 <= l) =>
NatRepr l -> f w -> f l -> f (w + l)
jn NatRepr w
w Vector n (f w)
v = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) (f :: Natural -> Type) (n :: Natural)
       (w :: Natural).
(1 <= w, Monad m) =>
(forall (l :: Natural).
 (1 <= l) =>
 NatRepr l -> f w -> f l -> m (f (w + l)))
-> NatRepr w -> Vector n (f w) -> m (f (n * w))
joinWithM (\NatRepr l
n f w
x -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (l :: Natural).
(1 <= l) =>
NatRepr l -> f w -> f l -> f (w + l)
jn NatRepr l
n f w
x)) NatRepr w
w Vector n (f w)
v
{-# Inline joinWith #-}

-- | Split a vector into a vector of vectors.
--
-- The "Endian" parameter determines the ordering of the inner
-- vectors.  If "LittleEndian", then less significant bits go into
-- smaller indexes.  If "BigEndian", then less significant bits go
-- into larger indexes.  See the documentation for 'split' for more
-- details.
splitWith :: forall f w n.
  (1 <= w, 1 <= n) =>
  Endian ->
  (forall i. (i + w <= n * w) =>
             NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w)
  {- ^ A function for slicing out a chunk of length @w@, starting at @i@ -} ->
  NatRepr n -> NatRepr w -> f (n * w) -> Vector n (f w)
splitWith :: forall (f :: Natural -> Type) (w :: Natural) (n :: Natural).
(1 <= w, 1 <= n) =>
Endian
-> (forall (i :: Natural).
    ((i + w) <= (n * w)) =>
    NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w)
-> NatRepr n
-> NatRepr w
-> f (n * w)
-> Vector n (f w)
splitWith Endian
endian forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w
select NatRepr n
n NatRepr w
w f (n * w)
val = forall (n :: Natural) a. (1 <= n) => Vector a -> Vector n a
Vector (forall a. (forall s. ST s (MVector s a)) -> Vector a
Vector.create forall s. ST s (MVector s (f w))
initializer)
  where
  len :: Int
len          = forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr n
n
  start :: Int
  next :: Int -> Int
  (Int
start,Int -> Int
next) = case Endian
endian of
                   Endian
LittleEndian -> (Int
0, forall a. Enum a => a -> a
succ)
                   Endian
BigEndian    -> (Int
len forall a. Num a => a -> a -> a
- Int
1, forall a. Enum a => a -> a
pred)

  initializer :: forall s. ST s (MVector s (f w))
  initializer :: forall s. ST s (MVector s (f w))
initializer =
    do LeqProof 1 (n * w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (p :: Natural -> Type) (q :: Natural -> Type) (x :: Natural)
       (y :: Natural).
(1 <= x, 1 <= y) =>
p x -> q y -> LeqProof 1 (x * y)
leqMulPos NatRepr n
n NatRepr w
w)
       LeqProof w (n * w)
LeqProof <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (x :: Natural) (p :: Natural -> Type) (q :: Natural -> Type)
       (y :: Natural).
(1 <= x) =>
p x -> q y -> LeqProof y (x * y)
leqMulMono NatRepr n
n NatRepr w
w)

       MVector s (f w)
v <- forall (m :: Type -> Type) a.
PrimMonad m =>
Int -> m (MVector (PrimState m) a)
MVector.new Int
len
       let fill :: Int -> NatRepr i -> ST s ()
           fill :: forall (i :: Natural). Int -> NatRepr i -> ST s ()
fill Int
loc NatRepr i
i =
             let end :: NatRepr (i + w)
end = forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr i
i NatRepr w
w in
             case forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq NatRepr (i + w)
end NatRepr (n * w)
inLen of
               Just LeqProof (i + w) (n * w)
LeqProof ->
                 do forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MVector.write MVector s (f w)
v Int
loc (forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w
select NatRepr (n * w)
inLen NatRepr i
i f (n * w)
val)
                    forall (i :: Natural). Int -> NatRepr i -> ST s ()
fill (Int -> Int
next Int
loc) NatRepr (i + w)
end
               Maybe (LeqProof (i + w) (n * w))
Nothing -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ()


       forall (i :: Natural). Int -> NatRepr i -> ST s ()
fill Int
start (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0)
       forall (m :: Type -> Type) a. Monad m => a -> m a
return MVector s (f w)
v

  inLen :: NatRepr (n * w)
  inLen :: NatRepr (n * w)
inLen = forall (n :: Natural) (m :: Natural).
NatRepr n -> NatRepr m -> NatRepr (n * m)
natMultiply NatRepr n
n NatRepr w
w
{-# Inline splitWith #-}

-- We can sneakily put our functor in the parameter "f" of @splitWith@ using the
-- @Compose@ newtype.
-- | An applicative version of @splitWith@.
splitWithA :: forall f g w n. (Applicative f, 1 <= w, 1 <= n) =>
  Endian ->
  (forall i. (i + w <= n * w) =>
             NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w))
  {- ^ f function for slicing out f chunk of length @w@, starting at @i@ -} ->
  NatRepr n -> NatRepr w -> g (n * w) -> f (Vector n (g w))
splitWithA :: forall (f :: Type -> Type) (g :: Natural -> Type) (w :: Natural)
       (n :: Natural).
(Applicative f, 1 <= w, 1 <= n) =>
Endian
-> (forall (i :: Natural).
    ((i + w) <= (n * w)) =>
    NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w))
-> NatRepr n
-> NatRepr w
-> g (n * w)
-> f (Vector n (g w))
splitWithA Endian
e forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w)
select NatRepr n
n NatRepr w
w g (n * w)
val = forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose forall a b. (a -> b) -> a -> b
$
  forall (f :: Natural -> Type) (w :: Natural) (n :: Natural).
(1 <= w, 1 <= n) =>
Endian
-> (forall (i :: Natural).
    ((i + w) <= (n * w)) =>
    NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w)
-> NatRepr n
-> NatRepr w
-> f (n * w)
-> Vector n (f w)
splitWith @(Compose f g) Endian
e forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w)
-> NatRepr i -> Compose f g (n * w) -> Compose f g w
select' NatRepr n
n NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall (f :: Type -> Type) a. Applicative f => a -> f a
pure g (n * w)
val)
  where -- Wrap everything in Compose
        select' :: (forall i. (i + w <= n * w)
                => NatRepr (n * w) -> NatRepr i -> Compose f g (n * w) -> Compose f g w)
        -- Whatever we pass in as "val" is what's passed to select anyway,
        -- so there's no need to examine the argument. Just use "val" directly here.
        select' :: forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w)
-> NatRepr i -> Compose f g (n * w) -> Compose f g w
select' NatRepr (n * w)
nw NatRepr i
i Compose f g (n * w)
_ = forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall a b. (a -> b) -> a -> b
$ forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w)
select NatRepr (n * w)
nw NatRepr i
i g (n * w)
val

newtype Vec a n = Vec (Vector n a)

vSlice :: (i + w <= l, 1 <= w) =>
  NatRepr w -> NatRepr l -> NatRepr i -> Vec a l -> Vec a w
vSlice :: forall (i :: Natural) (w :: Natural) (l :: Natural) a.
((i + w) <= l, 1 <= w) =>
NatRepr w -> NatRepr l -> NatRepr i -> Vec a l -> Vec a w
vSlice NatRepr w
w NatRepr l
_ NatRepr i
i (Vec Vector l a
xs) = forall a (n :: Natural). Vector n a -> Vec a n
Vec (forall (i :: Natural) (w :: Natural) (n :: Natural) a.
((i + w) <= n, 1 <= w) =>
NatRepr i -> NatRepr w -> Vector n a -> Vector w a
slice NatRepr i
i NatRepr w
w Vector l a
xs)
{-# Inline vSlice #-}

-- | Append the two bit vectors.  The first argument is
-- at the lower indexes of the resulting vector.
vAppend :: NatRepr n -> Vec a m -> Vec a n -> Vec a (m + n)
vAppend :: forall (n :: Natural) a (m :: Natural).
NatRepr n -> Vec a m -> Vec a n -> Vec a (m + n)
vAppend NatRepr n
_ (Vec Vector m a
xs) (Vec Vector n a
ys) = forall a (n :: Natural). Vector n a -> Vec a n
Vec (forall (m :: Natural) a (n :: Natural).
Vector m a -> Vector n a -> Vector (m + n) a
append Vector m a
xs Vector n a
ys)
{-# Inline vAppend #-}

-- | Split a vector into a vector of vectors.  The default ordering of
-- the outer result vector is "LittleEndian".
--
-- For example:
-- @
--   let wordsize = knownNat :: NatRepr 3
--       vecsize = knownNat :: NatRepr 12
--       numwords = knownNat :: NatRepr 4  (12 / 3)
--       Just inpvec = fromList vecsize [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ]
--   in show (split numwords wordsize inpvec) == "[ [1,2,3], [4,5,6], [7,8,9], [10,11,12] ]"
-- @
-- whereas a BigEndian result would have been
-- @
--      [ [10,11,12], [7,8,9], [4,5,6], [1,2,3] ]
-- @
split :: (1 <= w, 1 <= n) =>
         NatRepr n -- ^ Inner vector size
      -> NatRepr w -- ^ Outer vector size
      -> Vector (n * w) a -- ^ Input vector
      -> Vector n (Vector w a)
split :: forall (w :: Natural) (n :: Natural) a.
(1 <= w, 1 <= n) =>
NatRepr n -> NatRepr w -> Vector (n * w) a -> Vector n (Vector w a)
split NatRepr n
n NatRepr w
w Vector (n * w) a
xs = forall a b (n :: Natural).
Coercible a b =>
Vector n a -> Vector n b
coerceVec (forall (f :: Natural -> Type) (w :: Natural) (n :: Natural).
(1 <= w, 1 <= n) =>
Endian
-> (forall (i :: Natural).
    ((i + w) <= (n * w)) =>
    NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w)
-> NatRepr n
-> NatRepr w
-> f (n * w)
-> Vector n (f w)
splitWith Endian
LittleEndian (forall (i :: Natural) (w :: Natural) (l :: Natural) a.
((i + w) <= l, 1 <= w) =>
NatRepr w -> NatRepr l -> NatRepr i -> Vec a l -> Vec a w
vSlice NatRepr w
w) NatRepr n
n NatRepr w
w (forall a (n :: Natural). Vector n a -> Vec a n
Vec Vector (n * w) a
xs))
{-# Inline split #-}

-- | Join a vector of vectors into a single vector.  Assumes an
-- append/"LittleEndian" join strategy: the order of the inner vectors
-- is preserved in the result vector.
--
-- @
--   let innersize = knownNat :: NatRepr 4
--       Just inner1 = fromList innersize [ 1, 2, 3, 4 ]
--       Just inner2 = fromList innersize [ 5, 6, 7, 8 ]
--       Just inner3 = fromList innersize [ 9, 10, 11, 12 ]
--       outersize = knownNat :: NatRepr 3
--       Just outer = fromList outersize [ inner1, inner2, inner3 ]
--   in show (join innersize outer) = [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ]
-- @
-- a prepend/"BigEndian" join strategy would have the result:
-- @
--   [ 9, 10, 11, 12, 5, 6, 7, 8, 1, 2, 3, 4 ]
-- @
join :: (1 <= w) => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a
join :: forall (w :: Natural) (n :: Natural) a.
(1 <= w) =>
NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a
join NatRepr w
w Vector n (Vector w a)
xs = Vector (n * w) a
ys
  where Vec Vector (n * w) a
ys = forall (f :: Natural -> Type) (n :: Natural) (w :: Natural).
(1 <= w) =>
(forall (l :: Natural).
 (1 <= l) =>
 NatRepr l -> f w -> f l -> f (w + l))
-> NatRepr w -> Vector n (f w) -> f (n * w)
joinWith forall (n :: Natural) a (m :: Natural).
NatRepr n -> Vec a m -> Vec a n -> Vec a (m + n)
vAppend NatRepr w
w (forall a b (n :: Natural).
Coercible a b =>
Vector n a -> Vector n b
coerceVec Vector n (Vector w a)
xs)
{-# Inline join #-}