{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
module Utils.Vec (
module Utils.Vec
, module Utils.Peano
) where
import Prelude hiding (pred)
import Utils.Peano
import Data.Monoid ((<>))
data Vec n a where
Nil :: Vec Z a
(:.) :: a -> Vec n a -> Vec (S n) a
infixr 4 :.
instance Eq a => Eq (Vec n a) where
Nil == Nil = True
(x :. xs) == (y :. ys) = x == y && xs == ys
instance Functor (Vec n) where
fmap _ Nil = Nil
fmap f (x:.xs) = f x :. fmap f xs
instance Foldable (Vec n) where
foldMap _ Nil = mempty
foldMap f (x:.xs) = f x <> foldMap f xs
instance Show a => Show (Vec n a) where
show = show . list
list :: Vec n a -> [a]
list = foldr (:) []
vec :: SNat n -> [a] -> Vec n a
vec SZ [] = Nil
vec (SS n) (x:xs) = x :. (vec n xs)
vec _ _ = error "Given SNat is different than the length of the given list."
$(derivePeanoAliases 100)