{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
module Data.TypeNat.Vect (
Vect(..)
, vectMap
, vectSnoc
, vectToList
, listToVect
, showVect
, module Data.TypeNat.Nat
) where
import Data.TypeNat.Nat
data Vect :: Nat -> * -> * where
VNil :: Vect Z a
VCons :: a -> Vect n a -> Vect (S n) a
deriving instance Eq a => Eq (Vect n a)
deriving instance Show a => Show (Vect n a)
instance Functor (Vect n) where
fmap :: (a -> b) -> Vect n a -> Vect n b
fmap = (a -> b) -> Vect n a -> Vect n b
forall a b (n :: Nat). (a -> b) -> Vect n a -> Vect n b
vectMap
instance Foldable (Vect n) where
foldr :: (a -> b -> b) -> b -> Vect n a -> b
foldr a -> b -> b
f b
b Vect n a
vect = case Vect n a
vect of
Vect n a
VNil -> b
b
VCons a
x Vect n a
rest -> a -> b -> b
f a
x ((a -> b -> b) -> b -> Vect n a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f b
b Vect n a
rest)
instance Traversable (Vect n) where
traverse :: (a -> f b) -> Vect n a -> f (Vect n b)
traverse a -> f b
f Vect n a
vect = case Vect n a
vect of
Vect n a
VNil -> Vect 'Z b -> f (Vect 'Z b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vect 'Z b
forall a. Vect 'Z a
VNil
VCons a
x Vect n a
rest -> b -> Vect n b -> Vect ('S n) b
forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a
VCons (b -> Vect n b -> Vect ('S n) b)
-> f b -> f (Vect n b -> Vect ('S n) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x f (Vect n b -> Vect ('S n) b) -> f (Vect n b) -> f (Vect ('S n) b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b) -> Vect n a -> f (Vect n b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f Vect n a
rest
vectMap :: (a -> b) -> Vect n a -> Vect n b
vectMap :: (a -> b) -> Vect n a -> Vect n b
vectMap a -> b
f Vect n a
vect = case Vect n a
vect of
Vect n a
VNil -> Vect n b
forall a. Vect 'Z a
VNil
VCons a
x Vect n a
v -> b -> Vect n b -> Vect ('S n) b
forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a
VCons (a -> b
f a
x) ((a -> b) -> Vect n a -> Vect n b
forall a b (n :: Nat). (a -> b) -> Vect n a -> Vect n b
vectMap a -> b
f Vect n a
v)
vectSnoc :: a -> Vect n a -> Vect (S n) a
vectSnoc :: a -> Vect n a -> Vect ('S n) a
vectSnoc a
x Vect n a
vect = case Vect n a
vect of
Vect n a
VNil -> a -> Vect 'Z a -> Vect ('S 'Z) a
forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a
VCons a
x Vect 'Z a
forall a. Vect 'Z a
VNil
VCons a
y Vect n a
v -> a -> Vect ('S n) a -> Vect ('S ('S n)) a
forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a
VCons a
y (a -> Vect n a -> Vect ('S n) a
forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a
vectSnoc a
x Vect n a
v)
showVect :: Show a => Vect l a -> String
showVect :: Vect l a -> String
showVect Vect l a
VNil = String
"VNil"
showVect (VCons a
x Vect n a
xs) = a -> String
forall a. Show a => a -> String
show a
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" , " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Vect n a -> String
forall a (n :: Nat). Show a => Vect n a -> String
showVect Vect n a
xs
vectToList :: Vect n a -> [a]
vectToList :: Vect n a -> [a]
vectToList Vect n a
v = case Vect n a
v of
Vect n a
VNil -> []
VCons a
x Vect n a
xs -> a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Vect n a -> [a]
forall (n :: Nat) a. Vect n a -> [a]
vectToList Vect n a
xs
newtype MaybeVect a n = MV {
MaybeVect a n -> Maybe (Vect n a)
unMV :: Maybe (Vect n a)
}
listToVect:: IsNat n => [a] -> Maybe (Vect n a)
listToVect :: [a] -> Maybe (Vect n a)
listToVect = MaybeVect a n -> Maybe (Vect n a)
forall a (n :: Nat). MaybeVect a n -> Maybe (Vect n a)
unMV (MaybeVect a n -> Maybe (Vect n a))
-> ([a] -> MaybeVect a n) -> [a] -> Maybe (Vect n a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> MaybeVect a n
forall (n :: Nat) a. IsNat n => [a] -> MaybeVect a n
listToVect'
where
listToVect':: IsNat n => [a] -> MaybeVect a n
listToVect' :: [a] -> MaybeVect a n
listToVect' = (forall (m :: Nat). [a] -> MaybeVect a m -> MaybeVect a ('S m))
-> ([a] -> MaybeVect a 'Z) -> ([a] -> [a]) -> [a] -> MaybeVect a n
forall (n :: Nat) b (a :: Nat -> *).
IsNat n =>
(forall (m :: Nat). b -> a m -> a ('S m))
-> (b -> a 'Z) -> (b -> b) -> b -> a n
natRecursion forall a (m :: Nat). [a] -> MaybeVect a m -> MaybeVect a ('S m)
forall (m :: Nat). [a] -> MaybeVect a m -> MaybeVect a ('S m)
inductive [a] -> MaybeVect a 'Z
forall a. [a] -> MaybeVect a 'Z
base [a] -> [a]
forall a. [a] -> [a]
reduce
inductive :: [a] -> MaybeVect a m -> MaybeVect a (S m)
inductive :: [a] -> MaybeVect a m -> MaybeVect a ('S m)
inductive [a]
xs MaybeVect a m
maybeVect = case MaybeVect a m
maybeVect of
MV Maybe (Vect m a)
Nothing -> Maybe (Vect ('S m) a) -> MaybeVect a ('S m)
forall a (n :: Nat). Maybe (Vect n a) -> MaybeVect a n
MV Maybe (Vect ('S m) a)
forall a. Maybe a
Nothing
MV (Just Vect m a
vect) -> case [a]
xs of
[] -> Maybe (Vect ('S m) a) -> MaybeVect a ('S m)
forall a (n :: Nat). Maybe (Vect n a) -> MaybeVect a n
MV Maybe (Vect ('S m) a)
forall a. Maybe a
Nothing
(a
x : [a]
_) -> Maybe (Vect ('S m) a) -> MaybeVect a ('S m)
forall a (n :: Nat). Maybe (Vect n a) -> MaybeVect a n
MV (Vect ('S m) a -> Maybe (Vect ('S m) a)
forall a. a -> Maybe a
Just (a -> Vect m a -> Vect ('S m) a
forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a
VCons a
x Vect m a
vect))
base :: [a] -> MaybeVect a Z
base :: [a] -> MaybeVect a 'Z
base [a]
xs = case [a]
xs of
[] -> Maybe (Vect 'Z a) -> MaybeVect a 'Z
forall a (n :: Nat). Maybe (Vect n a) -> MaybeVect a n
MV (Vect 'Z a -> Maybe (Vect 'Z a)
forall a. a -> Maybe a
Just Vect 'Z a
forall a. Vect 'Z a
VNil)
[a]
_ -> Maybe (Vect 'Z a) -> MaybeVect a 'Z
forall a (n :: Nat). Maybe (Vect n a) -> MaybeVect a n
MV Maybe (Vect 'Z a)
forall a. Maybe a
Nothing
reduce :: [a] -> [a]
reduce :: [a] -> [a]
reduce [a]
xs = case [a]
xs of
[] -> []
(a
x : [a]
xs) -> [a]
xs