------------------------------------------------------------------------
-- | 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
import Agda.Utils.Singleton

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