{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Utils.NonemptyList
( module Agda.Utils.NonemptyList
, toList ) where
import Control.Monad
import Data.Data (Data)
import Data.Foldable (Foldable, toList)
import Data.Traversable (Traversable)
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
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)
zipWithNe :: (a -> b -> c) -> NonemptyList a -> NonemptyList b -> NonemptyList c
zipWithNe f (x :! xs) (y :! ys) = f x y :! zipWith f xs ys
zipNe :: NonemptyList a -> NonemptyList b -> NonemptyList (a, b)
zipNe = zipWithNe (,)
caseListNe :: [a] -> b -> (NonemptyList a -> b) -> b
caseListNe [] e ne = e
caseListNe (x : xs) e ne = ne (x :! xs)
listCaseNe :: b -> (NonemptyList a -> b) -> [a] -> b
listCaseNe e ne xs = caseListNe xs e ne
elemNe :: Eq a => a -> NonemptyList a -> Bool
elemNe y (x :! xs) = elem y (x : xs)