||| A Zipper implementation for Lists
||| inspired by
||| https://hackage.haskell.org/package/ListZipper-1.2.0.2/docs/src/Data-List-Zipper.html
module Data.List.Zipper

%default total
%access public export

||| A Zipper for Lists
data Zipper: Type -> Type where
  Zip: List a -> List a -> Zipper a

%name Zipper z1, z2

-- Implementations
--------------------------------------------------------------------------------

Functor Zipper where
  map f (Zip xs ys) = Zip (map f xs) (map f ys)

Foldable Zipper where
  foldr f acc (Zip xs ys) = foldr f acc (reverse xs ++ ys)

Show a => Show (Zipper a) where
  show (Zip xs []) = show $ reverse xs
  show (Zip xs (x :: ys)) = unwords [show $ reverse xs, "-", show x, "-", show ys]

||| Equality for Zippers
||| Two zipper are equal if they zip the same list and point to the same cursor
Eq a => Eq (Zipper a) where
  (==) (Zip xs ys) (Zip zs ws) = (xs == zs) && (ys == ws)
-- Functions
--------------------------------------------------------------------------------

||| creates an empty Zipper
||| ```idris example
||| empty {a = Nat}
||| ```
empty: Zipper a
empty = Zip [] []

||| checks whether this Zipper is empty
||| ```idris example
||| isEmpty empty {a = Nat}
||| ```
isEmpty: Zipper a -> Bool
isEmpty (Zip [] []) = True
isEmpty _ = False

||| creates a Zipper from a List
||| ```idris example
||| show $ fromList [1,2,3,4,5]
||| ```
fromList: List a -> Zipper a
fromList xs = Zip [] xs

||| moves the cursor to the right or leaves the cursor unchanged
||| ```idris example
|||  show $ right $ fromList [1,2,3,4,5]
||| ```
right: Zipper a -> Zipper a
right (Zip xs (x :: ys)) = Zip (x :: xs) ys
right z = z

||| moves the cursor to the left or leaves the cursor unchanged
||| ```idris example
||| show $ left $ fromList [1,2,3,4,5]
||| ```
left: Zipper a -> Zipper a
left (Zip (x :: xs) ys) = Zip xs (x :: ys)
left z = z

||| gets the element at the current cursor
||| ```idris example
||| cursor $ fromList [1,2,3,4,5]
||| ```
cursor: Zipper a -> Maybe a
cursor (Zip xs ys) = listToMaybe ys

||| move the cursor to the start of the Zipper
||| ```idris example
||| show $ start $ fromList [1,2,3,4,5]
||| ```
start: Zipper a -> Zipper a
start (Zip xs ys) = Zip [] (reverse xs ++ ys)

||| move the cursor to the end of the Zipper
||| ```idris example
||| show $ end $ fromList [1,2,3,4,5]
||| ```
end: Zipper a -> Zipper a
end (Zip xs ys) = Zip (reverse ys ++ xs) []

||| checks whether the cursor is at the start of the Zipper
||| ```idris example
||| startp $ fromList [1,2,3,4,5]
||| ```
startp: Zipper a -> Bool
startp (Zip [] ys) = True
startp _ = False

||| checks whether the cursor is at the end of the Zipper
||| ```idris example
||| endp $ fromList [1,2,3,4,5]
||| ```
endp: Zipper a -> Bool
endp (Zip xs []) = True
endp _ = False

||| inserts an element at the current cursor
||| ```idris example
||| show $ insert 0 $ fromList [1,2,3,4,5]
||| ```
insert: a -> Zipper a -> Zipper a
insert x (Zip xs ys) = Zip xs (x :: ys)

||| push an element into the Zipper and move the cursor past it
||| ```idris example
||| show $ push 0 $ fromList [1,2,3,4,5]
||| ```
push: a -> Zipper a -> Zipper a
push x (Zip xs ys) = Zip (x :: xs) (ys)

||| pop an element from the Zipper
||| ```idris example
||| show $ pop $ right $ fromList [1,2,3,4,5]
||| ```
pop: Zipper a -> Zipper a
pop (Zip (_ :: xs) ys) = Zip xs ys
pop z = z

||| delete the element at the current cursor
||| ```idris example
||| show $ Data.List.Zipper.delete $ fromList [1,2,3,4,5]
||| ```
delete: Zipper a -> Zipper a
delete (Zip xs (x :: ys)) = Zip xs ys
delete z = z

||| remove an element from the zipper
||| ```idris example
||| show $ replace 9 $ fromList[1,2,3,4,5]
||| ```
replace: a -> Zipper a -> Zipper a
replace x (Zip xs (_ :: ys)) = Zip xs (x :: ys)
replace _ z1 = z1

||| Return the index of the current cursor
||| ```idris example
||| index $ fromList [1,2,3,4,5]
||| ```
index: Zipper a -> Nat
index (Zip xs ys) = length xs

||| convert this Zipper to a list
||| ```idris example
||| toList $ fromList[1,2,3,4,5]
||| ```
toList: Zipper a -> List a
toList (Zip xs ys) = reverse xs ++ ys