{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}

module ZkFold.Base.Data.Vector where

import           Control.DeepSeq                  (NFData)
import           Control.Monad.State.Strict       (runState, state)
import           Data.Aeson                       (ToJSON (..))
import           Data.Distributive                (Distributive (..))
import           Data.Foldable                    (fold)
import           Data.Functor.Rep                 (Representable (..), collectRep, distributeRep, mzipRep, pureRep)
import           Data.These                       (These (..))
import qualified Data.Vector                      as V
import           Data.Vector.Binary               ()
import qualified Data.Vector.Split                as V
import           Data.Zip                         (Semialign (..), Zip (..))
import           GHC.Generics                     (Generic)
import           GHC.IsList                       (IsList (..))
import           Prelude                          hiding (concat, drop, head, length, mod, replicate, sum, tail, take,
                                                   zip, zipWith, (*))
import           System.Random                    (Random (..))
import           Test.QuickCheck                  (Arbitrary (..))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Data.ByteString      (Binary (..))
import           ZkFold.Prelude                   (length)

newtype Vector (size :: Natural) a = Vector {forall (size :: Natural) a. Vector size a -> Vector a
toV :: V.Vector a}
    deriving (Int -> Vector size a -> ShowS
[Vector size a] -> ShowS
Vector size a -> String
(Int -> Vector size a -> ShowS)
-> (Vector size a -> String)
-> ([Vector size a] -> ShowS)
-> Show (Vector size a)
forall (size :: Natural) a. Show a => Int -> Vector size a -> ShowS
forall (size :: Natural) a. Show a => [Vector size a] -> ShowS
forall (size :: Natural) a. Show a => Vector size a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (size :: Natural) a. Show a => Int -> Vector size a -> ShowS
showsPrec :: Int -> Vector size a -> ShowS
$cshow :: forall (size :: Natural) a. Show a => Vector size a -> String
show :: Vector size a -> String
$cshowList :: forall (size :: Natural) a. Show a => [Vector size a] -> ShowS
showList :: [Vector size a] -> ShowS
Show, Vector size a -> Vector size a -> Bool
(Vector size a -> Vector size a -> Bool)
-> (Vector size a -> Vector size a -> Bool) -> Eq (Vector size a)
forall (size :: Natural) a.
Eq a =>
Vector size a -> Vector size a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (size :: Natural) a.
Eq a =>
Vector size a -> Vector size a -> Bool
== :: Vector size a -> Vector size a -> Bool
$c/= :: forall (size :: Natural) a.
Eq a =>
Vector size a -> Vector size a -> Bool
/= :: Vector size a -> Vector size a -> Bool
Eq, (forall a b. (a -> b) -> Vector size a -> Vector size b)
-> (forall a b. a -> Vector size b -> Vector size a)
-> Functor (Vector size)
forall (size :: Natural) a b. a -> Vector size b -> Vector size a
forall (size :: Natural) a b.
(a -> b) -> Vector size a -> Vector size b
forall a b. a -> Vector size b -> Vector size a
forall a b. (a -> b) -> Vector size a -> Vector size b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (size :: Natural) a b.
(a -> b) -> Vector size a -> Vector size b
fmap :: forall a b. (a -> b) -> Vector size a -> Vector size b
$c<$ :: forall (size :: Natural) a b. a -> Vector size b -> Vector size a
<$ :: forall a b. a -> Vector size b -> Vector size a
Functor, (forall m. Monoid m => Vector size m -> m)
-> (forall m a. Monoid m => (a -> m) -> Vector size a -> m)
-> (forall m a. Monoid m => (a -> m) -> Vector size a -> m)
-> (forall a b. (a -> b -> b) -> b -> Vector size a -> b)
-> (forall a b. (a -> b -> b) -> b -> Vector size a -> b)
-> (forall b a. (b -> a -> b) -> b -> Vector size a -> b)
-> (forall b a. (b -> a -> b) -> b -> Vector size a -> b)
-> (forall a. (a -> a -> a) -> Vector size a -> a)
-> (forall a. (a -> a -> a) -> Vector size a -> a)
-> (forall a. Vector size a -> [a])
-> (forall a. Vector size a -> Bool)
-> (forall a. Vector size a -> Int)
-> (forall a. Eq a => a -> Vector size a -> Bool)
-> (forall a. Ord a => Vector size a -> a)
-> (forall a. Ord a => Vector size a -> a)
-> (forall a. Num a => Vector size a -> a)
-> (forall a. Num a => Vector size a -> a)
-> Foldable (Vector size)
forall (size :: Natural) a. Eq a => a -> Vector size a -> Bool
forall (size :: Natural) a. Num a => Vector size a -> a
forall (size :: Natural) a. Ord a => Vector size a -> a
forall (size :: Natural) m. Monoid m => Vector size m -> m
forall (size :: Natural) a. Vector size a -> Bool
forall (size :: Natural) a. Vector size a -> Int
forall (size :: Natural) a. Vector size a -> [a]
forall (size :: Natural) a. (a -> a -> a) -> Vector size a -> a
forall (size :: Natural) m a.
Monoid m =>
(a -> m) -> Vector size a -> m
forall (size :: Natural) b a.
(b -> a -> b) -> b -> Vector size a -> b
forall (size :: Natural) a b.
(a -> b -> b) -> b -> Vector size a -> b
forall a. Eq a => a -> Vector size a -> Bool
forall a. Num a => Vector size a -> a
forall a. Ord a => Vector size a -> a
forall m. Monoid m => Vector size m -> m
forall a. Vector size a -> Bool
forall a. Vector size a -> Int
forall a. Vector size a -> [a]
forall a. (a -> a -> a) -> Vector size a -> a
forall m a. Monoid m => (a -> m) -> Vector size a -> m
forall b a. (b -> a -> b) -> b -> Vector size a -> b
forall a b. (a -> b -> b) -> b -> Vector size a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall (size :: Natural) m. Monoid m => Vector size m -> m
fold :: forall m. Monoid m => Vector size m -> m
$cfoldMap :: forall (size :: Natural) m a.
Monoid m =>
(a -> m) -> Vector size a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Vector size a -> m
$cfoldMap' :: forall (size :: Natural) m a.
Monoid m =>
(a -> m) -> Vector size a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Vector size a -> m
$cfoldr :: forall (size :: Natural) a b.
(a -> b -> b) -> b -> Vector size a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Vector size a -> b
$cfoldr' :: forall (size :: Natural) a b.
(a -> b -> b) -> b -> Vector size a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Vector size a -> b
$cfoldl :: forall (size :: Natural) b a.
(b -> a -> b) -> b -> Vector size a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Vector size a -> b
$cfoldl' :: forall (size :: Natural) b a.
(b -> a -> b) -> b -> Vector size a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Vector size a -> b
$cfoldr1 :: forall (size :: Natural) a. (a -> a -> a) -> Vector size a -> a
foldr1 :: forall a. (a -> a -> a) -> Vector size a -> a
$cfoldl1 :: forall (size :: Natural) a. (a -> a -> a) -> Vector size a -> a
foldl1 :: forall a. (a -> a -> a) -> Vector size a -> a
$ctoList :: forall (size :: Natural) a. Vector size a -> [a]
toList :: forall a. Vector size a -> [a]
$cnull :: forall (size :: Natural) a. Vector size a -> Bool
null :: forall a. Vector size a -> Bool
$clength :: forall (size :: Natural) a. Vector size a -> Int
length :: forall a. Vector size a -> Int
$celem :: forall (size :: Natural) a. Eq a => a -> Vector size a -> Bool
elem :: forall a. Eq a => a -> Vector size a -> Bool
$cmaximum :: forall (size :: Natural) a. Ord a => Vector size a -> a
maximum :: forall a. Ord a => Vector size a -> a
$cminimum :: forall (size :: Natural) a. Ord a => Vector size a -> a
minimum :: forall a. Ord a => Vector size a -> a
$csum :: forall (size :: Natural) a. Num a => Vector size a -> a
sum :: forall a. Num a => Vector size a -> a
$cproduct :: forall (size :: Natural) a. Num a => Vector size a -> a
product :: forall a. Num a => Vector size a -> a
Foldable, Functor (Vector size)
Foldable (Vector size)
(Functor (Vector size), Foldable (Vector size)) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> Vector size a -> f (Vector size b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    Vector size (f a) -> f (Vector size a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Vector size a -> m (Vector size b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    Vector size (m a) -> m (Vector size a))
-> Traversable (Vector size)
forall (size :: Natural). Functor (Vector size)
forall (size :: Natural). Foldable (Vector size)
forall (size :: Natural) (m :: Type -> Type) a.
Monad m =>
Vector size (m a) -> m (Vector size a)
forall (size :: Natural) (f :: Type -> Type) a.
Applicative f =>
Vector size (f a) -> f (Vector size a)
forall (size :: Natural) (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Vector size a -> m (Vector size b)
forall (size :: Natural) (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector size a -> f (Vector size b)
forall (t :: Type -> Type).
(Functor t, Foldable t) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a.
Monad m =>
Vector size (m a) -> m (Vector size a)
forall (f :: Type -> Type) a.
Applicative f =>
Vector size (f a) -> f (Vector size a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Vector size a -> m (Vector size b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector size a -> f (Vector size b)
$ctraverse :: forall (size :: Natural) (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector size a -> f (Vector size b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector size a -> f (Vector size b)
$csequenceA :: forall (size :: Natural) (f :: Type -> Type) a.
Applicative f =>
Vector size (f a) -> f (Vector size a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Vector size (f a) -> f (Vector size a)
$cmapM :: forall (size :: Natural) (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Vector size a -> m (Vector size b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Vector size a -> m (Vector size b)
$csequence :: forall (size :: Natural) (m :: Type -> Type) a.
Monad m =>
Vector size (m a) -> m (Vector size a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
Vector size (m a) -> m (Vector size a)
Traversable, (forall x. Vector size a -> Rep (Vector size a) x)
-> (forall x. Rep (Vector size a) x -> Vector size a)
-> Generic (Vector size a)
forall (size :: Natural) a x.
Rep (Vector size a) x -> Vector size a
forall (size :: Natural) a x.
Vector size a -> Rep (Vector size a) x
forall x. Rep (Vector size a) x -> Vector size a
forall x. Vector size a -> Rep (Vector size a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (size :: Natural) a x.
Vector size a -> Rep (Vector size a) x
from :: forall x. Vector size a -> Rep (Vector size a) x
$cto :: forall (size :: Natural) a x.
Rep (Vector size a) x -> Vector size a
to :: forall x. Rep (Vector size a) x -> Vector size a
Generic, Vector size a -> ()
(Vector size a -> ()) -> NFData (Vector size a)
forall (size :: Natural) a. NFData a => Vector size a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (size :: Natural) a. NFData a => Vector size a -> ()
rnf :: Vector size a -> ()
NFData, Eq (Vector size a)
Eq (Vector size a) =>
(Vector size a -> Vector size a -> Ordering)
-> (Vector size a -> Vector size a -> Bool)
-> (Vector size a -> Vector size a -> Bool)
-> (Vector size a -> Vector size a -> Bool)
-> (Vector size a -> Vector size a -> Bool)
-> (Vector size a -> Vector size a -> Vector size a)
-> (Vector size a -> Vector size a -> Vector size a)
-> Ord (Vector size a)
Vector size a -> Vector size a -> Bool
Vector size a -> Vector size a -> Ordering
Vector size a -> Vector size a -> Vector size a
forall (size :: Natural) a. Ord a => Eq (Vector size a)
forall (size :: Natural) a.
Ord a =>
Vector size a -> Vector size a -> Bool
forall (size :: Natural) a.
Ord a =>
Vector size a -> Vector size a -> Ordering
forall (size :: Natural) a.
Ord a =>
Vector size a -> Vector size a -> Vector size a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (size :: Natural) a.
Ord a =>
Vector size a -> Vector size a -> Ordering
compare :: Vector size a -> Vector size a -> Ordering
$c< :: forall (size :: Natural) a.
Ord a =>
Vector size a -> Vector size a -> Bool
< :: Vector size a -> Vector size a -> Bool
$c<= :: forall (size :: Natural) a.
Ord a =>
Vector size a -> Vector size a -> Bool
<= :: Vector size a -> Vector size a -> Bool
$c> :: forall (size :: Natural) a.
Ord a =>
Vector size a -> Vector size a -> Bool
> :: Vector size a -> Vector size a -> Bool
$c>= :: forall (size :: Natural) a.
Ord a =>
Vector size a -> Vector size a -> Bool
>= :: Vector size a -> Vector size a -> Bool
$cmax :: forall (size :: Natural) a.
Ord a =>
Vector size a -> Vector size a -> Vector size a
max :: Vector size a -> Vector size a -> Vector size a
$cmin :: forall (size :: Natural) a.
Ord a =>
Vector size a -> Vector size a -> Vector size a
min :: Vector size a -> Vector size a -> Vector size a
Ord)

-- helper
knownNat :: forall size n . (KnownNat size, Integral n) => n
knownNat :: forall (size :: Natural) n. (KnownNat size, Integral n) => n
knownNat = Natural -> n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural). KnownNat n => Natural
value @size)

instance KnownNat size => Representable (Vector size) where
  type Rep (Vector size) = Zp size
  index :: forall a. Vector size a -> Rep (Vector size) -> a
index (Vector Vector a
v) Rep (Vector size)
ix = Vector a
v Vector a -> Int -> a
forall a. Vector a -> Int -> a
V.! (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Zp size -> Natural
forall (p :: Natural). Zp p -> Natural
fromZp Rep (Vector size)
Zp size
ix))
  tabulate :: forall a. (Rep (Vector size) -> a) -> Vector size a
tabulate Rep (Vector size) -> a
f = Vector a -> Vector size a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Int -> (Int -> a) -> Vector a
forall a. Int -> (Int -> a) -> Vector a
V.generate (forall (size :: Natural) n. (KnownNat size, Integral n) => n
knownNat @size) (Rep (Vector size) -> a
Zp size -> a
f (Zp size -> a) -> (Int -> Zp size) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Zp size
forall a b. (Integral a, Num b) => a -> b
fromIntegral))

instance KnownNat size => Distributive (Vector size) where
  distribute :: forall (f :: Type -> Type) a.
Functor f =>
f (Vector size a) -> Vector size (f a)
distribute = f (Vector size a) -> Vector size (f a)
forall (f :: Type -> Type) (w :: Type -> Type) a.
(Representable f, Functor w) =>
w (f a) -> f (w a)
distributeRep
  collect :: forall (f :: Type -> Type) a b.
Functor f =>
(a -> Vector size b) -> f a -> Vector size (f b)
collect = (a -> Vector size b) -> f a -> Vector size (f b)
forall (f :: Type -> Type) (w :: Type -> Type) a b.
(Representable f, Functor w) =>
(a -> f b) -> w a -> f (w b)
collectRep


vtoVector :: forall size a . KnownNat size => V.Vector a -> Maybe (Vector size a)
vtoVector :: forall (size :: Natural) a.
KnownNat size =>
Vector a -> Maybe (Vector size a)
vtoVector Vector a
as
  | Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== forall (size :: Natural) n. (KnownNat size, Integral n) => n
knownNat @size = Vector size a -> Maybe (Vector size a)
forall a. a -> Maybe a
Just (Vector size a -> Maybe (Vector size a))
-> Vector size a -> Maybe (Vector size a)
forall a b. (a -> b) -> a -> b
$ Vector a -> Vector size a
forall (size :: Natural) a. Vector a -> Vector size a
Vector Vector a
as
  | Bool
otherwise                     = Maybe (Vector size a)
forall a. Maybe a
Nothing

instance IsList (Vector n a) where
    type Item (Vector n a) = a
    toList :: Vector n a -> [Item (Vector n a)]
toList = Vector n a -> [a]
Vector n a -> [Item (Vector n a)]
forall (size :: Natural) a. Vector size a -> [a]
fromVector
    fromList :: [Item (Vector n a)] -> Vector n a
fromList = [a] -> Vector n a
[Item (Vector n a)] -> Vector n a
forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector

toVector :: forall size a . KnownNat size => [a] -> Maybe (Vector size a)
toVector :: forall (size :: Natural) a.
KnownNat size =>
[a] -> Maybe (Vector size a)
toVector [a]
as
    | [a] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [a]
as Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== forall (n :: Natural). KnownNat n => Natural
value @size = Vector size a -> Maybe (Vector size a)
forall a. a -> Maybe a
Just (Vector size a -> Maybe (Vector size a))
-> Vector size a -> Maybe (Vector size a)
forall a b. (a -> b) -> a -> b
$ Vector a -> Vector size a
forall (size :: Natural) a. Vector a -> Vector size a
Vector ([a] -> Vector a
forall a. [a] -> Vector a
V.fromList [a]
as)
    | Bool
otherwise                = Maybe (Vector size a)
forall a. Maybe a
Nothing

unsafeToVector :: forall size a . [a] -> Vector size a
unsafeToVector :: forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector = Vector a -> Vector size a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector size a)
-> ([a] -> Vector a) -> [a] -> Vector size a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Vector a
forall a. [a] -> Vector a
V.fromList

unfold :: forall size a b. KnownNat size => (b -> (a, b)) -> b -> Vector size a
unfold :: forall (size :: Natural) a b.
KnownNat size =>
(b -> (a, b)) -> b -> Vector size a
unfold b -> (a, b)
f = Vector a -> Vector size a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector size a)
-> (b -> Vector a) -> b -> Vector size a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Vector a -> Vector a
forall a. Int -> Vector a -> Vector a
V.take (forall (size :: Natural) n. (KnownNat size, Integral n) => n
knownNat @size) (Vector a -> Vector a) -> (b -> Vector a) -> b -> Vector a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Maybe (a, b)) -> b -> Vector a
forall b a. (b -> Maybe (a, b)) -> b -> Vector a
V.unfoldr ((a, b) -> Maybe (a, b)
forall a. a -> Maybe a
Just ((a, b) -> Maybe (a, b)) -> (b -> (a, b)) -> b -> Maybe (a, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> (a, b)
f)

fromVector :: Vector size a -> [a]
fromVector :: forall (size :: Natural) a. Vector size a -> [a]
fromVector (Vector Vector a
as) = Vector a -> [a]
forall a. Vector a -> [a]
V.toList Vector a
as

(!!) :: Vector size a -> Natural -> a
(Vector Vector a
as) !! :: forall (size :: Natural) a. Vector size a -> Natural -> a
!! Natural
i = Vector a
as Vector a -> Int -> a
forall a. Vector a -> Int -> a
V.! Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i

uncons :: Vector size a -> (a, Vector (size - 1) a)
uncons :: forall (size :: Natural) a.
Vector size a -> (a, Vector (size - 1) a)
uncons (Vector Vector a
lst) = (Vector a -> a
forall a. Vector a -> a
V.head Vector a
lst, Vector a -> Vector (size - 1) a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector (size - 1) a)
-> Vector a -> Vector (size - 1) a
forall a b. (a -> b) -> a -> b
$ Vector a -> Vector a
forall a. Vector a -> Vector a
V.tail Vector a
lst)

reverse :: Vector size a -> Vector size a
reverse :: forall (size :: Natural) a. Vector size a -> Vector size a
reverse (Vector Vector a
lst) = Vector a -> Vector size a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector a
forall a. Vector a -> Vector a
V.reverse Vector a
lst)

head :: Vector size a -> a
head :: forall (size :: Natural) a. Vector size a -> a
head (Vector Vector a
as) = Vector a -> a
forall a. Vector a -> a
V.head Vector a
as

tail :: Vector size a -> Vector (size - 1) a
tail :: forall (size :: Natural) a. Vector size a -> Vector (size - 1) a
tail (Vector Vector a
as) = Vector a -> Vector (size - 1) a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector (size - 1) a)
-> Vector a -> Vector (size - 1) a
forall a b. (a -> b) -> a -> b
$ Vector a -> Vector a
forall a. Vector a -> Vector a
V.tail Vector a
as

singleton :: a -> Vector 1 a
singleton :: forall a. a -> Vector 1 a
singleton = Vector a -> Vector 1 a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector 1 a) -> (a -> Vector a) -> a -> Vector 1 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Vector a
forall a. a -> Vector a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure

item :: Vector 1 a -> a
item :: forall a. Vector 1 a -> a
item = Vector 1 a -> a
forall (size :: Natural) a. Vector size a -> a
head

mapWithIx :: forall n a b . KnownNat n => (Natural -> a -> b) -> Vector n a -> Vector n b
mapWithIx :: forall (n :: Natural) a b.
KnownNat n =>
(Natural -> a -> b) -> Vector n a -> Vector n b
mapWithIx Natural -> a -> b
f (Vector Vector a
l) = Vector b -> Vector n b
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector b -> Vector n b) -> Vector b -> Vector n b
forall a b. (a -> b) -> a -> b
$ (Natural -> a -> b) -> Vector Natural -> Vector a -> Vector b
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith Natural -> a -> b
f (Natural -> Natural -> Vector Natural
forall a. Enum a => a -> a -> Vector a
V.enumFromTo Natural
0 (forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! Natural
1)) Vector a
l

mapMWithIx :: forall n m a b . (KnownNat n, Monad m) => (Natural -> a -> m b) -> Vector n a -> m (Vector n b)
mapMWithIx :: forall (n :: Natural) (m :: Type -> Type) a b.
(KnownNat n, Monad m) =>
(Natural -> a -> m b) -> Vector n a -> m (Vector n b)
mapMWithIx Natural -> a -> m b
f (Vector Vector a
l) = Vector b -> Vector n b
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector b -> Vector n b) -> m (Vector b) -> m (Vector n b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Natural -> a -> m b) -> Vector Natural -> Vector a -> m (Vector b)
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> m c) -> Vector a -> Vector b -> m (Vector c)
V.zipWithM Natural -> a -> m b
f (Natural -> Natural -> Vector Natural
forall a. Enum a => a -> a -> Vector a
V.enumFromTo Natural
0 (forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! Natural
1)) Vector a
l

