    {-# 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
      , module IsList
      , module Unzip
      ) where

    import Prelude hiding (filter, unzip)

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

    import qualified Data.Either as Either
    import Data.Function ( on )
    import qualified Data.List as List
    import qualified Data.Maybe as Maybe

    import Data.List.NonEmpty as List1 hiding (fromList, toList, unzip)
    import qualified Data.List.NonEmpty as List1 (toList)

    -- Prevent warning -Wx-data-list-nonempty-unzip
    #if MIN_VERSION_base(4,19,0)
    import Data.Functor as Unzip (unzip)
    #else
    import Data.List.NonEmpty as Unzip (unzip)
    #endif

    import GHC.Exts as IsList ( IsList(..) )

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

    -- Set up doctest.
    -- $setup
    -- >>> :seti -XOverloadedLists

    type List1 = NonEmpty
    type String1 = List1 Char

    -- | Lossless 'toList', opposite of 'nonEmpty'.
    --
    toList' :: Maybe (List1 a) -> [a]
    toList' :: forall a. Maybe (List1 a) -> [a]
    toList' = [a] -> (List1 a -> [a]) -> Maybe (List1 a) -> [a]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] List1 a -> [a]
    List1 a -> [Item (List1 a)]
    forall l. IsList l => l -> [Item l]
    toList

    -- | Lift a function on non-empty lists to a function on lists.
    --
    -- This is in essence 'fmap' for 'Maybe', if we take @[a] = Maybe (List1 a)@.
    --
    liftList1 :: (List1 a -> List1 b) -> [a] -> [b]
    liftList1 :: forall a b. (List1 a -> List1 b) -> [a] -> [b]
    liftList1 List1 a -> List1 b
    f = Maybe (List1 b) -> [b]
    forall a. Maybe (List1 a) -> [a]
    toList' (Maybe (List1 b) -> [b]) -> ([a] -> Maybe (List1 b)) -> [a] -> [b]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (List1 a -> List1 b) -> Maybe (List1 a) -> Maybe (List1 b)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap List1 a -> List1 b
    f (Maybe (List1 a) -> Maybe (List1 b))
    -> ([a] -> Maybe (List1 a)) -> [a] -> Maybe (List1 b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [a] -> Maybe (List1 a)
    forall a. [a] -> Maybe (NonEmpty a)
    nonEmpty

    -- | Safe version of 'Data.List.NonEmpty.fromList'.

    fromListSafe
      :: List1 a  -- ^ Default value if convertee is empty.
      -> [a]      -- ^ List to convert, supposedly non-empty.
      -> List1 a  -- ^ Converted list.
    fromListSafe :: forall a. List1 a -> [a] -> List1 a
    fromListSafe List1 a
    err   [] = List1 a
    err
    fromListSafe List1 a
    _ (a
    x:[a]
    xs) = a
    x a -> [a] -> List1 a
    forall a. a -> [a] -> NonEmpty a
    :| [a]
    xs

    -- | Return the last element and the rest.

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

    -- | Last two elements (safe).
    --   O(n).
    last2 :: List1 a -> Maybe (a, a)
    last2 :: forall a. List1 a -> Maybe (a, a)
    last2 (a
    x :| a
    y : [a]
    xs) = (a, a) -> Maybe (a, a)
    forall a. a -> Maybe a
    Just ((a, a) -> Maybe (a, a)) -> (a, a) -> Maybe (a, a)
    forall a b. (a -> b) -> a -> b
    $ a -> a -> [a] -> (a, a)
    forall a. a -> a -> [a] -> (a, a)
    List.last2' a
    x a
    y [a]
    xs
    last2 NonEmpty a
    _ = Maybe (a, a)
    forall a. Maybe a
    Nothing

    -- | 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 (x :| xs) ys = x :| mappend xs ys

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

    prependList :: [a] -> List1 a -> List1 a
    prependList as bs = Prelude.foldr (<|) bs 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] -> NonEmpty a -> NonEmpty a
    forall a. [a] -> NonEmpty a -> NonEmpty a
    prependList [a]
    as (NonEmpty a -> NonEmpty a) -> NonEmpty a -> NonEmpty a
    forall a b. (a -> b) -> a -> b
    $ a
    a a -> [a] -> NonEmpty a
    forall a. a -> [a] -> NonEmpty a
    :| []

    -- | @'groupOn' f = 'groupBy' (('==') \`on\` f) '.' 'List.sortBy' ('compare' \`on\` f)@.
    -- O(n log n).
    groupOn :: Ord b => (a -> b) -> [a] -> [List1 a]
    groupOn :: forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
    groupOn a -> b
    f = (a -> a -> Bool) -> [a] -> [NonEmpty a]
    forall (f :: * -> *) a.
    Foldable f =>
    (a -> a -> Bool) -> f a -> [NonEmpty a]
    List1.groupBy (b -> b -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (b -> b -> Bool) -> (a -> b) -> a -> a -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` a -> b
    f) ([a] -> [NonEmpty a]) -> ([a] -> [a]) -> [a] -> [NonEmpty a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> a -> Ordering) -> [a] -> [a]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (b -> b -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (b -> b -> Ordering) -> (a -> b) -> a -> a -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` a -> b
    f)

    groupOn1 :: Ord b => (a -> b) -> List1 a -> List1 (List1 a)
    groupOn1 :: forall b a. Ord b => (a -> b) -> List1 a -> List1 (List1 a)
    groupOn1 a -> b
    f = (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
    forall a. (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
    List1.groupBy1 (b -> b -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (b -> b -> Bool) -> (a -> b) -> a -> a -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` a -> b
    f) (NonEmpty a -> NonEmpty (NonEmpty a))
    -> (NonEmpty a -> NonEmpty a)
    -> NonEmpty a
    -> NonEmpty (NonEmpty a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
    forall a. (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
    List1.sortBy (b -> b -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (b -> b -> Ordering) -> (a -> b) -> a -> a -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` a -> b
    f)

    -- | 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

    -- | Group consecutive items that share the same first component.
    --
    groupByFst :: forall a b. Eq a => [(a,b)] -> [(a, List1 b)]
    groupByFst :: forall a b. Eq a => [(a, b)] -> [(a, List1 b)]
    groupByFst =
        (NonEmpty (a, b) -> (a, List1 b))
    -> [NonEmpty (a, b)] -> [(a, List1 b)]
    forall a b. (a -> b) -> [a] -> [b]
    List.map (\ ((a
    tag, b
    b) :| [(a, b)]
    xs) -> (a
    tag, b
    b b -> [b] -> List1 b
    forall a. a -> [a] -> NonEmpty a
    :| ((a, b) -> b) -> [(a, b)] -> [b]
    forall a b. (a -> b) -> [a] -> [b]
    List.map (a, b) -> b
    forall a b. (a, b) -> b
    snd [(a, b)]
    xs))
          -- Float the grouping to the top level
      ([NonEmpty (a, b)] -> [(a, List1 b)])
    -> ([(a, b)] -> [NonEmpty (a, b)]) -> [(a, b)] -> [(a, List1 b)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((a, b) -> (a, b) -> Bool) -> [(a, b)] -> [NonEmpty (a, b)]
    forall (f :: * -> *) a.
    Foldable f =>
    (a -> a -> Bool) -> f a -> [NonEmpty a]
    List1.groupBy (a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (a -> a -> Bool) -> ((a, b) -> a) -> (a, b) -> (a, b) -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (a, b) -> a
    forall a b. (a, b) -> a
    fst)
          -- Group together characters in the same role.

    -- | Group consecutive items that share the same first component.
    --
    groupByFst1 :: forall a b. Eq a => List1 (a, b) -> List1 (a, List1 b)
    groupByFst1 :: forall a b. Eq a => List1 (a, b) -> List1 (a, List1 b)
    groupByFst1 =
        (NonEmpty (a, b) -> (a, List1 b))
    -> NonEmpty (NonEmpty (a, b)) -> NonEmpty (a, List1 b)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\ ((a
    tag, b
    b) :| [(a, b)]
    xs) -> (a
    tag, b
    b b -> [b] -> List1 b
    forall a. a -> [a] -> NonEmpty a
    :| ((a, b) -> b) -> [(a, b)] -> [b]
    forall a b. (a -> b) -> [a] -> [b]
    List.map (a, b) -> b
    forall a b. (a, b) -> b
    snd [(a, b)]
    xs))
          -- Float the grouping to the top level
      (NonEmpty (NonEmpty (a, b)) -> NonEmpty (a, List1 b))
    -> (NonEmpty (a, b) -> NonEmpty (NonEmpty (a, b)))
    -> NonEmpty (a, b)
    -> NonEmpty (a, List1 b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((a, b) -> (a, b) -> Bool)
    -> NonEmpty (a, b) -> NonEmpty (NonEmpty (a, b))
    forall a. (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
    List1.groupBy1 (a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (a -> a -> Bool) -> ((a, b) -> a) -> (a, b) -> (a, b) -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (a, b) -> a
    forall a b. (a, b) -> a
    fst)
          -- Group together characters in the same role.

    -- | Split a list into sublists. Generalisation of the prelude function
    --   @words@.
    --   Same as 'Data.List.Split.wordsBy' and 'Data.List.Extra.wordsBy',
    --   but with the non-emptyness guarantee on the chunks.
    --   O(n).
    --
    --   > words xs == wordsBy isSpace xs
    wordsBy :: (a -> Bool) -> [a] -> [List1 a]
    wordsBy :: forall a. (a -> Bool) -> [a] -> [List1 a]
    wordsBy a -> Bool
    p = [a] -> [NonEmpty a]
    loop
      where
      loop :: [a] -> [NonEmpty a]
    loop [a]
    as = case (a -> Bool) -> [a] -> [a]
    forall a. (a -> Bool) -> [a] -> [a]
    List.dropWhile a -> Bool
    p [a]
    as of
        []   -> []
        a
    x:[a]
    xs -> (a
    x a -> [a] -> NonEmpty a
    forall a. a -> [a] -> NonEmpty a
    :| [a]
    ys) NonEmpty a -> [NonEmpty a] -> [NonEmpty a]
    forall a. a -> [a] -> [a]
    : [a] -> [NonEmpty a]
    loop [a]
    zs where ([a]
    ys, [a]
    zs) = (a -> Bool) -> [a] -> ([a], [a])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.break a -> Bool
    p [a]
    xs

    -- | 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 = (List1 a -> [a]) -> [List1 a] -> [a]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap List1 a -> [a]
    List1 a -> [Item (List1 a)]
    forall l. IsList l => l -> [Item l]
    toList

    concatMap1 :: (a -> List1 b) -> List1 a -> List1 b
    concatMap1 :: forall a b. (a -> List1 b) -> List1 a -> List1 b
    concatMap1 = (a -> NonEmpty b) -> NonEmpty a -> NonEmpty b
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    (=<<)

    -- | 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

    -- | The more general type @Null m => [a] -> (List1 a -> m) -> m@
    --   often causes type inference to fail, as we do not in general have
    --   @instance Applicative m => Null (m ())@.
    unlessNull :: Applicative m => [a] -> (List1 a -> m ()) -> m ()
    unlessNull :: forall (m :: * -> *) a.
    Applicative m =>
    [a] -> (List1 a -> m ()) -> m ()
    unlessNull []       List1 a -> m ()
    _ = () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
    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

    unlessNullM :: Monad m => m [a] -> (List1 a -> m ()) -> m ()
    unlessNullM :: forall (m :: * -> *) a.
    Monad m =>
    m [a] -> (List1 a -> m ()) -> m ()
    unlessNullM m [a]
    m List1 a -> m ()
    k = m [a]
    m m [a] -> ([a] -> m ()) -> m ()
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= ([a] -> (List1 a -> m ()) -> m ()
    forall (m :: * -> *) a.
    Applicative m =>
    [a] -> (List1 a -> m ()) -> m ()
    `unlessNull` List1 a -> m ()
    k)

    -- * 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])
    -> (List1 (Maybe a) -> [Maybe a]) -> List1 (Maybe a) -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 (Maybe a) -> [Maybe a]
    forall a. NonEmpty a -> [a]
    List1.toList

    -- | Like 'Maybe.mapMaybe'.

    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]) -> (List1 a -> [a]) -> List1 a -> [b]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 a -> [a]
    forall a. NonEmpty a -> [a]
    List1.toList

    -- | Like 'List.find'.

    find :: (a -> Bool) -> List1 a -> Maybe a
    find :: forall a. (a -> Bool) -> List1 a -> Maybe a
    find a -> Bool
    f = (a -> Bool) -> [a] -> Maybe a
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find a -> Bool
    f ([a] -> Maybe a) -> (List1 a -> [a]) -> List1 a -> Maybe a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 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]))
    -> (List1 (Either a b) -> [Either a b])
    -> List1 (Either a b)
    -> ([a], [b])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 (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])
    -> (List1 (Either a b) -> [Either a b])
    -> List1 (Either a b)
    -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 (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])
    -> (List1 (Either a b) -> [Either a b])
    -> List1 (Either a b)
    -> [b]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 (Either a b) -> [Either a b]
    forall a. NonEmpty a -> [a]
    List1.toList

    -- | Like 'Data.List.unwords'.

    unwords :: List1 String -> String
    unwords :: List1 String -> String
    unwords = [String] -> String
    List.unwords ([String] -> String)
    -> (List1 String -> [String]) -> List1 String -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 String -> [String]
    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 'Agda.Utils.List.unzipWith'.

    unzipWith :: (a -> (b, c)) -> List1 a -> (List1 b, List1 c)
    unzipWith :: forall a b c. (a -> (b, c)) -> List1 a -> (List1 b, List1 c)
    unzipWith a -> (b, c)
    f = NonEmpty (b, c) -> (NonEmpty b, NonEmpty c)
    forall (f :: * -> *) a b. Functor f => f (a, b) -> (f a, f b)
    unzip (NonEmpty (b, c) -> (NonEmpty b, NonEmpty c))
    -> (List1 a -> NonEmpty (b, c))
    -> List1 a
    -> (NonEmpty b, NonEmpty c)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> (b, c)) -> List1 a -> NonEmpty (b, c)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> (b, c)
    f

    -- | 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 a b. m (a -> b) -> m a -> m b
    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 a b. m a -> m b -> m b
    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

    -- | List 'Data.List.foldr' but with a base case for the singleton list.

    foldr :: (a -> b -> b) -> (a -> b) -> List1 a -> b
    foldr :: forall a b. (a -> b -> b) -> (a -> b) -> List1 a -> b
    foldr a -> b -> b
    f a -> b
    g (a
    x :| [a]
    xs) = a -> [a] -> b
    loop a
    x [a]
    xs
      where
      loop :: a -> [a] -> b
    loop a
    x []       = a -> b
    g a
    x
      loop a
    x (a
    y : [a]
    ys) = a -> b -> b
    f a
    x (b -> b) -> b -> b
    forall a b. (a -> b) -> a -> b
    $ a -> [a] -> b
    loop a
    y [a]
    ys

    -- | Update the first element of a non-empty list.
    --   O(1).
    updateHead :: (a -> a) -> List1 a -> List1 a
    updateHead :: forall a. (a -> a) -> List1 a -> List1 a
    updateHead a -> a
    f (a
    a :| [a]
    as) = a -> a
    f a
    a a -> [a] -> NonEmpty a
    forall a. a -> [a] -> NonEmpty a
    :| [a]
    as

    -- | Update the last element of a non-empty list.
    --   O(n).
    updateLast :: (a -> a) -> List1 a -> List1 a
    updateLast :: forall a. (a -> a) -> List1 a -> List1 a
    updateLast a -> a
    f (a
    a :| [a]
    as) = a -> [a] -> NonEmpty a
    loop a
    a [a]
    as
      where
      loop :: a -> [a] -> NonEmpty a
    loop a
    a []       = a -> NonEmpty a
    forall a. a -> NonEmpty a
    singleton (a -> NonEmpty a) -> a -> NonEmpty a
    forall a b. (a -> b) -> a -> b
    $ a -> a
    f a
    a
      loop a
    a (a
    b : [a]
    bs) = a -> NonEmpty a -> NonEmpty a
    forall a. a -> NonEmpty a -> NonEmpty a
    cons a
    a (NonEmpty a -> NonEmpty a) -> NonEmpty a -> NonEmpty a
    forall a b. (a -> b) -> a -> b
    $ a -> [a] -> NonEmpty a
    loop a
    b [a]
    bs

    -- | Focus on the first element of a non-empty list.
    --   O(1).
    lensHead :: Functor f => (a -> f a) -> List1 a -> f (List1 a)
    lensHead :: forall (f :: * -> *) a.
    Functor f =>
    (a -> f a) -> List1 a -> f (List1 a)
    lensHead a -> f a
    f (a
    a :| [a]
    as) = a -> f a
    f a
    a f a -> (a -> NonEmpty a) -> f (NonEmpty a)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> (a -> [a] -> NonEmpty a
    forall a. a -> [a] -> NonEmpty a
    :| [a]
    as)

    -- | Focus on the last element of a non-empty list.
    --   O(n).
    lensLast :: Functor f => (a -> f a) -> List1 a -> f (List1 a)
    lensLast :: forall (f :: * -> *) a.
    Functor f =>
    (a -> f a) -> List1 a -> f (List1 a)
    lensLast a -> f a
    f (a
    a :| [a]
    as) = a -> [a] -> f (NonEmpty a)
    loop a
    a [a]
    as
      where
      loop :: a -> [a] -> f (NonEmpty a)
    loop a
    a []       = a -> NonEmpty a
    forall a. a -> NonEmpty a
    singleton (a -> NonEmpty a) -> f a -> f (NonEmpty a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> f a
    f a
    a
      loop a
    a (a
    b : [a]
    bs) = a -> NonEmpty a -> NonEmpty a
    forall a. a -> NonEmpty a -> NonEmpty a
    cons a
    a (NonEmpty a -> NonEmpty a) -> f (NonEmpty a) -> f (NonEmpty a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> [a] -> f (NonEmpty a)
    loop a
    b [a]
    bs