    -- Liang-Ting Chen (2019-07-04):
    -- Consider using Data.Maybe.Strict instead
    -- Andreas Abel (2019-07-05)@GitHub:
    -- The dependencies of strict-base-types are too heavy,
    -- especially since it depends on lens which we consciously ruled out.

    {-# LANGUAGE CPP #-}

    {-# OPTIONS_GHC -fno-warn-orphans #-}

    -- | A strict version of the 'Maybe' type.
    --
    --   Import qualified, as in
    --   @
    --     import qualified Agda.Utils.Maybe.Strict as Strict
    --   @
    --
    -- Copyright :  (c) 2006-2007 Roman Leshchinskiy
    --              (c) 2013 Simon Meier
    -- License   :  BSD-style (see the file LICENSE)
    --
    -- Copyright :  (c) 2014 Andreas Abel

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

    -- The following code is copied from
    -- http://hackage.haskell.org/package/strict-base-types-0.3.0/docs/src/Data-Maybe-Strict.html

    import           Prelude             hiding (Maybe (..), maybe, null)
    import qualified Prelude             as Lazy

    import           Control.DeepSeq     (NFData (..))
    import           Data.Binary         (Binary (..))
    import           Data.Data           (Data (..))
    import           Data.Semigroup      (Semigroup, (<>))
    import           Data.Strict.Maybe   (Maybe (Nothing, Just), fromJust,
                                          fromMaybe, isJust, isNothing, maybe)
    import           GHC.Generics        (Generic (..))

    import Agda.Utils.Null

    toStrict :: Lazy.Maybe a -> Maybe a
    toStrict :: forall a. Maybe a -> Maybe a
    toStrict Maybe a
    Lazy.Nothing  = Maybe a
    forall a. Maybe a
    Nothing
    toStrict (Lazy.Just a
    x) = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x

    toLazy :: Maybe a -> Lazy.Maybe a
    toLazy :: forall a. Maybe a -> Maybe a
    toLazy Maybe a
    Nothing  = Maybe a
    forall a. Maybe a
    Lazy.Nothing
    toLazy (Just a
    x) = a -> Maybe a
    forall a. a -> Maybe a
    Lazy.Just a
    x

    #if !(MIN_VERSION_strict(0,4,0))
    deriving instance Data a => Data (Maybe a)
    deriving instance Generic  (Maybe a)

    -- The monoid instance was fixed in strict-base-types 0.5.0. See
    -- Issue 1805.
    instance Semigroup a => Semigroup (Maybe a) where
      (<>) = unionMaybeWith (<>)

    instance Semigroup a => Monoid (Maybe a) where
      mempty  = Nothing
      mappend = (<>)

    instance Foldable Maybe where
        foldMap _ Nothing  = mempty
        foldMap f (Just x) = f x

    instance Traversable Maybe where
        traverse _ Nothing  = pure Nothing
        traverse f (Just x) = Just <$> f x

    instance NFData a => NFData (Maybe a) where
      rnf = rnf . toLazy

    instance Binary a => Binary (Maybe a) where
      put = put . toLazy
      get = toStrict <$> get
    #endif

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

    -- | Analogous to 'Lazy.listToMaybe' in "Data.Maybe".
    listToMaybe :: [a] -> Maybe a
    listToMaybe :: forall a. [a] -> Maybe a
    listToMaybe []        =  Maybe a
    forall a. Maybe a
    Nothing
    listToMaybe (a
    a:[a]
    _)     =  a -> Maybe a
    forall a. a -> Maybe a
    Just a
    a

    -- | Analogous to 'Lazy.maybeToList' in "Data.Maybe".
    maybeToList :: Maybe a -> [a]
    maybeToList :: forall a. Maybe a -> [a]
    maybeToList  Maybe a
    Nothing   = []
    maybeToList  (Just a
    x)  = [a
    x]

    -- | Analogous to 'Lazy.catMaybes' in "Data.Maybe".
    catMaybes :: [Maybe a] -> [a]
    catMaybes :: forall a. [Maybe a] -> [a]
    catMaybes [Maybe a]
    ls = [a
    x | Just a
    x <- [Maybe a]
    ls]

    -- | Analogous to 'Lazy.mapMaybe' in "Data.Maybe".
    mapMaybe :: (a -> Maybe b) -> [a] -> [b]
    mapMaybe :: forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe a -> Maybe b
    _ []     = []
    mapMaybe a -> Maybe b
    f (a
    x:[a]
    xs) = case a -> Maybe b
    f a
    x of
        Maybe b
    Nothing -> [b]
    rs
        Just b
    r  -> b
    rb -> [b] -> [b]
    forall a. a -> [a] -> [a]
    :[b]
    rs
      where
        rs :: [b]
    rs = (a -> Maybe b) -> [a] -> [b]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe a -> Maybe b
    f [a]
    xs

    -- The remaining code is a copy of Agda.Utils.Maybe

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