-- TODO: Check that n <= size?
take :: forall n size a. KnownNat n => Vector size a -> Vector n a
take :: forall (n :: Natural) (size :: Natural) a.
KnownNat n =>
Vector size a -> Vector n a
take (Vector Vector a
lst) = Vector a -> Vector n a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Int -> Vector a -> Vector a
forall a. Int -> Vector a -> Vector a
V.take (forall (size :: Natural) n. (KnownNat size, Integral n) => n
knownNat @n) Vector a
lst)

drop :: forall n m a. KnownNat n => Vector (n + m) a -> Vector m a
drop :: forall (n :: Natural) (m :: Natural) a.
KnownNat n =>
Vector (n + m) a -> Vector m a
drop (Vector Vector a
lst) = Vector a -> Vector m a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Int -> Vector a -> Vector a
forall a. Int -> Vector a -> Vector a
V.drop (forall (size :: Natural) n. (KnownNat size, Integral n) => n
knownNat @n) Vector a
lst)

splitAt :: forall n m a. KnownNat n => Vector (n + m) a -> (Vector n a, Vector m a)
splitAt :: forall (n :: Natural) (m :: Natural) a.
KnownNat n =>
Vector (n + m) a -> (Vector n a, Vector m a)
splitAt (Vector Vector a
lst) = (Vector a -> Vector n a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Int -> Vector a -> Vector a
forall a. Int -> Vector a -> Vector a
V.take (forall (size :: Natural) n. (KnownNat size, Integral n) => n
knownNat @n) Vector a
lst), Vector a -> Vector m a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Int -> Vector a -> Vector a
forall a. Int -> Vector a -> Vector a
V.drop (forall (size :: Natural) n. (KnownNat size, Integral n) => n
knownNat @n) Vector a
lst))

