    -- | Extend 'Data.Maybe' by common operations for the 'Maybe' type.
    --
    --   Note: since this module is usually imported unqualified,
    --   we do not use short names, but all names contain 'Maybe',
    --   'Just', or 'Nothing.

    module Agda.Utils.Maybe
        ( module Agda.Utils.Maybe
        , module Data.Maybe
        ) where

    import Control.Applicative
    import Control.Monad.Trans.Maybe

    import Data.Maybe

    -- * Conversion.

    -- | Retain object when tag is 'True'.
    boolToMaybe :: Bool -> a -> Maybe a
    boolToMaybe :: forall a. Bool -> a -> Maybe a
    boolToMaybe Bool
    b a
    x = if Bool
    b then a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x else Maybe a
    forall a. Maybe a
    Nothing

    -- * Collection operations.

    -- | @unionWith@ for collections of size <= 1.
    unionMaybeWith :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
    unionMaybeWith :: forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
    unionMaybeWith a -> a -> a
    f Maybe a
    Nothing Maybe a
    mb      = Maybe a
    mb
    unionMaybeWith a -> a -> a
    f Maybe a
    ma      Maybe a
    Nothing = Maybe a
    ma
    unionMaybeWith a -> a -> a
    f (Just a
    a) (Just a
    b) = a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ a -> a -> a
    f a
    a a
    b

    -- | @unionsWith@ for collections of size <= 1.
    unionsMaybeWith :: (a -> a -> a) -> [Maybe a] -> Maybe a
    unionsMaybeWith :: forall a. (a -> a -> a) -> [Maybe a] -> Maybe a
    unionsMaybeWith a -> a -> a
    f [Maybe a]
    ms = case [Maybe a] -> [a]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe a]
    ms of
      [] -> Maybe a
    forall a. Maybe a
    Nothing
      [a]
    as -> a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldl1 a -> a -> a
    f [a]
    as

    -- | Unzipping a list of length <= 1.

    unzipMaybe :: Maybe (a,b) -> (Maybe a, Maybe b)
    unzipMaybe :: forall a b. Maybe (a, b) -> (Maybe a, Maybe b)
    unzipMaybe Maybe (a, b)
    Nothing      = (Maybe a
    forall a. Maybe a
    Nothing, Maybe b
    forall a. Maybe a
    Nothing)
    unzipMaybe (Just (a
    a,b
    b)) = (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    a, b -> Maybe b
    forall a. a -> Maybe a
    Just b
    b)

    -- | Filtering a singleton list.
    --
    --   @filterMaybe p a = 'listToMaybe' ('filter' p [a])@

    filterMaybe :: (a -> Bool) -> a -> Maybe a
    filterMaybe :: forall a. (a -> Bool) -> a -> Maybe a
    filterMaybe a -> Bool
    p a
    a
      | a -> Bool
    p a
    a       = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    a
      | Bool
    otherwise = Maybe a
    forall a. Maybe a
    Nothing

    -- * Conditionals and loops.

    -- | Version of 'mapMaybe' with different argument ordering.

    forMaybe :: [a] -> (a -> Maybe b) -> [b]
    forMaybe :: forall a b. [a] -> (a -> Maybe b) -> [b]
    forMaybe = ((a -> Maybe b) -> [a] -> [b]) -> [a] -> (a -> Maybe b) -> [b]
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (a -> Maybe b) -> [a] -> [b]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe

    -- | Version of 'maybe' with different argument ordering.
    --   Often, we want to case on a 'Maybe', do something interesting
    --   in the 'Just' case, but only a default action in the 'Nothing'
    --   case.  Then, the argument ordering of @caseMaybe@ is preferable.
    --
    --   @caseMaybe m d f = flip (maybe d) m f@
    caseMaybe :: Maybe a -> b -> (a -> b) -> b
    caseMaybe :: forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe a
    m b
    d a -> b
    f = b -> (a -> b) -> Maybe a -> b
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe b
    d a -> b
    f Maybe a
    m

    -- | 'caseMaybe' with flipped branches.
    ifJust :: Maybe a -> (a -> b) -> b -> b
    ifJust :: forall a b. Maybe a -> (a -> b) -> b -> b
    ifJust Maybe a
    m a -> b
    f b
    d = b -> (a -> b) -> Maybe a -> b
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe b
    d a -> b
    f Maybe a
    m

    -- * Monads and Maybe.

    -- | Monadic version of 'maybe'.

    maybeM :: Monad m => m b -> (a -> m b) -> m (Maybe a) -> m b
    maybeM :: forall (m :: * -> *) b a.
    Monad m =>
    m b -> (a -> m b) -> m (Maybe a) -> m b
    maybeM m b
    n a -> m b
    j m (Maybe a)
    mm = m b -> (a -> m b) -> Maybe a -> m b
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m b
    n a -> m b
    j (Maybe a -> m b) -> m (Maybe a) -> m b
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m (Maybe a)
    mm

    -- | Monadic version of 'fromMaybe'.

    fromMaybeM :: Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM :: forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM m a
    m m (Maybe a)
    mm = m a -> (a -> m a) -> m (Maybe a) -> m a
    forall (m :: * -> *) b a.
    Monad m =>
    m b -> (a -> m b) -> m (Maybe a) -> m b
    maybeM m a
    m a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return m (Maybe a)
    mm

    -- | Monadic version of 'caseMaybe'.
    --   That is, 'maybeM' with a different argument ordering.
    caseMaybeM :: Monad m => m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM :: forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM m (Maybe a)
    mm m b
    d a -> m b
    f = m b -> (a -> m b) -> m (Maybe a) -> m b
    forall (m :: * -> *) b a.
    Monad m =>
    m b -> (a -> m b) -> m (Maybe a) -> m b
    maybeM m b
    d a -> m b
    f m (Maybe a)
    mm

    -- | 'caseMaybeM' with flipped branches.
    ifJustM :: Monad m => m (Maybe a) -> (a -> m b) -> m b -> m b
    ifJustM :: forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> (a -> m b) -> m b -> m b
    ifJustM m (Maybe a)
    mm = (m b -> (a -> m b) -> m b) -> (a -> m b) -> m b -> m b
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (m (Maybe a) -> m b -> (a -> m b) -> m b
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM m (Maybe a)
    mm)

    -- | A more telling name for 'Traversable.forM_' for the 'Maybe' collection type.
    --   Or: 'caseMaybe' without the 'Nothing' case.
    whenJust :: Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust :: forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe a
    m a -> m ()
    k = Maybe a -> m () -> (a -> m ()) -> m ()
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe a
    m (() -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) a -> m ()
    k

    -- | 'caseMaybe' without the 'Just' case.
    whenNothing :: Monoid m => Maybe a -> m -> m
    whenNothing :: forall m a. Monoid m => Maybe a -> m -> m
    whenNothing Maybe a
    m m
    d = Maybe a -> m -> (a -> m) -> m
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe a
    m m
    d (\a
    _ -> m
    forall a. Monoid a => a
    mempty)

    -- | 'caseMaybeM' without the 'Nothing' case.
    whenJustM :: Monad m => m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM :: forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM m (Maybe a)
    c a -> m ()
    m = m (Maybe a)
    c m (Maybe a) -> (Maybe a -> m ()) -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (Maybe a -> (a -> m ()) -> m ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    `whenJust` a -> m ()
    m)

    -- | 'caseMaybeM' without the 'Just' case.
    whenNothingM :: Monad m => m (Maybe a) -> m () -> m ()
    whenNothingM :: forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
    whenNothingM m (Maybe a)
    mm m ()
    d = m () -> (a -> m ()) -> Maybe a -> m ()
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m ()
    d (\a
    _ -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) (Maybe a -> m ()) -> m (Maybe a) -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m (Maybe a)
    mm

    -- | Lazy version of @allJust <.> sequence@.
    --   (@allJust = mapM@ for the @Maybe@ monad.)
    --   Only executes monadic effect while @isJust@.
    allJustM :: Monad m => [m (Maybe a)] -> m (Maybe [a])
    allJustM :: forall (m :: * -> *) a. Monad m => [m (Maybe a)] -> m (Maybe [a])
    allJustM = MaybeT m [a] -> m (Maybe [a])
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT m [a] -> m (Maybe [a]))
    -> ([m (Maybe a)] -> MaybeT m [a])
    -> [m (Maybe a)]
    -> m (Maybe [a])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (m (Maybe a) -> MaybeT m a) -> [m (Maybe a)] -> MaybeT m [a]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM m (Maybe a) -> MaybeT m a
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT

    -- | Lift a maybe to an Alternative.
    liftMaybe :: Alternative f => Maybe a -> f a
    liftMaybe :: forall (f :: * -> *) a. Alternative f => Maybe a -> f a
    liftMaybe = f a -> (a -> f a) -> Maybe a -> f a
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe f a
    forall (f :: * -> *) a. Alternative f => f a
    empty a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure