non-empty vectors

NEVect.idr

module Data.NEVect

import public Data.Fin

%access public export
%default total

||| Non-zero natural numbers: upper unbounded, unsigned integers that are
||| greater than one.
data NZNat : Type where
  One : NZNat
  S   : NZNat -> NZNat

||| Convert a NZNat to Nat.
toNat : NZNat -> Nat
toNat One = 1
toNat (S n) = 1 + toNat n

infixr 7 ::

||| Non-empty vectors: Generic lists with at least one element and explicit length.
||| @ len the length of the list
||| @ elem the type of elements
data NEVect : (len : NZNat) -> (elem : Type) -> Type where
  End  : a -> NEVect One a
  (::) : a -> NEVect n a -> NEVect (S n) a

-- Hints for interactive editing
%name NEVect xs,ys,zs,ws

--------------------------------------------------------------------------------
-- Length
--------------------------------------------------------------------------------

||| Calculate the length of a `NEVect`.
|||
||| **Note**: this is only useful if you don't already statically know the length
||| and you want to avoid matching the implicit argument for erasure reasons.
||| @ len the length (provably equal to the return value)
||| @ xs the non-empty vector
length : (xs : NEVect len elem) -> Nat
length (End x) = 1
length (x::xs) = 1 + length xs
||| Show that the length function on non-empty vectors in fact calculates the length
private lengthCorrect : (len : NZNat) -> (xs : NEVect len elem) -> length xs = toNat len
lengthCorrect One (End _)     = Refl
lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl

--------------------------------------------------------------------------------
-- Indexing into non-empty vectors
--------------------------------------------------------------------------------
||| All but the first element of the non-empty vector
tail : NEVect (S len) elem -> NEVect len elem
tail (_::xs) = xs

||| Only the first element of the non-empty vector
head : NEVect (S len) elem -> elem
head (x::_) = x

||| The last element of the non-empty vector
last : NEVect len elem -> elem
last (End x) = x
last (x::xs) = last xs