rotate :: forall size a. KnownNat size => Vector size a -> Integer -> Vector size a
rotate :: forall (size :: Natural) a.
KnownNat size =>
Vector size a -> Integer -> Vector size a
rotate (Vector Vector a
lst) Integer
n = Vector a -> Vector size a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a
r Vector a -> Vector a -> Vector a
forall a. Semigroup a => a -> a -> a
<> Vector a
l)
    where
        len :: Integer
        len :: Integer
len = Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Integer) -> Natural -> Integer
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @size

        lshift :: Int
        lshift :: Int
lshift = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. SemiEuclidean a => a -> a -> a
`mod` Integer
len

        (Vector a
l, Vector a
r) = Int -> Vector a -> (Vector a, Vector a)
forall a. Int -> Vector a -> (Vector a, Vector a)
V.splitAt Int
lshift Vector a
lst

shift :: forall size a. KnownNat size => Vector size a -> Integer -> a -> Vector size a
shift :: forall (size :: Natural) a.
KnownNat size =>
Vector size a -> Integer -> a -> Vector size a
shift (Vector Vector a
lst) Integer
n a
pad
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Vector a -> Vector size a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector size a) -> Vector a -> Vector size a
forall a b. (a -> b) -> a -> b
$ Int -> Vector a -> Vector a
forall a. Int -> Vector a -> Vector a
V.take (forall (size :: Natural) n. (KnownNat size, Integral n) => n
knownNat @size) (Vector a
padList Vector a -> Vector a -> Vector a
forall a. Semigroup a => a -> a -> a
<> Vector a
lst)
  | Bool
