module Parsley.Internal.Common.Vec (module Parsley.Internal.Common.Vec, Nat(..)) where

import Parsley.Internal.Common.Indexed (Nat(..))

data Vec n a where
  VNil :: Vec Zero a
  VCons :: a -> Vec n a -> Vec (Succ n) a

replicateVec :: SNat n -> a -> Vec n a
replicateVec :: SNat n -> a -> Vec n a
replicateVec SNat n
SZero a
_     = Vec n a
forall a. Vec 'Zero a
VNil
replicateVec (SSucc SNat n
n) a
x = a -> Vec n a -> Vec ('Succ n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons a
x (SNat n -> a -> Vec n a
forall (n :: Nat) a. SNat n -> a -> Vec n a
replicateVec SNat n
n a
x)

zipWithVec :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWithVec :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWithVec a -> b -> c
_ Vec n a
VNil         Vec n b
VNil         = Vec n c
forall a. Vec 'Zero a
VNil
zipWithVec a -> b -> c
f (VCons a
x Vec n a
xs) (VCons b
y Vec n b
ys) = c -> Vec n c -> Vec ('Succ n) c
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons (a -> b -> c
f a
x b
y) ((a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWithVec a -> b -> c
f Vec n a
xs Vec n b
Vec n b
ys)

data SNat (n :: Nat) where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)

class SingNat (n :: Nat) where sing :: SNat n
instance SingNat Zero where sing :: SNat 'Zero
sing = SNat 'Zero
SZero
instance SingNat n => SingNat (Succ n) where sing :: SNat ('Succ n)
sing = SNat n -> SNat ('Succ n)
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat n
forall (n :: Nat). SingNat n => SNat n
sing