    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | A strict version of the 'Maybe' type.
    --
    --   Import qualified, as in
    --   @
    --     import qualified Agda.Utils.Maybe.Strict as Strict
    --   @

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

    import Prelude hiding (Maybe(..), maybe)

    import qualified Data.Maybe as Lazy
    import Data.Strict.Classes
    import Data.Strict.Maybe

    import Agda.Utils.Functor ( (<.>) )
    import Agda.Utils.Lens    ( Lens' )
    import Agda.Utils.Null

    -- | Note that strict Maybe is an 'Applicative' only modulo strictness.
    --   The laws only hold in the strict semantics.
    --   Eg. @pure f <*> pure _|_ = _|_@, but according to the laws for
    --   'Applicative' it should be @pure (f _|_)@.
    --   We ignore this issue here, it applies also to 'Foldable' and 'Traversable'.

    instance Applicative Maybe where
      pure :: forall a. a -> Maybe a
    pure              = a -> Maybe a
    forall a. a -> Maybe a
    Just
      Just a -> b
    f <*> :: forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
    <*> Just a
    x = b -> Maybe b
    forall a. a -> Maybe a
    Just (b -> Maybe b) -> b -> Maybe b
    forall a b. (a -> b) -> a -> b
    $ a -> b
    f a
    x
      Maybe (a -> b)
    _      <*> Maybe a
    _      = Maybe b
    forall a. Maybe a
    Nothing

    instance Null (Maybe a) where
      empty :: Maybe a
    empty = Maybe a
    forall a. Maybe a
    Nothing
      null :: Maybe a -> Bool
    null = Maybe a -> Bool
    forall a. Maybe a -> Bool
    isNothing

    -- * Conversion to lazy @Maybe@.

    lensMaybeLazy :: Lens' (Maybe a) (Lazy.Maybe a)
    lensMaybeLazy :: forall a (f :: * -> *).
    Functor f =>
    (Maybe a -> f (Maybe a)) -> Maybe a -> f (Maybe a)
    lensMaybeLazy Maybe a -> f (Maybe a)
    f = Maybe a -> Maybe a
    forall lazy strict. Strict lazy strict => lazy -> strict
    toStrict (Maybe a -> Maybe a)
    -> (Maybe a -> f (Maybe a)) -> Maybe a -> f (Maybe a)
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Maybe a -> f (Maybe a)
    f (Maybe a -> f (Maybe a))
    -> (Maybe a -> Maybe a) -> Maybe a -> f (Maybe a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe a -> Maybe a
    forall lazy strict. Strict lazy strict => strict -> lazy
    toLazy

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

    -- | 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 err f = flip (maybe err) m f@
    caseMaybe :: Maybe a -> b -> (a -> b) -> b
    caseMaybe :: forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe a
    m b
    err a -> b
    f = b -> (a -> b) -> Maybe a -> b
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe b
    err 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 a. 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
    err 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
    err 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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) a -> m ()
    k

    -- | '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 a b. m a -> (a -> m b) -> m b
    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)