otherwise = Vector a -> Vector size a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector size a) -> Vector a -> Vector size a
forall a b. (a -> b) -> a -> b
$ Int -> Vector a -> Vector a
forall a. Int -> Vector a -> Vector a
V.drop (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n) (Vector a
lst Vector a -> Vector a -> Vector a
forall a. Semigroup a => a -> a -> a
<> Vector a
padList)
    where
        padList :: Vector a
padList = Int -> a -> Vector a
forall a. Int -> a -> Vector a
V.replicate (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
abs Integer
n) a
pad

vectorDotProduct :: forall size a . Semiring a => Vector size a -> Vector size a -> a
vectorDotProduct :: forall (size :: Natural) a.
Semiring a =>
Vector size a -> Vector size a -> a
vectorDotProduct (Vector Vector a
as) (Vector Vector a
bs) = Vector a -> a
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum (Vector a -> a) -> Vector a -> a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> Vector a -> Vector a -> Vector a
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
(*) Vector a
as Vector a
bs

empty :: Vector 0 a
empty :: forall a. Vector 0 a
empty = Vector a -> Vector 0 a
forall (size :: Natural) a. Vector a -> Vector size a
Vector Vector a
forall a. Vector a
V.empty

infixr 5 .:
(.:) :: a -> Vector n a -> Vector (n + 1) a
a
a .: :: forall a (n :: Natural). a -> Vector n a -> Vector (n + 1) a
.: (Vector Vector a
lst) = Vector a -> Vector (n + 1) a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (a
a a -> Vector a -> Vector a
forall a. a -> Vector a -> Vector a
`V.cons` Vector a
lst)

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 (Vector Vector a
l) (Vector Vector a
r) = Vector a -> Vector (m + n) a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a
l Vector a -> Vector a -> Vector a
forall a. Semigroup a => a -> a -> a
<> Vector a
r)

