    {-# LANGUAGE DeriveDataTypeable #-}

    -- | Nonempty lists.

    module Agda.Utils.NonemptyList where

    import Control.Monad

    import Data.Data (Data)
    import Data.Foldable (Foldable)
      -- The toList method of Foldable may do something stupid,
      -- like traversing the list just to build a list again.
    import Data.Traversable (Traversable)
    import Data.Maybe
    import Data.Semigroup
    import qualified Data.List as List

    infixr 5 :!
    data NonemptyList a = (:!) { headNe :: a, tailNe :: [a] }
      deriving (Eq, Ord, Functor, Foldable, Traversable, Data)

    instance Semigroup (NonemptyList a) where
      (x :! xs) <> (y :! ys) = x :! xs ++ y : ys

    instance Applicative NonemptyList where
      pure x = x :! []
      (<*>) = ap

    instance Monad NonemptyList where
      return = pure
      (x :! xs) >>= f = foldr1 (<>) (f x : map f xs)

    instance Show a => Show (NonemptyList a) where
      showsPrec _ = showList . toList

    -- | Implementing conversion to list manually, since @Foldable.toList@
    --   might recurse over the tail and, thus, destroy sharing.
    toList :: NonemptyList a -> [a]
    toList (x :! xs) = x : xs

    -- | Converting a list (safe).
    fromList :: [a] -> Maybe (NonemptyList a)
    fromList []       = Nothing
    fromList (x : xs) = Just $ x :! xs

    -- | Prepending an element.
    consNe :: a -> NonemptyList a -> NonemptyList a
    consNe x (y :! zs) = x :! (y : zs)

    -- | Returns the union of the argument lists seen as sets. The order of the
    --   elements in the result is not specified. Precondition: arguments contain
    --   no duplicates.
    unionNe :: Eq a => NonemptyList a -> NonemptyList a -> NonemptyList a
    unionNe (x :! xs) (y :! ys) = z :! zs
      where z : zs = List.union (x : xs) (y : ys)

    -- | Zip two nonempty lists.
    zipWithNe :: (a -> b -> c) -> NonemptyList a -> NonemptyList b -> NonemptyList c
    zipWithNe f (x :! xs) (y :! ys) = f x y :! zipWith f xs ys

    -- | Zip two nonempty lists.
    zipNe :: NonemptyList a -> NonemptyList b -> NonemptyList (a, b)
    zipNe = zipWithNe (,)

    -- | Case on a list, getting a nonempty list in the cons case.
    caseListNe :: [a] -> b -> (NonemptyList a -> b) -> b
    caseListNe []       e ne = e
    caseListNe (x : xs) e ne = ne (x :! xs)

    -- | Case on a list, with list last.
    listCaseNe :: b -> (NonemptyList a -> b) -> [a] -> b
    listCaseNe e ne xs = caseListNe xs e ne

    -- | Check if an element is present in a list.
    elemNe :: Eq a => a -> NonemptyList a -> Bool
    elemNe y (x :! xs) = elem y (x : xs)