    ------------------------------------------------------------------------
    -- | Utilities for the 'Either' type.
    ------------------------------------------------------------------------

    module Agda.Utils.Either
      ( whileLeft
      , caseEitherM
      , mapLeft
      , mapRight
      , traverseEither
      , isLeft
      , isRight
      , fromLeft
      , fromRight
      , fromLeftM
      , fromRightM
      , maybeLeft
      , maybeRight
      , allLeft
      , allRight
      , groupByEither
      , maybeToEither
      , swapEither
      ) where

    import Data.Bifunctor
    import Data.Either (isLeft, isRight)
    import Data.List   (unfoldr)

    import Agda.Utils.List ( spanJust )
    import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
    import qualified Agda.Utils.List1 as List1

    -- | Loop while we have an exception.

    whileLeft :: Monad m => (a -> Either b c) -> (a -> b -> m a) -> (a -> c -> m d) -> a -> m d
    whileLeft :: forall (m :: * -> *) a b c d.
    Monad m =>
    (a -> Either b c) -> (a -> b -> m a) -> (a -> c -> m d) -> a -> m d
    whileLeft a -> Either b c
    test a -> b -> m a
    left a -> c -> m d
    right = a -> m d
    loop where
      loop :: a -> m d
    loop a
    a =
        case a -> Either b c
    test a
    a of
          Left  b
    b -> a -> m d
    loop (a -> m d) -> m a -> m d
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< a -> b -> m a
    left a
    a b
    b
          Right c
    c -> a -> c -> m d
    right a
    a c
    c

    -- | Monadic version of 'either' with a different argument ordering.

    caseEitherM :: Monad m => m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
    caseEitherM :: forall (m :: * -> *) a b c.
    Monad m =>
    m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
    caseEitherM m (Either a b)
    mm a -> m c
    f b -> m c
    g = (a -> m c) -> (b -> m c) -> Either a b -> m c
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either a -> m c
    f b -> m c
    g (Either a b -> m c) -> m (Either a b) -> m c
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m (Either a b)
    mm

    -- | 'Either _ b' is a functor.

    mapLeft :: (a -> c) -> Either a b -> Either c b
    mapLeft :: forall a c b. (a -> c) -> Either a b -> Either c b
    mapLeft = (a -> c) -> Either a b -> Either c b
    forall a c b. (a -> c) -> Either a b -> Either c b
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first

    -- | 'Either a' is a functor.

    mapRight :: (b -> d) -> Either a b -> Either a d
    mapRight :: forall b d a. (b -> d) -> Either a b -> Either a d
    mapRight = (b -> d) -> Either a b -> Either a d
    forall b d a. (b -> d) -> Either a b -> Either a d
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second

    -- | 'Either' is bitraversable.
    -- Note: From @base >= 4.10.0.0@ already present in `Data.Bitraversable`.
    traverseEither :: Functor f => (a -> f c) -> (b -> f d) -> Either a b -> f (Either c d)
    traverseEither :: forall (f :: * -> *) a c b d.
    Functor f =>
    (a -> f c) -> (b -> f d) -> Either a b -> f (Either c d)
    traverseEither a -> f c
    f b -> f d
    g = (a -> f (Either c d))
    -> (b -> f (Either c d)) -> Either a b -> f (Either c d)
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either ((c -> Either c d) -> f c -> f (Either c d)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap c -> Either c d
    forall a b. a -> Either a b
    Left (f c -> f (Either c d)) -> (a -> f c) -> a -> f (Either c d)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> f c
    f) ((d -> Either c d) -> f d -> f (Either c d)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap d -> Either c d
    forall a b. b -> Either a b
    Right (f d -> f (Either c d)) -> (b -> f d) -> b -> f (Either c d)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b -> f d
    g)

    -- | Analogue of 'Data.Maybe.fromMaybe'.
    fromLeft :: (b -> a) -> Either a b -> a
    fromLeft :: forall b a. (b -> a) -> Either a b -> a
    fromLeft = (a -> a
    forall a. a -> a
    id (a -> a) -> (b -> a) -> Either a b -> a
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    `either`)

    -- | Analogue of 'Data.Maybe.fromMaybe'.
    fromRight :: (a -> b) -> Either a b -> b
    fromRight :: forall a b. (a -> b) -> Either a b -> b
    fromRight = ((a -> b) -> (b -> b) -> Either a b -> b
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    `either` b -> b
    forall a. a -> a
    id)

    -- | Analogue of 'Agda.Utils.Maybe.fromMaybeM'.
    fromLeftM :: Monad m => (b -> m a) -> m (Either a b) -> m a
    fromLeftM :: forall (m :: * -> *) b a.
    Monad m =>
    (b -> m a) -> m (Either a b) -> m a
    fromLeftM b -> m a
    f m (Either a b)
    m = (a -> m a) -> (b -> m a) -> Either a b -> m a
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either a -> m a
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return b -> m a
    f (Either a b -> m a) -> m (Either a b) -> m a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m (Either a b)
    m

    -- | Analogue of 'Agda.Utils.Maybe.fromMaybeM'.
    fromRightM :: Monad m => (a -> m b) -> m (Either a b) -> m b
    fromRightM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> m (Either a b) -> m b
    fromRightM a -> m b
    f m (Either a b)
    m = (a -> m b) -> (b -> m b) -> Either a b -> m b
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either a -> m b
    f b -> m b
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either a b -> m b) -> m (Either a b) -> m b
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m (Either a b)
    m

    -- | Safe projection from 'Left'.
    --
    --   > maybeLeft (Left a) = Just a
    --   > maybeLeft Right{}  = Nothing
    --
    maybeLeft :: Either a b -> Maybe a
    maybeLeft :: forall a b. Either a b -> Maybe a
    maybeLeft = (a -> Maybe a) -> (b -> Maybe a) -> Either a b -> Maybe a
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either a -> Maybe a
    forall a. a -> Maybe a
    Just (Maybe a -> b -> Maybe a
    forall a b. a -> b -> a
    const Maybe a
    forall a. Maybe a
    Nothing)

    -- | Safe projection from 'Right'.
    --
    --   > maybeRight (Right b) = Just b
    --   > maybeRight Left{}    = Nothing
    --
    maybeRight :: Either a b -> Maybe b
    maybeRight :: forall a b. Either a b -> Maybe b
    maybeRight = (a -> Maybe b) -> (b -> Maybe b) -> Either a b -> Maybe b
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (Maybe b -> a -> Maybe b
    forall a b. a -> b -> a
    const Maybe b
    forall a. Maybe a
    Nothing) b -> Maybe b
    forall a. a -> Maybe a
    Just

    -- | Returns @'Just' input_with_tags_stripped@ if all elements are
    -- to the 'Left', and otherwise 'Nothing'.
    allLeft :: [Either a b] -> Maybe [a]
    allLeft :: forall a b. [Either a b] -> Maybe [a]
    allLeft = (Either a b -> Maybe a) -> [Either a b] -> Maybe [a]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Either a b -> Maybe a
    forall a b. Either a b -> Maybe a
    maybeLeft

    -- | Returns @'Just' input_with_tags_stripped@ if all elements are
    -- to the right, and otherwise 'Nothing'.
    --
    -- @
    --  allRight xs ==
    --    if all isRight xs then
    --      Just (map (\(Right x) -> x) xs)
    --     else
    --      Nothing
    -- @

    allRight :: [Either a b] -> Maybe [b]
    allRight :: forall a b. [Either a b] -> Maybe [b]
    allRight = (Either a b -> Maybe b) -> [Either a b] -> Maybe [b]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Either a b -> Maybe b
    forall a b. Either a b -> Maybe b
    maybeRight

    -- | Groups a list into alternating chunks of 'Left' and 'Right' values
    groupByEither :: forall a b. [Either a b] -> [Either (List1 a) (List1 b)]
    groupByEither :: forall a b. [Either a b] -> [Either (List1 a) (List1 b)]
    groupByEither = ([Either a b] -> Maybe (Either (List1 a) (List1 b), [Either a b]))
    -> [Either a b] -> [Either (List1 a) (List1 b)]
    forall b a. (b -> Maybe (a, b)) -> b -> [a]
    unfoldr [Either a b] -> Maybe (Either (List1 a) (List1 b), [Either a b])
    c
      where
      c :: [Either a b] -> Maybe (Either (List1 a) (List1 b), [Either a b])
      c :: [Either a b] -> Maybe (Either (List1 a) (List1 b), [Either a b])
    c []             = Maybe (Either (List1 a) (List1 b), [Either a b])
    forall a. Maybe a
    Nothing
      c (Left  a
    a : [Either a b]
    xs) = (Either (List1 a) (List1 b), [Either a b])
    -> Maybe (Either (List1 a) (List1 b), [Either a b])
    forall a. a -> Maybe a
    Just ((Either (List1 a) (List1 b), [Either a b])
     -> Maybe (Either (List1 a) (List1 b), [Either a b]))
    -> (Either (List1 a) (List1 b), [Either a b])
    -> Maybe (Either (List1 a) (List1 b), [Either a b])
    forall a b. (a -> b) -> a -> b
    $ ([a] -> Either (List1 a) (List1 b))
    -> ([a], [Either a b])
    -> (Either (List1 a) (List1 b), [Either a b])
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first (List1 a -> Either (List1 a) (List1 b)
    forall a b. a -> Either a b
    Left  (List1 a -> Either (List1 a) (List1 b))
    -> ([a] -> List1 a) -> [a] -> Either (List1 a) (List1 b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a
    a a -> [a] -> List1 a
    forall a. a -> [a] -> NonEmpty a
    :|)) (([a], [Either a b]) -> (Either (List1 a) (List1 b), [Either a b]))
    -> ([a], [Either a b])
    -> (Either (List1 a) (List1 b), [Either a b])
    forall a b. (a -> b) -> a -> b
    $ (Either a b -> Maybe a) -> [Either a b] -> ([a], [Either a b])
    forall a b. (a -> Maybe b) -> [a] -> (Prefix b, [a])
    spanJust Either a b -> Maybe a
    forall a b. Either a b -> Maybe a
    maybeLeft  [Either a b]
    xs
      c (Right b
    b : [Either a b]
    xs) = (Either (List1 a) (List1 b), [Either a b])
    -> Maybe (Either (List1 a) (List1 b), [Either a b])
    forall a. a -> Maybe a
    Just ((Either (List1 a) (List1 b), [Either a b])
     -> Maybe (Either (List1 a) (List1 b), [Either a b]))
    -> (Either (List1 a) (List1 b), [Either a b])
    -> Maybe (Either (List1 a) (List1 b), [Either a b])
    forall a b. (a -> b) -> a -> b
    $ ([b] -> Either (List1 a) (List1 b))
    -> ([b], [Either a b])
    -> (Either (List1 a) (List1 b), [Either a b])
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first (List1 b -> Either (List1 a) (List1 b)
    forall a b. b -> Either a b
    Right (List1 b -> Either (List1 a) (List1 b))
    -> ([b] -> List1 b) -> [b] -> Either (List1 a) (List1 b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (b
    b b -> [b] -> List1 b
    forall a. a -> [a] -> NonEmpty a
    :|)) (([b], [Either a b]) -> (Either (List1 a) (List1 b), [Either a b]))
    -> ([b], [Either a b])
    -> (Either (List1 a) (List1 b), [Either a b])
    forall a b. (a -> b) -> a -> b
    $ (Either a b -> Maybe b) -> [Either a b] -> ([b], [Either a b])
    forall a b. (a -> Maybe b) -> [a] -> (Prefix b, [a])
    spanJust Either a b -> Maybe b
    forall a b. Either a b -> Maybe b
    maybeRight [Either a b]
    xs

    -- | Convert 'Maybe' to @'Either' e@, given an error @e@ for the 'Nothing' case.
    maybeToEither :: e -> Maybe a -> Either e a
    maybeToEither :: forall e a. e -> Maybe a -> Either e a
    maybeToEither e
    e = Either e a -> (a -> Either e a) -> Maybe a -> Either e a
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (e -> Either e a
    forall a b. a -> Either a b
    Left e
    e) a -> Either e a
    forall a b. b -> Either a b
    Right

    -- | Swap tags 'Left' and 'Right'.
    swapEither :: Either a b -> Either b a
    swapEither :: forall a b. Either a b -> Either b a
    swapEither = (a -> Either b a) -> (b -> Either b a) -> Either a b -> Either b a
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either a -> Either b a
    forall a b. b -> Either a b
    Right b -> Either b a
    forall a b. a -> Either a b
    Left