concat :: Vector m (Vector n a) -> Vector (m * n) a
concat :: forall (m :: Natural) (n :: Natural) a.
Vector m (Vector n a) -> Vector (m * n) a
concat = Vector a -> Vector (m * n) a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector (m * n) a)
-> (Vector m (Vector n a) -> Vector a)
-> Vector m (Vector n a)
-> Vector (m * n) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vector n a -> Vector a) -> Vector (Vector n a) -> Vector a
forall a b. (a -> Vector b) -> Vector a -> Vector b
V.concatMap Vector n a -> Vector a
forall (size :: Natural) a. Vector size a -> Vector a
toV (Vector (Vector n a) -> Vector a)
-> (Vector m (Vector n a) -> Vector (Vector n a))
-> Vector m (Vector n a)
-> Vector a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector m (Vector n a) -> Vector (Vector n a)
forall (size :: Natural) a. Vector size a -> Vector a
toV

unsafeConcat :: forall m n a . [Vector n a] -> Vector (m * n) a
unsafeConcat :: forall (m :: Natural) (n :: Natural) a.
[Vector n a] -> Vector (m * n) a
unsafeConcat = Vector m (Vector n a) -> Vector (m * n) a
forall (m :: Natural) (n :: Natural) a.
Vector m (Vector n a) -> Vector (m * n) a
concat (Vector m (Vector n a) -> Vector (m * n) a)
-> ([Vector n a] -> Vector m (Vector n a))
-> [Vector n a]
-> Vector (m * n) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector @m

