-- 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 DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric      #-}


{-# 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 :: 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 :: 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

deriving instance Data a => Data (Maybe a)
deriving instance Generic  (Maybe a)

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

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

instance Semigroup a => Monoid (Maybe a) where
  mempty :: Maybe a
mempty  = Maybe a
forall a. Maybe a
Nothing
  mappend :: Maybe a -> Maybe a -> Maybe a
mappend = Maybe a -> Maybe a -> Maybe a
forall a. Semigroup a => a -> a -> a
(<>)

-- | 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 :: a -> Maybe a
pure              = a -> Maybe a
forall a. a -> Maybe a
Just
  Just a -> b
f <*> :: 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 Foldable Maybe where
    foldMap :: (a -> m) -> Maybe a -> m
foldMap a -> m
_ Maybe a
Nothing  = m
forall a. Monoid a => a
mempty
    foldMap a -> m
f (Just a
x) = a -> m
f a
x

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

instance NFData a => NFData (Maybe a) where
  rnf :: Maybe a -> ()
rnf = Maybe a -> ()
forall a. NFData a => a -> ()
rnf (Maybe a -> ()) -> (Maybe a -> Maybe a) -> Maybe a -> ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> Maybe a
forall a. Maybe a -> Maybe a
toLazy

instance Binary a => Binary (Maybe a) where
  put :: Maybe a -> Put
put = Maybe a -> Put
forall t. Binary t => t -> Put
put (Maybe a -> Put) -> (Maybe a -> Maybe a) -> Maybe a -> Put
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> Maybe a
forall a. Maybe a -> Maybe a
toLazy
  get :: Get (Maybe a)
get = Maybe a -> Maybe a
forall a. Maybe a -> Maybe a
toStrict (Maybe a -> Maybe a) -> Get (Maybe a) -> Get (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get (Maybe a)
forall t. Binary t => Get t
get

-- | Analogous to 'Lazy.listToMaybe' in "Data.Maybe".
listToMaybe :: [a] -> Maybe a
listToMaybe :: [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 :: 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 :: [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 :: (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 :: (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 :: 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 :: (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 :: [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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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)