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