chunks :: forall m n a . KnownNat n => Vector (m * n) a -> Vector m (Vector n a)
chunks :: forall (m :: Natural) (n :: Natural) a.
KnownNat n =>
Vector (m * n) a -> Vector m (Vector n a)
chunks (Vector Vector a
vectors) = [Vector n a] -> Vector m (Vector n a)
forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector (Vector a -> Vector n a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector n a) -> [Vector a] -> [Vector n a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Vector a -> [Vector a]
forall (v :: Type -> Type) a. Vector v a => Int -> v a -> [v a]
V.chunksOf (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @n) Vector a
vectors)

instance (KnownNat n, Binary a) => Binary (Vector n a) where
    put :: Vector n a -> Put
put = Vector Put -> Put
forall m. Monoid m => Vector m -> m
forall (t :: Type -> Type) m. (Foldable t, Monoid m) => t m -> m
fold (Vector Put -> Put)
-> (Vector n a -> Vector Put) -> Vector n a -> Put
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Put) -> Vector a -> Vector Put
forall a b. (a -> b) -> Vector a -> Vector b
V.map a -> Put
forall t. Binary t => t -> Put
put (Vector a -> Vector Put)
-> (Vector n a -> Vector a) -> Vector n a -> Vector Put
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector n a -> Vector a
forall (size :: Natural) a. Vector size a -> Vector a
toV
    get :: Get (Vector n a)
