module Haskell.Data.List.NonEmpty where

open import Haskell.Prelude
  hiding (NonEmpty; head; tail; toList; init; last)

open import Haskell.Data.Foldable1 using (Foldable1)

infixr  _:|_ _<|_

--------------------------------------------------------------------------------

record NonEmpty (a : Type) : Type where
  no-eta-equality
  pattern
  constructor _:|_
  field
    head : a
    tail : List a

open NonEmpty public

toList : {a : Type} → NonEmpty a → List a
toList xs = head xs List.∷ tail xs

_<|_ : {a : Type} → a → NonEmpty a → NonEmpty a
x <| xs = x :| head xs List.∷ tail xs

cons = _<|_

singleton : {a : Type} → a → NonEmpty a
singleton x = x :| []

init : {a : Type} → NonEmpty a → List a
init = λ xs → helper (head xs) (tail xs)
  module Init where
    helper : {a : Type} → a → List a → List a
    helper x [] = []
    helper x (y List.∷ xs) = x List.∷ helper y xs

last : {a : Type} → NonEmpty a → a
last = λ xs → helper (head xs) (tail xs)
  module Last where
    helper : {a : Type} → a → List a → a
    helper x [] = x
    helper _ (y List.∷ xs) = helper y xs

--------------------------------------------------------------------------------

private
  bindNonEmpty : ∀ {a b} → NonEmpty a → (a → NonEmpty b) → NonEmpty b
  bindNonEmpty xs f = head fx :| tail fx ++ fxs
    where
      fx = f (head xs)
      fxs = tail xs >>= (toList ∘ f)

instance

  iFunctorNonEmpty : Functor NonEmpty
  iFunctorNonEmpty .fmap f xs = f (head xs) :| fmap f (tail xs)
  iFunctorNonEmpty ._<$_ b xs = b ⦃ head xs ⦄ :| (b <$ tail xs)

  iDefaultApplicativeNonEmpty : DefaultApplicative NonEmpty
  iDefaultApplicativeNonEmpty .DefaultApplicative.pure x = x :| []
  iDefaultApplicativeNonEmpty .DefaultApplicative._<*>_ fs xs =
    bindNonEmpty fs λ f → bindNonEmpty xs λ x → f x :| []

  iApplicativeNonEmpty : Applicative NonEmpty
  iApplicativeNonEmpty = record {DefaultApplicative iDefaultApplicativeNonEmpty}

  iDefaultMonadNonEmpty : DefaultMonad NonEmpty
  iDefaultMonadNonEmpty .DefaultMonad._>>=_ = bindNonEmpty

  iMonadNonEmpty : Monad NonEmpty
  iMonadNonEmpty = record {DefaultMonad iDefaultMonadNonEmpty}

  iSemigroupNonEmpty : ∀ {a} → Semigroup (NonEmpty a)
  iSemigroupNonEmpty ._<>_ (x :| xs) ys = x :| xs ++ toList ys

  iDefaultFoldableNonEmpty : DefaultFoldable NonEmpty
  iDefaultFoldableNonEmpty .DefaultFoldable.foldMap f (x :| xs) = f x <> foldMap f xs

  iFoldableNonEmpty : Foldable NonEmpty
  iFoldableNonEmpty = record {DefaultFoldable iDefaultFoldableNonEmpty}

  iFoldable1NonEmpty : Foldable1 NonEmpty
  iFoldable1NonEmpty .Foldable1.foldMap1 f (x :| xs) = go (f x) xs
    where
      go : _ → List _ → _
      go y [] = y
      go y (x List.∷ xs) = y <> go (f x) xs