content: ------------------------------------------------------------------------
  -- | 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 test left right = loop where
    loop a =
      case test a of
        Left  b -> loop =<< left a b
        Right c -> right a 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 mm f g = either f g =<< mm
  
  -- | 'Either _ b' is a functor.
  
  mapLeft :: (a -> c) -> Either a b -> Either c b
  mapLeft = first
  
  -- | 'Either a' is a functor.
  
  mapRight :: (b -> d) -> Either a b -> Either a d
  mapRight = 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 f g = either (fmap Left . f) (fmap Right . g)
  
  -- | Analogue of 'Data.Maybe.fromMaybe'.
  fromLeft :: (b -> a) -> Either a b -> a
  fromLeft = (id `either`)
  
  -- | Analogue of 'Data.Maybe.fromMaybe'.
  fromRight :: (a -> b) -> Either a b -> b
  fromRight = (`either` id)
  
  -- | Analogue of 'Agda.Utils.Maybe.fromMaybeM'.
  fromLeftM :: Monad m => (b -> m a) -> m (Either a b) -> m a
  fromLeftM f m = either return f =<< m
  
  -- | Analogue of 'Agda.Utils.Maybe.fromMaybeM'.
  fromRightM :: Monad m => (a -> m b) -> m (Either a b) -> m b
  fromRightM f m = either f return =<< m
  
  -- | Safe projection from 'Left'.
  --
  --   > maybeLeft (Left a) = Just a
  --   > maybeLeft Right{}  = Nothing
  --
  maybeLeft :: Either a b -> Maybe a
  maybeLeft = either Just (const Nothing)
  
  -- | Safe projection from 'Right'.
  --
  --   > maybeRight (Right b) = Just b
  --   > maybeRight Left{}    = Nothing
  --
  maybeRight :: Either a b -> Maybe b
  maybeRight = either (const Nothing) Just
  
  -- | Returns @'Just' input_with_tags_stripped@ if all elements are
  -- to the 'Left', and otherwise 'Nothing'.
  allLeft :: [Either a b] -> Maybe [a]
  allLeft = mapM 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 = mapM 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 = unfoldr c
    where
    c :: [Either a b] -> Maybe (Either (List1 a) (List1 b), [Either a b])
    c []             = Nothing
    c (Left  a : xs) = Just $ first (Left  . (a :|)) $ spanJust maybeLeft  xs
    c (Right b : xs) = Just $ first (Right . (b :|)) $ spanJust maybeRight xs
  
  -- | Convert 'Maybe' to @'Either' e@, given an error @e@ for the 'Nothing' case.
  maybeToEither :: e -> Maybe a -> Either e a
  maybeToEither e = maybe (Left e) Right
  
  -- | Swap tags 'Left' and 'Right'.
  swapEither :: Either a b -> Either b a
  swapEither = either Right Left
  