get = Vector a -> Vector n a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector n a) -> Get (Vector a) -> Get (Vector n a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Get a -> Get (Vector a)
forall (m :: Type -> Type) a. Monad m => Int -> m a -> m (Vector a)
V.replicateM (forall (size :: Natural) n. (KnownNat size, Integral n) => n
knownNat @n) Get a
forall t. Binary t => Get t
get

instance KnownNat size => Applicative (Vector size) where
    pure :: forall a. a -> Vector size a
pure a
a = Vector a -> Vector size a
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector a -> Vector size a) -> Vector a -> Vector size a
forall a b. (a -> b) -> a -> b
$ Int -> a -> Vector a
forall a. Int -> a -> Vector a
V.replicate (forall (size :: Natural) n. (KnownNat size, Integral n) => n
knownNat @size) a
a

    (Vector Vector (a -> b)
fs) <*> :: forall a b. Vector size (a -> b) -> Vector size a -> Vector size b
<*> (Vector Vector a
as) = Vector b -> Vector size b
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector b -> Vector size b) -> Vector b -> Vector size b
forall a b. (a -> b) -> a -> b
$ ((a -> b) -> a -> b) -> Vector (a -> b) -> Vector a -> Vector b
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($) Vector (a -> b)
fs Vector a
as

instance Semialign (Vector size) where
    align :: forall a b.
