-- |
-- Module      : Data.Vec
-- Description : Vectors, or length-indexed lists
--
-- This file re-exports definitions from [vec](https://hackage.haskell.org/package/vec)'s
-- [Data.Vec.Lazy](https://hackage.haskell.org/package/vec-0.5.1/docs/Data-Vec-Lazy.html).
--
-- @
-- import 'Vec' ('Vec' (..))
-- import qualified 'Vec' as 'Vec'
-- @
module Data.Vec
  ( module Data.Vec.Lazy,
    vlength,
    append,
    setAt,
    all2
 ) where

-- based on
-- https://hackage.haskell.org/package/fin


import Data.Fin (Fin (..))
import Data.Fin qualified
import Data.Nat
import Data.SNat
import Data.Type.Equality
import Data.Vec.Lazy
import Test.QuickCheck
import Prelude hiding (lookup, repeat, zipWith)

-----------------------------------------------------
-- Vectors (additional definitions)
-----------------------------------------------------

-- | Update a vector value at a given index
setAt :: Fin n -> Vec n a -> a -> Vec n a
setAt :: forall (n :: Nat) a. Fin n -> Vec n a -> a -> Vec n a
setAt Fin n
FZ (a
_ ::: Vec n1 a
vs) a
w = a
w a -> Vec n1 a -> Vec ('S n1) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec n1 a
vs
setAt (FS Fin n1
x) (a
w1 ::: Vec n1 a
env) a
w2 = a
w1 a -> Vec n1 a -> Vec ('S n1) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin n1 -> Vec n1 a -> a -> Vec n1 a
forall (n :: Nat) a. Fin n -> Vec n a -> a -> Vec n a
setAt Fin n1
x Vec n1 a
Vec n1 a
env a
w2

-- | Concatenate two vectors
append :: forall n m a. Vec n a -> Vec m a -> Vec (n + m) a
append :: forall (n :: Nat) (m :: Nat) a. Vec n a -> Vec m a -> Vec (n + m) a
append = Vec n a -> Vec m a -> Vec (Plus n m) a
Vec n a -> Vec m a -> Vec (n + m) a
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
(Data.Vec.Lazy.++)

-- | Access elements by position
lookup :: Fin n -> Vec n a -> a
lookup :: forall (n :: Nat) a. Fin n -> Vec n a -> a
lookup = (Vec n a -> Fin n -> a) -> Fin n -> Vec n a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Vec n a -> Fin n -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
(!)

-- | Calculate length as a singleton value
vlength :: Vec n a -> SNat n
vlength :: forall (n :: Nat) a. Vec n a -> SNat n
vlength Vec n a
VNil = SNat n
SNat 'Z
SZ
vlength (a
_ ::: Vec n1 a
v) = SNat n1 -> (SNatI n1 => SNat n) -> SNat n
forall (n :: Nat) r. SNat n -> (SNatI n => r) -> r
withSNat (Vec n1 a -> SNat n1
forall (n :: Nat) a. Vec n a -> SNat n
vlength Vec n1 a
v) SNat n
SNat ('S n1)
SNatI n1 => SNat n
forall (n1 :: Nat). SNatI n1 => SNat ('S n1)
SS


-- >>> all (\x -> x > 3) (4 ::: 5 ::: VNil)
-- True

-- | Ensure that a binary predicate holds for
-- corresponding elements in two vectors
all2 :: (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
all2 :: forall a b (n :: Nat).
(a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
all2 a -> b -> Bool
f (a
x ::: Vec n1 a
xs) (b
y ::: Vec n1 b
ys) = a -> b -> Bool
f a
x b
y Bool -> Bool -> Bool
&& (a -> b -> Bool) -> Vec n1 a -> Vec n1 b -> Bool
forall a b (n :: Nat).
(a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
all2 a -> b -> Bool
f Vec n1 a
xs Vec n1 b
Vec n1 b
ys
all2 a -> b -> Bool
f Vec n a
VNil Vec n b
VNil = Bool
True