    {-# LANGUAGE CPP #-}

    -- | Non-empty lists.
    --
    --   Better name @List1@ for non-empty lists, plus missing functionality.
    --
    --   Import:
    --   @
    --
    --     {-# LANGUAGE PatternSynonyms #-}
    --
    --     import           Agda.Utils.List1 (List1, pattern (:|))
    --     import qualified Agda.Utils.List1 as List1
    --
    --   @

    {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
      -- because of https://gitlab.haskell.org/ghc/ghc/issues/10339

    module Agda.Utils.List1
      ( module Agda.Utils.List1
      , module List1
      ) where

    import Prelude hiding (filter)

    import Control.Arrow ((&&&))
    import Control.Monad (filterM)
    import qualified Control.Monad as List (zipWithM, zipWithM_)

    import qualified Data.Either as Either
    import qualified Data.List as List
    import qualified Data.Maybe as Maybe
    import qualified Data.Semigroup as Semigroup

    import qualified Data.List.NonEmpty (NonEmpty)
    import Data.List.NonEmpty as List1 hiding (NonEmpty)

    import Agda.Utils.Functor ((<.>))
    import Agda.Utils.Null (Null(..))
    import qualified Agda.Utils.List as List

    type List1 = Data.List.NonEmpty.NonEmpty

    -- | Return the last element and the rest.

    initLast :: List1 a -> ([a], a)
    initLast :: forall a. List1 a -> ([a], a)
    initLast = NonEmpty a -> [a]
    forall a. NonEmpty a -> [a]
    List1.init (NonEmpty a -> [a]) -> (NonEmpty a -> a) -> NonEmpty a -> ([a], a)
    forall (a :: * -> * -> *) b c c'.
    Arrow a =>
    a b c -> a b c' -> a b (c, c')
    &&& NonEmpty a -> a
    forall a. NonEmpty a -> a
    List1.last
      -- traverses twice, but does not create intermediate pairs

    -- | Build a list with one element.

    #if !(MIN_VERSION_base(4,15,0))
    singleton :: a -> List1 a
    singleton = (:| [])
    #endif

    #if !MIN_VERSION_base(4,16,0)
    -- | Append a list to a non-empty list.

    appendList :: List1 a -> [a] -> List1 a
    appendList :: forall a. List1 a -> [a] -> List1 a
    appendList (a
    x :| [a]
    xs) [a]
    ys = a
    x a -> [a] -> NonEmpty a
    forall a. a -> [a] -> NonEmpty a
    :| [a] -> [a] -> [a]
    forall a. Monoid a => a -> a -> a
    mappend [a]
    xs [a]
    ys

    -- | Prepend a list to a non-empty list.

    prependList :: [a] -> List1 a -> List1 a
    prependList :: forall a. [a] -> List1 a -> List1 a
    prependList [a]
    as List1 a
    bs = (a -> List1 a -> List1 a) -> List1 a -> [a] -> List1 a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr a -> List1 a -> List1 a
    forall a. a -> NonEmpty a -> NonEmpty a
    (<|) List1 a
    bs [a]
    as
    #endif

    -- | More precise type for @snoc@.

    snoc :: [a] -> a -> List1 a
    snoc :: forall a. [a] -> a -> List1 a
    snoc [a]
    as a
    a = [a] -> List1 a -> List1 a
    forall a. [a] -> List1 a -> List1 a
    prependList [a]
    as (List1 a -> List1 a) -> List1 a -> List1 a
    forall a b. (a -> b) -> a -> b
    $ a
    a a -> [a] -> List1 a
    forall a. a -> [a] -> NonEmpty a
    :| []

    -- | More precise type for 'Agda.Utils.List.groupBy''.
    --
    -- A variant of 'List.groupBy' which applies the predicate to consecutive
    -- pairs.
    -- O(n).
    groupBy' :: forall a. (a -> a -> Bool) -> [a] -> [List1 a]
    groupBy' :: forall a. (a -> a -> Bool) -> [a] -> [List1 a]
    groupBy' a -> a -> Bool
    _ []           = []
    groupBy' a -> a -> Bool
    p xxs :: [a]
    xxs@(a
    x : [a]
    xs) = a -> [(Bool, a)] -> [List1 a]
    grp a
    x ([(Bool, a)] -> [List1 a]) -> [(Bool, a)] -> [List1 a]
    forall a b. (a -> b) -> a -> b
    $ (a -> a -> (Bool, a)) -> [a] -> [a] -> [(Bool, a)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    List.zipWith (\ a
    x a
    y -> (a -> a -> Bool
    p a
    x a
    y, a
    y)) [a]
    xxs [a]
    xs
      where
      grp :: a -> [(Bool,a)] -> [List1 a]
      grp :: a -> [(Bool, a)] -> [List1 a]
    grp a
    x [(Bool, a)]
    ys
        | let ([(Bool, a)]
    xs, [(Bool, a)]
    rest) = ((Bool, a) -> Bool) -> [(Bool, a)] -> ([(Bool, a)], [(Bool, a)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.span (Bool, a) -> Bool
    forall a b. (a, b) -> a
    fst [(Bool, a)]
    ys
        = (a
    x a -> [a] -> List1 a
    forall a. a -> [a] -> NonEmpty a
    :| ((Bool, a) -> a) -> [(Bool, a)] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    List.map (Bool, a) -> a
    forall a b. (a, b) -> b
    snd [(Bool, a)]
    xs) List1 a -> [List1 a] -> [List1 a]
    forall a. a -> [a] -> [a]
    : case [(Bool, a)]
    rest of
          []                 -> []
          ((Bool
    _false, a
    z) : [(Bool, a)]
    zs) -> a -> [(Bool, a)] -> [List1 a]
    grp a
    z [(Bool, a)]
    zs

    -- | Breaks a list just /after/ an element satisfying the predicate is
    --   found.
    --
    --   >>> breakAfter even [1,3,5,2,4,7,8]
    --   ([1,3,5,2],[4,7,8])

    breakAfter :: (a -> Bool) -> List1 a -> (List1 a, [a])
    breakAfter :: forall a. (a -> Bool) -> List1 a -> (List1 a, [a])
    breakAfter a -> Bool
    p (a
    x :| [a]
    xs) = (a -> Bool) -> a -> [a] -> (NonEmpty a, [a])
    forall a. (a -> Bool) -> a -> [a] -> (List1 a, [a])
    List.breakAfter1 a -> Bool
    p a
    x [a]
    xs

    -- | Concatenate one or more non-empty lists.

    concat :: [List1 a] -> [a]
    concat :: forall a. [List1 a] -> [a]
    concat = (NonEmpty a -> [a]) -> [NonEmpty a] -> [a]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap NonEmpty a -> [a]
    forall a. NonEmpty a -> [a]
    toList

    -- | Like 'Data.List.union'.  Duplicates in the first list are not removed.
    -- O(nm).
    union :: Eq a => List1 a -> List1 a -> List1 a
    union :: forall a. Eq a => List1 a -> List1 a -> List1 a
    union (a
    a :| [a]
    as) NonEmpty a
    bs = a
    a a -> [a] -> NonEmpty a
    forall a. a -> [a] -> NonEmpty a
    :| [a] -> [a] -> [a]
    forall a. Eq a => [a] -> [a] -> [a]
    List.union [a]
    as ((a -> Bool) -> NonEmpty a -> [a]
    forall a. (a -> Bool) -> NonEmpty a -> [a]
    filter (a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    a) NonEmpty a
    bs)

    -- * Recovering non-emptyness.

    ifNull :: [a] -> b -> (List1 a -> b) -> b
    ifNull :: forall a b. [a] -> b -> (List1 a -> b) -> b
    ifNull []       b
    b List1 a -> b
    _ = b
    b
    ifNull (a
    a : [a]
    as) b
    _ List1 a -> b
    f = List1 a -> b
    f (List1 a -> b) -> List1 a -> b
    forall a b. (a -> b) -> a -> b
    $ a
    a a -> [a] -> List1 a
    forall a. a -> [a] -> NonEmpty a
    :| [a]
    as

    ifNotNull :: [a] -> (List1 a -> b) -> b -> b
    ifNotNull :: forall a b. [a] -> (List1 a -> b) -> b -> b
    ifNotNull []       List1 a -> b
    _ b
    b = b
    b
    ifNotNull (a
    a : [a]
    as) List1 a -> b
    f b
    _ = List1 a -> b
    f (List1 a -> b) -> List1 a -> b
    forall a b. (a -> b) -> a -> b
    $ a
    a a -> [a] -> List1 a
    forall a. a -> [a] -> NonEmpty a
    :| [a]
    as

    unlessNull :: Null m => [a] -> (List1 a -> m) -> m
    unlessNull :: forall m a. Null m => [a] -> (List1 a -> m) -> m
    unlessNull []       List1 a -> m
    _ = m
    forall a. Null a => a
    empty
    unlessNull (a
    x : [a]
    xs) List1 a -> m
    f = List1 a -> m
    f (List1 a -> m) -> List1 a -> m
    forall a b. (a -> b) -> a -> b
    $ a
    x a -> [a] -> List1 a
    forall a. a -> [a] -> NonEmpty a
    :| [a]
    xs

    -- * List functions with no special behavior for non-empty lists.

    -- | Checks if all the elements in the list are equal. Assumes that
    --   the 'Eq' instance stands for an equivalence relation.
    --   O(n).
    allEqual :: Eq a => List1 a -> Bool
    allEqual :: forall a. Eq a => List1 a -> Bool
    allEqual (a
    x :| [a]
    xs) = (a -> Bool) -> [a] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    x) [a]
    xs

    -- | Like 'Maybe.catMaybes'.

    catMaybes :: List1 (Maybe a) -> [a]
    catMaybes :: forall a. List1 (Maybe a) -> [a]
    catMaybes =  [Maybe a] -> [a]
    forall a. [Maybe a] -> [a]
    Maybe.catMaybes ([Maybe a] -> [a])
    -> (NonEmpty (Maybe a) -> [Maybe a]) -> NonEmpty (Maybe a) -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty (Maybe a) -> [Maybe a]
    forall a. NonEmpty a -> [a]
    List1.toList

    -- | Like 'List1.filter'.

    mapMaybe :: (a -> Maybe b) -> List1 a -> [b]
    mapMaybe :: forall a b. (a -> Maybe b) -> List1 a -> [b]
    mapMaybe a -> Maybe b
    f = (a -> Maybe b) -> [a] -> [b]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    Maybe.mapMaybe a -> Maybe b
    f ([a] -> [b]) -> (NonEmpty a -> [a]) -> NonEmpty a -> [b]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty a -> [a]
    forall a. NonEmpty a -> [a]
    List1.toList

    -- | Like 'Data.Either.partitionEithers'.

    partitionEithers :: List1 (Either a b) -> ([a], [b])
    partitionEithers :: forall a b. List1 (Either a b) -> ([a], [b])
    partitionEithers = [Either a b] -> ([a], [b])
    forall a b. [Either a b] -> ([a], [b])
    Either.partitionEithers ([Either a b] -> ([a], [b]))
    -> (NonEmpty (Either a b) -> [Either a b])
    -> NonEmpty (Either a b)
    -> ([a], [b])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty (Either a b) -> [Either a b]
    forall a. NonEmpty a -> [a]
    List1.toList

    -- | Like 'Data.Either.lefts'.

    lefts :: List1 (Either a b) -> [a]
    lefts :: forall a b. List1 (Either a b) -> [a]
    lefts = [Either a b] -> [a]
    forall a b. [Either a b] -> [a]
    Either.lefts  ([Either a b] -> [a])
    -> (NonEmpty (Either a b) -> [Either a b])
    -> NonEmpty (Either a b)
    -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty (Either a b) -> [Either a b]
    forall a. NonEmpty a -> [a]
    List1.toList

    -- | Like 'Data.Either.rights'.

    rights :: List1 (Either a b) -> [b]
    rights :: forall a b. List1 (Either a b) -> [b]
    rights = [Either a b] -> [b]
    forall a b. [Either a b] -> [b]
    Either.rights  ([Either a b] -> [b])
    -> (NonEmpty (Either a b) -> [Either a b])
    -> NonEmpty (Either a b)
    -> [b]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty (Either a b) -> [Either a b]
    forall a. NonEmpty a -> [a]
    List1.toList

    -- | Non-efficient, monadic 'nub'.
    -- O(n²).
    nubM :: Monad m => (a -> a -> m Bool) -> List1 a -> m (List1 a)
    nubM :: forall (m :: * -> *) a.
    Monad m =>
    (a -> a -> m Bool) -> List1 a -> m (List1 a)
    nubM a -> a -> m Bool
    eq (a
    a :| [a]
    as) = (a
    a a -> [a] -> NonEmpty a
    forall a. a -> [a] -> NonEmpty a
    :|) ([a] -> NonEmpty a) -> m [a] -> m (NonEmpty a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do (a -> a -> m Bool) -> [a] -> m [a]
    forall (m :: * -> *) a.
    Monad m =>
    (a -> a -> m Bool) -> [a] -> m [a]
    List.nubM a -> a -> m Bool
    eq ([a] -> m [a]) -> m [a] -> m [a]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (a -> m Bool) -> [a] -> m [a]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM (Bool -> Bool
    not (Bool -> Bool) -> (a -> m Bool) -> a -> m Bool
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> a -> a -> m Bool
    eq a
    a) [a]
    as

    -- | Like 'Control.Monad.zipWithM'.

    zipWithM :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c)
    zipWithM :: forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c)
    zipWithM a -> b -> m c
    f (a
    a :| [a]
    as) (b
    b :| [b]
    bs) = c -> [c] -> NonEmpty c
    forall a. a -> [a] -> NonEmpty a
    (:|) (c -> [c] -> NonEmpty c) -> m c -> m ([c] -> NonEmpty c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> b -> m c
    f a
    a b
    b m ([c] -> NonEmpty c) -> m [c] -> m (NonEmpty c)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (a -> b -> m c) -> [a] -> [b] -> m [c]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    List.zipWithM a -> b -> m c
    f [a]
    as [b]
    bs

    -- | Like 'Control.Monad.zipWithM'.

    zipWithM_ :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m ()
    zipWithM_ :: forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> List1 a -> List1 b -> m ()
    zipWithM_ a -> b -> m c
    f (a
    a :| [a]
    as) (b
    b :| [b]
    bs) = a -> b -> m c
    f a
    a b
    b m c -> m () -> m ()
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
    *> (a -> b -> m c) -> [a] -> [b] -> m ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    List.zipWithM_ a -> b -> m c
    f [a]
    as [b]
    bs