module Agda.Utils.Either
( whileLeft
, caseEitherM
, mapLeft
, mapRight
, traverseEither
, isLeft
, isRight
, fromLeft
, fromRight
, fromLeftM
, fromRightM
, maybeLeft
, maybeRight
, allLeft
, allRight
, groupByEither
, maybeToEither
) where
import Data.Bifunctor
import Data.Either (isLeft, isRight)
import Agda.Utils.List ( listCase )
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
caseEitherM :: Monad m => m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM mm f g = either f g =<< mm
mapLeft :: (a -> c) -> Either a b -> Either c b
mapLeft = first
mapRight :: (b -> d) -> Either a b -> Either a d
mapRight = second
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)
fromLeft :: (b -> a) -> Either a b -> a
fromLeft = either id
fromRight :: (a -> b) -> Either a b -> b
fromRight f = either f id
fromLeftM :: Monad m => (b -> m a) -> m (Either a b) -> m a
fromLeftM f m = either return f =<< m
fromRightM :: Monad m => (a -> m b) -> m (Either a b) -> m b
fromRightM f m = either f return =<< m
maybeLeft :: Either a b -> Maybe a
maybeLeft = either Just (const Nothing)
maybeRight :: Either a b -> Maybe b
maybeRight = either (const Nothing) Just
allLeft :: [Either a b] -> Maybe [a]
allLeft = mapM maybeLeft
allRight :: [Either a b] -> Maybe [b]
allRight = mapM maybeRight
groupByEither :: forall a b. [Either a b] -> [Either [a] [b]]
groupByEither = listCase [] (go . init) where
go :: Either [a] [b] -> [Either a b] -> [Either [a] [b]]
go acc [] = adjust acc : []
go (Left acc) (Left a : abs) = go (Left $ a : acc) abs
go (Right acc) (Right b : abs) = go (Right $ b : acc) abs
go acc (ab : abs) = adjust acc : go (init ab) abs
adjust = bimap reverse reverse
init = bimap pure pure
maybeToEither :: Maybe a -> Either () a
maybeToEither = maybe (Left ()) Right