module Data.BoundedList

import Data.Fin

%access public export
%default total

||| A list with an upper bound on its length.
data BoundedList : Nat -> Type -> Type where
  Nil : BoundedList n a
  (::) : a -> BoundedList n a -> BoundedList (S n) a

||| Compute the length of a list.
length : BoundedList n a -> Fin (S n)
length [] = FZ
length (x :: xs) = FS (length xs)

--------------------------------------------------------------------------------
-- Indexing into bounded lists
--------------------------------------------------------------------------------

index : Fin (S n) -> BoundedList n a -> Maybe a
index _      []        = Nothing
index FZ     (x :: _)  = Just x
index (FS f) (_ :: xs) = index f xs

--------------------------------------------------------------------------------
-- Adjusting bounds
--------------------------------------------------------------------------------

||| Loosen the bounds on a list's length.
weaken : BoundedList n a -> BoundedList (n + m) a
weaken []        = []
weaken (x :: xs) = x :: weaken xs

--------------------------------------------------------------------------------
-- Conversions to and from list
--------------------------------------------------------------------------------

take : (n : Nat) -> List a -> BoundedList n a
take _ [] = []
take Z _ = []
take (S n') (x :: xs) = x :: take n' xs

toList : BoundedList n a -> List a
toList [] = []
toList (x :: xs) = x :: Data.BoundedList.toList xs

fromList : (xs : List a) -> BoundedList (length xs) a
fromList [] = []
fromList (x :: xs) = x :: fromList xs

--------------------------------------------------------------------------------
-- Building (bigger) bounded lists
--------------------------------------------------------------------------------

replicate : (n : Nat) -> a -> BoundedList n a
replicate Z _ = []
replicate (S n) x = x :: replicate n x

--------------------------------------------------------------------------------
-- Folds
--------------------------------------------------------------------------------

implementation Foldable (BoundedList n) where
  foldr f e []      = e
  foldr f e (x::xs) = f x (foldr f e xs)
  foldl f e []      = e
  foldl f e (x::xs) = foldl f (f e x) xs

--------------------------------------------------------------------------------
-- Maps
--------------------------------------------------------------------------------

implementation Functor (BoundedList n) where
  map f [] = []
  map f (x :: xs) = f x :: map f xs

--------------------------------------------------------------------------------
-- Misc
--------------------------------------------------------------------------------

||| Extend a bounded list to the maximum size by padding on the left.
pad : BoundedList n a -> a -> BoundedList n a
pad {n=Z}    []        _       = []
pad {n=S n'} []        padding = padding :: (pad {n=n'} [] padding)
pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding


--------------------------------------------------------------------------------
-- Simple properties
--------------------------------------------------------------------------------

zeroBoundIsEmpty : (xs : BoundedList 0 a) -> xs = the (BoundedList 0 a) []
zeroBoundIsEmpty [] = Refl
zeroBoundIsEmpty (_ :: _) impossible