{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}

-----------------------------------------------------------------------------
{-|
Module      : Math.Tensor.Safe.Vector
Description : Length-typed vector.
Copyright   : (c) Nils Alex, 2020
License     : MIT
Maintainer  : nils.alex@fau.de

Length-typed vector.
-}
-----------------------------------------------------------------------------
module Math.Tensor.Safe.Vector
  ( Vec(..)
  , vecFromListUnsafe
  ) where

import Math.Tensor.Safe.TH

import Data.Kind (Type)
import Data.Singletons (Sing)

import Control.DeepSeq (NFData(rnf))

data Vec :: N -> Type -> Type where
    VNil :: Vec 'Z a
    VCons :: a -> Vec n a -> Vec ('S n) a

deriving instance Show a => Show (Vec n a)

instance NFData a => NFData (Vec n a) where
    rnf :: Vec n a -> ()
rnf Vec n a
VNil         = ()
    rnf (VCons a
x Vec n a
xs) = a -> ()
forall a. NFData a => a -> ()
rnf a
x () -> () -> ()
`seq` Vec n a -> ()
forall a. NFData a => a -> ()
rnf Vec n a
xs

instance Eq a => Eq (Vec n a) where
  Vec n a
VNil           == :: Vec n a -> Vec n a -> Bool
== Vec n a
VNil           = Bool
True
  (a
x `VCons` Vec n a
xs) == (a
y `VCons` Vec n a
ys) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y Bool -> Bool -> Bool
&& Vec n a
xs Vec n a -> Vec n a -> Bool
forall a. Eq a => a -> a -> Bool
== Vec n a
Vec n a
ys

instance Ord a => Ord (Vec n a) where
  Vec n a
VNil compare :: Vec n a -> Vec n a -> Ordering
`compare` Vec n a
VNil = Ordering
EQ
  (a
x `VCons` Vec n a
xs) `compare` (a
y `VCons` Vec n a
ys) =
    case a
x a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
y of
      Ordering
LT -> Ordering
LT
      Ordering
EQ -> Vec n a
xs Vec n a -> Vec n a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Vec n a
Vec n a
ys
      Ordering
GT -> Ordering
GT

vecFromListUnsafe :: forall (n :: N) a.
                     Sing n -> [a] -> Vec n a
vecFromListUnsafe :: Sing n -> [a] -> Vec n a
vecFromListUnsafe Sing n
SZ [] = Vec n a
forall a. Vec 'Z a
VNil
vecFromListUnsafe (SS sn) (a
x:[a]
xs) =
    let xs' :: Vec n a
xs' = Sing n -> [a] -> Vec n a
forall (n :: N) a. Sing n -> [a] -> Vec n a
vecFromListUnsafe Sing n
sn [a]
xs
    in  a
x a -> Vec n a -> Vec ('S n) a
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec n a
xs'
vecFromListUnsafe Sing n
_ [a]
_ = String -> Vec n a
forall a. HasCallStack => String -> a
error String
"cannot reconstruct vector from list: incompatible lengths"