{-# 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

-- | Nat-indexed list, where the nat determines the length.
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

-- | A kind of fmap for Vect.
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)

-- | VCons to the end of a Vect.
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)

-- | Show a Vect.
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

-- | Drop the length index from a Vect, giving a typical list.
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

-- | Used to implement listToVect through natRecursion.
newtype MaybeVect a n = MV {
    MaybeVect a n -> Maybe (Vect n a)
unMV :: Maybe (Vect n a)
  }

-- | Try to produce a Vect from a list. The nat index must be fixed somehow,
--   perhaps with the help of ScopedTypeVariables.
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