Vector size a -> Vector size b -> Vector size (These a b)
align (Vector Vector a
as) (Vector Vector b
bs) = Vector (These a b) -> Vector size (These a b)
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector (These a b) -> Vector size (These a b))
-> Vector (These a b) -> Vector size (These a b)
forall a b. (a -> b) -> a -> b
$ (a -> b -> These a b) -> Vector a -> Vector b -> Vector (These a b)
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith a -> b -> These a b
forall a b. a -> b -> These a b
These Vector a
as Vector b
bs

instance Zip (Vector size) where
    zip :: forall a b. Vector size a -> Vector size b -> Vector size (a, b)
zip (Vector Vector a
as) (Vector Vector b
bs) = Vector (a, b) -> Vector size (a, b)
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector (a, b) -> Vector size (a, b))
-> Vector (a, b) -> Vector size (a, b)
forall a b. (a -> b) -> a -> b
$ Vector a -> Vector b -> Vector (a, b)
forall a b. Vector a -> Vector b -> Vector (a, b)
V.zip Vector a
as Vector b
bs

    zipWith :: forall a b c.
(a -> b -> c) -> Vector size a -> Vector size b -> Vector size c
zipWith a -> b -> c
f (Vector Vector a
as) (Vector Vector b
bs) = Vector c -> Vector size c
forall (size :: Natural) a. Vector a -> Vector size a
Vector (Vector c -> Vector size c) -> Vector c -> Vector size c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> Vector a -> Vector b -> Vector c
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith a -> b -> c
f Vector a
as Vector b
bs

instance (Arbitrary a, KnownNat size) => Arbitrary (Vector size a) where
    arbitrary :: Gen (Vector size a)
arbitrary = Vector size (Gen a) -> Gen (Vector size a)
forall (t :: Type -> Type) (f :: Type -> Type) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: Type -> Type) a.
Applicative f =>
Vector size (f a) -> f (Vector size a)
sequenceA (Gen a -> Vector size (Gen a)
forall (f :: Type -> Type) a. Representable f => a -> f a
pureRep Gen a
forall a. Arbitrary a => Gen a
arbitrary)

instance (Random a, KnownNat size) => Random (Vector size a) where
    random :: forall g. RandomGen g => g -> (Vector size a, g)
random = State g (Vector size a) -> g -> (Vector size a, g)
forall s a. State s a -> s -> (a, s)
runState (Vector size (StateT g Identity a) -> State g (Vector size a)
forall (t :: Type -> Type) (f :: Type -> Type) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: Type -> Type) a.
Applicative f =>
Vector size (f a) -> f (Vector size a)
sequenceA (StateT g Identity a -> Vector size (StateT g Identity a)
forall (f :: Type -> Type) a. Representable f => a -> f a
pureRep ((g -> (a, g)) -> StateT g Identity a
forall a. (g -> (a, g)) -> StateT g Identity a
forall s (m :: Type -> Type) a.
MonadState s m =>
(s -> (a, s)) -> m a
state g -> (a, g)
forall g. RandomGen g => g -> (a, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random)))
    randomR :: forall g.
RandomGen g =>
(Vector size a, Vector size a) -> g -> (Vector size a, g)
randomR = State g (Vector size a) -> g -> (Vector size a, g)
forall s a. State s a -> s -> (a, s)
runState (State g (Vector size a) -> g -> (Vector size a, g))
-> ((Vector size a, Vector size a) -> State g (Vector size a))
-> (Vector size a, Vector size a)
-> g
-> (Vector size a, g)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, a) -> StateT g Identity a)
-> Vector size (a, a) -> State g (Vector size a)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector size a -> f (Vector size b)
traverse ((g -> (a, g)) -> StateT g Identity a
forall a. (g -> (a, g)) -> StateT g Identity a
forall s (m :: Type -> Type) a.
MonadState s m =>
(s -> (a, s)) -> m a
state ((g -> (a, g)) -> StateT g Identity a)
-> ((a, a) -> g -> (a, g)) -> (a, a) -> StateT g Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, a) -> g -> (a, g)
forall g. RandomGen g => (a, a) -> g -> (a, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR) (Vector size (a, a) -> State g (Vector size a))
-> ((Vector size a, Vector size a) -> Vector size (a, a))
-> (Vector size a, Vector size a)
-> State g (Vector size a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vector size a -> Vector size a -> Vector size (a, a))
-> (Vector size a, Vector size a) -> Vector size (a, a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Vector size a -> Vector size a -> Vector size (a, a)
forall (f :: Type -> Type) a b.
Representable f =>
f a -> f b -> f (a, b)
mzipRep

instance ToJSON a => ToJSON (Vector n a) where
    toJSON :: Vector n a -> Value
toJSON (Vector Vector a
xs) = Vector a -> Value
forall a. ToJSON a => a -> Value
toJSON Vector a
xs