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