{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}

-- |
-- Module      :   Grisette.Unified.Lib.Control.Monad
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Unified.Lib.Control.Monad
  ( -- * Functor and Monad classes
    mrgFmap,
    (.<$),
    mrgReturnWithStrategy,
    mrgBindWithStrategy,
    mrgReturn,
    (.>>=),
    (.>>),
    mrgFail,
    mrgMzero,
    mrgMplus,

    -- * Functions

    -- ** Basic 'Monad' functions
    mrgMapM,
    mrgMapM_,
    mrgForM,
    mrgForM_,
    mrgSequence,
    mrgSequence_,
    (.=<<),
    (.>=>),
    (.<=<),
    mrgForever,
    mrgVoid,

    -- ** Generalisations of list functions
    mrgJoin,
    mrgMsum,
    mrgMfilter,
    symMfilter,
    mrgFilterM,
    symFilterM,
    mrgMapAndUnzipM,
    mrgZipWithM,
    mrgZipWithM_,
    mrgFoldM,
    mrgFoldM_,
    mrgReplicateM,
    symReplicateM,
    mrgReplicateM_,
    symReplicateM_,

    -- ** Conditional execution of monadic expressions
    mrgGuard,
    symGuard,
    mrgWhen,
    symWhen,
    mrgUnless,
    symUnless,

    -- ** Monadic lifting operators
    mrgLiftM,
    mrgLiftM2,
    mrgLiftM3,
    mrgLiftM4,
    mrgLiftM5,
    mrgAp,

    -- ** Strict monadic functions
    (.<$!>),
  )
where

import Control.Applicative (Alternative)
import Control.Monad (MonadPlus (mplus, mzero), join)
import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.||)))
import Grisette.Internal.Core.Data.Class.Mergeable
  ( Mergeable (rootStrategy),
    MergingStrategy,
  )
import Grisette.Internal.Core.Data.Class.SimpleMergeable (SymBranching)
import Grisette.Internal.Core.Data.Class.TryMerge
  ( MonadTryMerge,
    TryMerge (tryMergeWithStrategy),
    tryMerge,
  )
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Lib.Data.Functor (mrgFmap, mrgUnzip, mrgVoid, (.<$))
import Grisette.Lib.Data.Traversable
  ( mrgForM,
    mrgMapM,
    mrgSequence,
    mrgSequenceA,
    mrgTraverse,
  )
import Grisette.Unified
  ( EvalModeBase,
    GetBool,
    UnifiedBranching,
    UnifiedSymOrd,
    mrgIf,
    (.<=),
  )
import Grisette.Unified.Lib.Control.Applicative
  ( mrgEmpty,
    mrgLiftA2,
    mrgPure,
    (.*>),
    (.<$>),
    (.<*>),
  )
import Grisette.Unified.Lib.Data.Foldable
  ( mrgFoldlM,
    mrgForM_,
    mrgMapM_,
    mrgMsum,
    mrgSequenceA_,
    mrgSequence_,
  )

-- | 'return' with 'Grisette.Core.MergingStrategy' knowledge propagation.
mrgReturnWithStrategy :: (MonadTryMerge u) => MergingStrategy a -> a -> u a
mrgReturnWithStrategy :: forall (u :: * -> *) a.
MonadTryMerge u =>
MergingStrategy a -> a -> u a
mrgReturnWithStrategy MergingStrategy a
s = MergingStrategy a -> u a -> u a
forall a. MergingStrategy a -> u a -> u a
forall (m :: * -> *) a.
TryMerge m =>
MergingStrategy a -> m a -> m a
tryMergeWithStrategy MergingStrategy a
s (u a -> u a) -> (a -> u a) -> a -> u a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> u a
forall a. a -> u a
forall (m :: * -> *) a. Monad m => a -> m a
return
{-# INLINE mrgReturnWithStrategy #-}

-- | '>>=' with 'Grisette.Core.MergingStrategy' knowledge propagation.
mrgBindWithStrategy ::
  (MonadTryMerge u) =>
  MergingStrategy a ->
  MergingStrategy b ->
  u a ->
  (a -> u b) ->
  u b
mrgBindWithStrategy :: forall (u :: * -> *) a b.
MonadTryMerge u =>
MergingStrategy a -> MergingStrategy b -> u a -> (a -> u b) -> u b
mrgBindWithStrategy MergingStrategy a
sa MergingStrategy b
sb u a
a a -> u b
f =
  MergingStrategy b -> u b -> u b
forall a. MergingStrategy a -> u a -> u a
forall (m :: * -> *) a.
TryMerge m =>
MergingStrategy a -> m a -> m a
tryMergeWithStrategy MergingStrategy b
sb (u b -> u b) -> u b -> u b
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> u a -> u a
forall a. MergingStrategy a -> u a -> u a
forall (m :: * -> *) a.
TryMerge m =>
MergingStrategy a -> m a -> m a
tryMergeWithStrategy MergingStrategy a
sa u a
a u a -> (a -> u b) -> u b
forall a b. u a -> (a -> u b) -> u b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> u b
f
{-# INLINE mrgBindWithStrategy #-}

-- | 'return' with 'Grisette.Core.MergingStrategy' knowledge propagation.
mrgReturn :: (MonadTryMerge u, Mergeable a) => a -> u a
mrgReturn :: forall (u :: * -> *) a. (MonadTryMerge u, Mergeable a) => a -> u a
mrgReturn = MergingStrategy a -> a -> u a
forall (u :: * -> *) a.
MonadTryMerge u =>
MergingStrategy a -> a -> u a
mrgReturnWithStrategy MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy
{-# INLINE mrgReturn #-}

infixl 1 .>>=

-- | '>>=' with 'Grisette.Core.MergingStrategy' knowledge propagation.
(.>>=) ::
  (MonadTryMerge u, Mergeable a, Mergeable b) =>
  u a ->
  (a -> u b) ->
  u b
.>>= :: forall (u :: * -> *) a b.
(MonadTryMerge u, Mergeable a, Mergeable b) =>
u a -> (a -> u b) -> u b
(.>>=) = MergingStrategy a -> MergingStrategy b -> u a -> (a -> u b) -> u b
forall (u :: * -> *) a b.
MonadTryMerge u =>
MergingStrategy a -> MergingStrategy b -> u a -> (a -> u b) -> u b
mrgBindWithStrategy MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy MergingStrategy b
forall a. Mergeable a => MergingStrategy a
rootStrategy
{-# INLINE (.>>=) #-}

infixl 1 .>>

-- | '>>' with 'Grisette.Core.MergingStrategy' knowledge propagation.
--
-- This is usually more efficient than calling the original '>>' and merge the
-- results.
(.>>) :: (MonadTryMerge m, Mergeable a, Mergeable b) => m a -> m b -> m b
m a
a .>> :: forall (m :: * -> *) a b.
(MonadTryMerge m, Mergeable a, Mergeable b) =>
m a -> m b -> m b
.>> m b
f = m b -> m b
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ m a -> m ()
forall (f :: * -> *) a. (TryMerge f, Functor f) => f a -> f ()
mrgVoid m a
a m () -> m b -> m b
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m b
f
{-# INLINE (.>>) #-}

-- | 'fail' with 'Grisette.Core.MergingStrategy' knowledge propagation.
mrgFail :: (MonadTryMerge m, Mergeable a, MonadFail m) => String -> m a
mrgFail :: forall (m :: * -> *) a.
(MonadTryMerge m, Mergeable a, MonadFail m) =>
String -> m a
mrgFail = m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> (String -> m a) -> String -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail
{-# INLINE mrgFail #-}

-- | 'Control.Monad.mzero' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgMzero :: forall m a. (MonadTryMerge m, Mergeable a, MonadPlus m) => m a
mrgMzero :: forall (m :: * -> *) a.
(MonadTryMerge m, Mergeable a, MonadPlus m) =>
m a
mrgMzero = m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge m a
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
{-# INLINE mrgMzero #-}

-- | 'Control.Monad.mplus' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgMplus ::
  forall m a. (MonadTryMerge m, Mergeable a, MonadPlus m) => m a -> m a -> m a
mrgMplus :: forall (m :: * -> *) a.
(MonadTryMerge m, Mergeable a, MonadPlus m) =>
m a -> m a -> m a
mrgMplus m a
a m a
b = m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ m a -> m a -> m a
forall a. m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge m a
a) (m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge m a
b)
{-# INLINE mrgMplus #-}

infixr 1 .=<<

-- | '=<<' with 'Grisette.Core.MergingStrategy' knowledge propagation.
(.=<<) ::
  (MonadTryMerge m, Mergeable a, Mergeable b) => (a -> m b) -> m a -> m b
a -> m b
f .=<< :: forall (m :: * -> *) a b.
(MonadTryMerge m, Mergeable a, Mergeable b) =>
(a -> m b) -> m a -> m b
.=<< m a
a = m b -> m b
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ a -> m b
f (a -> m b) -> m a -> m b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge m a
a
{-# INLINE (.=<<) #-}

infixr 1 .>=>

-- | 'Control.Monad.>=>' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
(.>=>) ::
  (MonadTryMerge m, Mergeable a, Mergeable b, Mergeable c) =>
  (a -> m b) ->
  (b -> m c) ->
  a ->
  m c
a -> m b
f .>=> :: forall (m :: * -> *) a b c.
(MonadTryMerge m, Mergeable a, Mergeable b, Mergeable c) =>
(a -> m b) -> (b -> m c) -> a -> m c
.>=> b -> m c
g = \a
a -> m c -> m c
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m c -> m c) -> m c -> m c
forall a b. (a -> b) -> a -> b
$ m b -> m b
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (a -> m b
f a
a) m b -> (b -> m c) -> m c
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> m c
g
{-# INLINE (.>=>) #-}

infixr 1 .<=<

-- | 'Control.Monad.<=<' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
(.<=<) ::
  (MonadTryMerge m, Mergeable a, Mergeable b, Mergeable c) =>
  (b -> m c) ->
  (a -> m b) ->
  a ->
  m c
.<=< :: forall (m :: * -> *) a b c.
(MonadTryMerge m, Mergeable a, Mergeable b, Mergeable c) =>
(b -> m c) -> (a -> m b) -> a -> m c
(.<=<) = ((a -> m b) -> (b -> m c) -> a -> m c)
-> (b -> m c) -> (a -> m b) -> a -> m c
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> m b) -> (b -> m c) -> a -> m c
forall (m :: * -> *) a b c.
(MonadTryMerge m, Mergeable a, Mergeable b, Mergeable c) =>
(a -> m b) -> (b -> m c) -> a -> m c
(.>=>)
{-# INLINE (.<=<) #-}

-- | 'Control.Monad.forever' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgForever ::
  (Applicative m, TryMerge m, Mergeable b, Mergeable a) => m a -> m b
mrgForever :: forall (m :: * -> *) b a.
(Applicative m, TryMerge m, Mergeable b, Mergeable a) =>
m a -> m b
mrgForever m a
a = let a' :: m b
a' = m a
a m a -> m b -> m b
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f a -> f b -> f b
.*> m b
a' in m b
a'
{-# INLINE mrgForever #-}

-- | 'Control.Monad.join' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgJoin :: (MonadTryMerge m, Mergeable a) => m (m a) -> m a
mrgJoin :: forall (m :: * -> *) a.
(MonadTryMerge m, Mergeable a) =>
m (m a) -> m a
mrgJoin m (m a)
a = m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ m (m a) -> m a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join m (m a)
a
{-# INLINE mrgJoin #-}

-- | 'Control.Monad.mfilter' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgMfilter ::
  (MonadTryMerge m, MonadPlus m, Mergeable a) =>
  (a -> Bool) ->
  m a ->
  m a
mrgMfilter :: forall (m :: * -> *) a.
(MonadTryMerge m, MonadPlus m, Mergeable a) =>
(a -> Bool) -> m a -> m a
mrgMfilter a -> Bool
p m a
ma = do
  a
a <- m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge m a
ma
  if a -> Bool
p a
a then a -> m a
forall (u :: * -> *) a. (MonadTryMerge u, Mergeable a) => a -> u a
mrgReturn a
a else m a
forall (m :: * -> *) a.
(MonadTryMerge m, Mergeable a, MonadPlus m) =>
m a
mrgMzero
{-# INLINE mrgMfilter #-}

-- | 'Control.Monad.mfilter' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation and symbolic conditions.
symMfilter ::
  forall mode m a.
  ( MonadTryMerge m,
    MonadPlus m,
    UnifiedBranching mode m,
    Mergeable a
  ) =>
  (a -> GetBool mode) ->
  m a ->
  m a
symMfilter :: forall (mode :: EvalModeTag) (m :: * -> *) a.
(MonadTryMerge m, MonadPlus m, UnifiedBranching mode m,
 Mergeable a) =>
(a -> GetBool mode) -> m a -> m a
symMfilter a -> GetBool mode
p m a
ma = do
  a
a <- m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge m a
ma
  GetBool mode -> m a -> m a -> m a
forall (mode :: EvalModeTag) a (m :: * -> *).
(DecideEvalMode mode, Mergeable a, UnifiedBranching mode m) =>
GetBool mode -> m a -> m a -> m a
mrgIf (a -> GetBool mode
p a
a) (a -> m a
forall (u :: * -> *) a. (MonadTryMerge u, Mergeable a) => a -> u a
mrgReturn a
a) m a
forall (m :: * -> *) a.
(MonadTryMerge m, Mergeable a, MonadPlus m) =>
m a
mrgMzero
{-# INLINE symMfilter #-}

-- | 'Control.Monad.filterM' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgFilterM ::
  (TryMerge m, Applicative m, Mergeable a, Foldable t) =>
  (a -> m Bool) ->
  t a ->
  m [a]
mrgFilterM :: forall (m :: * -> *) a (t :: * -> *).
(TryMerge m, Applicative m, Mergeable a, Foldable t) =>
(a -> m Bool) -> t a -> m [a]
mrgFilterM a -> m Bool
p =
  (a -> m [a] -> m [a]) -> m [a] -> t a -> m [a]
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
    (\a
x m [a]
lst -> (\Bool
flg -> if Bool
flg then (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) else [a] -> [a]
forall a. a -> a
id) (Bool -> [a] -> [a]) -> m Bool -> m ([a] -> [a])
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
.<$> a -> m Bool
p a
x m ([a] -> [a]) -> m [a] -> m [a]
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
.<*> m [a]
lst)
    ([a] -> m [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure [])
{-# INLINE mrgFilterM #-}

-- | 'Control.Monad.filterM' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation and symbolic conditions.
symFilterM ::
  forall mode m t a.
  ( TryMerge m,
    UnifiedBranching mode m,
    MonadTryMerge m,
    EvalModeBase mode,
    Mergeable a,
    Foldable t
  ) =>
  (a -> m (GetBool mode)) ->
  t a ->
  m [a]
symFilterM :: forall (mode :: EvalModeTag) (m :: * -> *) (t :: * -> *) a.
(TryMerge m, UnifiedBranching mode m, MonadTryMerge m,
 EvalModeBase mode, Mergeable a, Foldable t) =>
(a -> m (GetBool mode)) -> t a -> m [a]
symFilterM a -> m (GetBool mode)
p =
  (a -> m [a] -> m [a]) -> m [a] -> t a -> m [a]
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
    ( \a
x m [a]
lst -> do
        GetBool mode
flag <- m (GetBool mode) -> m (GetBool mode)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (GetBool mode) -> m (GetBool mode))
-> m (GetBool mode) -> m (GetBool mode)
forall a b. (a -> b) -> a -> b
$ a -> m (GetBool mode)
p a
x
        GetBool mode -> m [a] -> m [a] -> m [a]
forall (mode :: EvalModeTag) a (m :: * -> *).
(DecideEvalMode mode, Mergeable a, UnifiedBranching mode m) =>
GetBool mode -> m a -> m a -> m a
mrgIf GetBool mode
flag ((a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> m [a] -> m [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [a]
lst) m [a]
lst
    )
    ([a] -> m [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure [])
{-# INLINE symFilterM #-}

-- | 'Control.Monad.mapAndUnzipM' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgMapAndUnzipM ::
  ( Applicative m,
    TryMerge m,
    Mergeable b,
    Mergeable c
  ) =>
  (a -> m (b, c)) ->
  [a] ->
  m ([b], [c])
mrgMapAndUnzipM :: forall (m :: * -> *) b c a.
(Applicative m, TryMerge m, Mergeable b, Mergeable c) =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mrgMapAndUnzipM a -> m (b, c)
f [a]
xs = [(b, c)] -> ([b], [c])
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
f (a, b) -> (f a, f b)
mrgUnzip ([(b, c)] -> ([b], [c])) -> m [(b, c)] -> m ([b], [c])
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
.<$> (a -> m (b, c)) -> [a] -> m [(b, c)]
forall a b (t :: * -> *) (f :: * -> *).
(Mergeable b, Mergeable1 t, TryMerge f, Applicative f,
 Traversable t) =>
(a -> f b) -> t a -> f (t b)
mrgTraverse a -> m (b, c)
f [a]
xs
{-# INLINE mrgMapAndUnzipM #-}

-- | 'Control.Monad.zipWithM' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgZipWithM ::
  (Applicative m, TryMerge m, Mergeable c) =>
  (a -> b -> m c) ->
  [a] ->
  [b] ->
  m [c]
mrgZipWithM :: forall (m :: * -> *) c a b.
(Applicative m, TryMerge m, Mergeable c) =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
mrgZipWithM a -> b -> m c
f [a]
xs [b]
ys = [m c] -> m [c]
forall a (t :: * -> *) (f :: * -> *).
(Mergeable a, Mergeable1 t, Applicative f, TryMerge f,
 Traversable t) =>
t (f a) -> f (t a)
mrgSequenceA ((a -> b -> m c) -> [a] -> [b] -> [m c]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> b -> m c
f [a]
xs [b]
ys)
{-# INLINE mrgZipWithM #-}

-- | 'Control.Monad.zipWithM_' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgZipWithM_ ::
  (Applicative m, TryMerge m, Mergeable c) =>
  (a -> b -> m c) ->
  [a] ->
  [b] ->
  m ()
mrgZipWithM_ :: forall (m :: * -> *) c a b.
(Applicative m, TryMerge m, Mergeable c) =>
(a -> b -> m c) -> [a] -> [b] -> m ()
mrgZipWithM_ a -> b -> m c
f [a]
xs [b]
ys = [m c] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, TryMerge m, Applicative m) =>
t (m a) -> m ()
mrgSequenceA_ ((a -> b -> m c) -> [a] -> [b] -> [m c]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> b -> m c
f [a]
xs [b]
ys)
{-# INLINE mrgZipWithM_ #-}

-- | 'Control.Monad.foldM' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgFoldM ::
  (MonadTryMerge m, Mergeable b, Foldable t) =>
  (b -> a -> m b) ->
  b ->
  t a ->
  m b
mrgFoldM :: forall (m :: * -> *) b (t :: * -> *) a.
(MonadTryMerge m, Mergeable b, Foldable t) =>
(b -> a -> m b) -> b -> t a -> m b
mrgFoldM = (b -> a -> m b) -> b -> t a -> m b
forall (m :: * -> *) b (t :: * -> *) a.
(MonadTryMerge m, Mergeable b, Foldable t) =>
(b -> a -> m b) -> b -> t a -> m b
mrgFoldlM
{-# INLINE mrgFoldM #-}

-- | 'Control.Monad.foldM_' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgFoldM_ ::
  (MonadTryMerge m, Foldable t, Mergeable b) =>
  (b -> a -> m b) ->
  b ->
  t a ->
  m ()
mrgFoldM_ :: forall (m :: * -> *) (t :: * -> *) b a.
(MonadTryMerge m, Foldable t, Mergeable b) =>
(b -> a -> m b) -> b -> t a -> m ()
mrgFoldM_ b -> a -> m b
f b
a t a
xs = (b -> a -> m b) -> b -> t a -> m b
forall (m :: * -> *) b (t :: * -> *) a.
(MonadTryMerge m, Mergeable b, Foldable t) =>
(b -> a -> m b) -> b -> t a -> m b
mrgFoldlM b -> a -> m b
f b
a t a
xs m b -> m () -> m ()
forall (m :: * -> *) a b.
(MonadTryMerge m, Mergeable a, Mergeable b) =>
m a -> m b -> m b
.>> () -> m ()
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ()
{-# INLINE mrgFoldM_ #-}

-- | 'Control.Monad.replicateM' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgReplicateM ::
  (Applicative m, TryMerge m, Mergeable a) =>
  Int ->
  m a ->
  m [a]
mrgReplicateM :: forall (m :: * -> *) a.
(Applicative m, TryMerge m, Mergeable a) =>
Int -> m a -> m [a]
mrgReplicateM Int
n = [m a] -> m [a]
forall a (t :: * -> *) (f :: * -> *).
(Mergeable a, Mergeable1 t, Applicative f, TryMerge f,
 Traversable t) =>
t (f a) -> f (t a)
mrgSequenceA ([m a] -> m [a]) -> (m a -> [m a]) -> m a -> m [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> m a -> [m a]
forall a. Int -> a -> [a]
replicate Int
n
{-# INLINE mrgReplicateM #-}

-- | 'Control.Monad.replicateM' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation and symbolic number of elements.
symReplicateM ::
  forall mode m a int.
  ( EvalModeBase mode,
    TryMerge m,
    Applicative m,
    Mergeable a,
    Num int,
    UnifiedBranching mode m,
    UnifiedSymOrd mode Int,
    UnifiedSymOrd mode int
  ) =>
  Int ->
  int ->
  m a ->
  m [a]
symReplicateM :: forall (mode :: EvalModeTag) (m :: * -> *) a int.
(EvalModeBase mode, TryMerge m, Applicative m, Mergeable a,
 Num int, UnifiedBranching mode m, UnifiedSymOrd mode Int,
 UnifiedSymOrd mode int) =>
Int -> int -> m a -> m [a]
symReplicateM Int
maxCnt int
cnt0 m a
f =
  Int -> int -> m [a]
loop Int
maxCnt int
cnt0
  where
    loop :: Int -> int -> m [a]
loop Int
concreteCnt int
cnt =
      forall (mode :: EvalModeTag) a (m :: * -> *).
(DecideEvalMode mode, Mergeable a, UnifiedBranching mode m) =>
GetBool mode -> m a -> m a -> m a
mrgIf @mode
        (int
cnt int -> int -> GetBool mode
forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymOrd mode a) =>
a -> a -> GetBool mode
.<= int
0 GetBool mode -> GetBool mode -> GetBool mode
forall b. LogicalOp b => b -> b -> b
.|| Int
concreteCnt Int -> Int -> GetBool mode
forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymOrd mode a) =>
a -> a -> GetBool mode
.<= Int
0)
        ([a] -> m [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure [])
        ((a -> [a] -> [a]) -> m a -> m [a] -> m [a]
forall (f :: * -> *) a b c.
(Applicative f, TryMerge f, Mergeable a, Mergeable b,
 Mergeable c) =>
(a -> b -> c) -> f a -> f b -> f c
mrgLiftA2 (:) m a
f (Int -> int -> m [a]
loop (Int
concreteCnt Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (int
cnt int -> int -> int
forall a. Num a => a -> a -> a
- int
1)))
{-# INLINE symReplicateM #-}

-- | 'Control.Monad.replicateM_' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgReplicateM_ ::
  (Applicative m, TryMerge m, Mergeable a) =>
  Int ->
  m a ->
  m ()
mrgReplicateM_ :: forall (m :: * -> *) a.
(Applicative m, TryMerge m, Mergeable a) =>
Int -> m a -> m ()
mrgReplicateM_ Int
n = [m a] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, TryMerge m, Applicative m) =>
t (m a) -> m ()
mrgSequenceA_ ([m a] -> m ()) -> (m a -> [m a]) -> m a -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> m a -> [m a]
forall a. Int -> a -> [a]
replicate Int
n
{-# INLINE mrgReplicateM_ #-}

-- | 'Control.Monad.replicateM_' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation and symbolic number of elements.
symReplicateM_ ::
  forall mode m a int.
  ( EvalModeBase mode,
    TryMerge m,
    Applicative m,
    Mergeable a,
    Num int,
    UnifiedBranching mode m,
    UnifiedSymOrd mode Int,
    UnifiedSymOrd mode int
  ) =>
  Int ->
  int ->
  m a ->
  m ()
symReplicateM_ :: forall (mode :: EvalModeTag) (m :: * -> *) a int.
(EvalModeBase mode, TryMerge m, Applicative m, Mergeable a,
 Num int, UnifiedBranching mode m, UnifiedSymOrd mode Int,
 UnifiedSymOrd mode int) =>
Int -> int -> m a -> m ()
symReplicateM_ Int
maxCnt int
cnt0 m a
f =
  Int -> int -> m ()
loop Int
maxCnt int
cnt0
  where
    loop :: Int -> int -> m ()
loop Int
concreteCnt int
cnt =
      forall (mode :: EvalModeTag) a (m :: * -> *).
(DecideEvalMode mode, Mergeable a, UnifiedBranching mode m) =>
GetBool mode -> m a -> m a -> m a
mrgIf @mode
        (int
cnt int -> int -> GetBool mode
forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymOrd mode a) =>
a -> a -> GetBool mode
.<= int
0 GetBool mode -> GetBool mode -> GetBool mode
forall b. LogicalOp b => b -> b -> b
.|| Int
concreteCnt Int -> Int -> GetBool mode
forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymOrd mode a) =>
a -> a -> GetBool mode
.<= Int
0)
        (() -> m ()
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ())
        (m a
f m a -> m () -> m ()
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f a -> f b -> f b
.*> (Int -> int -> m ()
loop (Int
concreteCnt Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (int
cnt int -> int -> int
forall a. Num a => a -> a -> a
- int
1)))
{-# INLINE symReplicateM_ #-}

-- | 'Control.Monad.guard' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgGuard :: (Alternative m, TryMerge m) => Bool -> m ()
mrgGuard :: forall (m :: * -> *). (Alternative m, TryMerge m) => Bool -> m ()
mrgGuard Bool
True = () -> m ()
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ()
mrgGuard Bool
False = m ()
forall (f :: * -> *) a.
(Alternative f, TryMerge f, Mergeable a) =>
f a
mrgEmpty
{-# INLINE mrgGuard #-}

-- | 'Control.Monad.guard' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation and symbolic conditions.
symGuard :: (SymBranching m, TryMerge m, Alternative m) => SymBool -> m ()
symGuard :: forall (m :: * -> *).
(SymBranching m, TryMerge m, Alternative m) =>
SymBool -> m ()
symGuard SymBool
b = GetBool 'S -> m () -> m () -> m ()
forall (mode :: EvalModeTag) a (m :: * -> *).
(DecideEvalMode mode, Mergeable a, UnifiedBranching mode m) =>
GetBool mode -> m a -> m a -> m a
mrgIf SymBool
GetBool 'S
b (() -> m ()
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ()) m ()
forall (f :: * -> *) a.
(Alternative f, TryMerge f, Mergeable a) =>
f a
mrgEmpty
{-# INLINE symGuard #-}

-- | 'Control.Monad.when' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgWhen :: (Applicative m, TryMerge m) => Bool -> m () -> m ()
mrgWhen :: forall (m :: * -> *).
(Applicative m, TryMerge m) =>
Bool -> m () -> m ()
mrgWhen Bool
True m ()
a = m () -> m ()
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge m ()
a
mrgWhen Bool
False m ()
_ = () -> m ()
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ()
{-# INLINE mrgWhen #-}

-- | 'Control.Monad.when' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation and symbolic conditions.
symWhen ::
  (Applicative m, TryMerge m, SymBranching m) => SymBool -> m () -> m ()
symWhen :: forall (m :: * -> *).
(Applicative m, TryMerge m, SymBranching m) =>
SymBool -> m () -> m ()
symWhen SymBool
b m ()
a = GetBool 'S -> m () -> m () -> m ()
forall (mode :: EvalModeTag) a (m :: * -> *).
(DecideEvalMode mode, Mergeable a, UnifiedBranching mode m) =>
GetBool mode -> m a -> m a -> m a
mrgIf SymBool
GetBool 'S
b m ()
a (() -> m ()
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ())
{-# INLINE symWhen #-}

-- | 'Control.Monad.unless' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgUnless :: (Applicative m, TryMerge m) => Bool -> m () -> m ()
mrgUnless :: forall (m :: * -> *).
(Applicative m, TryMerge m) =>
Bool -> m () -> m ()
mrgUnless Bool
b = Bool -> m () -> m ()
forall (m :: * -> *).
(Applicative m, TryMerge m) =>
Bool -> m () -> m ()
mrgWhen (Bool -> Bool
not Bool
b)
{-# INLINE mrgUnless #-}

-- | 'Control.Monad.unless' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation and symbolic conditions.
symUnless ::
  (Applicative m, TryMerge m, SymBranching m) => SymBool -> m () -> m ()
symUnless :: forall (m :: * -> *).
(Applicative m, TryMerge m, SymBranching m) =>
SymBool -> m () -> m ()
symUnless SymBool
b = SymBool -> m () -> m ()
forall (m :: * -> *).
(Applicative m, TryMerge m, SymBranching m) =>
SymBool -> m () -> m ()
symWhen (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
b)
{-# INLINE symUnless #-}

-- | 'Control.Monad.liftM' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgLiftM ::
  (MonadTryMerge m, Mergeable a, Mergeable b) => (a -> b) -> m a -> m b
mrgLiftM :: forall (m :: * -> *) a b.
(MonadTryMerge m, Mergeable a, Mergeable b) =>
(a -> b) -> m a -> m b
mrgLiftM a -> b
f m a
a = a -> b
f (a -> b) -> m a -> m b
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
.<$> m a
a
{-# INLINE mrgLiftM #-}

-- | 'Control.Monad.liftM2' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgLiftM2 ::
  (MonadTryMerge m, Mergeable a, Mergeable b, Mergeable c) =>
  (a -> b -> c) ->
  m a ->
  m b ->
  m c
mrgLiftM2 :: forall (m :: * -> *) a b c.
(MonadTryMerge m, Mergeable a, Mergeable b, Mergeable c) =>
(a -> b -> c) -> m a -> m b -> m c
mrgLiftM2 a -> b -> c
f m a
a m b
b = a -> b -> c
f (a -> b -> c) -> m a -> m (b -> c)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
.<$> m a
a m (b -> c) -> m b -> m c
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
.<*> m b
b
{-# INLINE mrgLiftM2 #-}

-- | 'Control.Monad.liftM3' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgLiftM3 ::
  (MonadTryMerge m, Mergeable a, Mergeable b, Mergeable c, Mergeable d) =>
  (a -> b -> c -> d) ->
  m a ->
  m b ->
  m c ->
  m d
mrgLiftM3 :: forall (m :: * -> *) a b c d.
(MonadTryMerge m, Mergeable a, Mergeable b, Mergeable c,
 Mergeable d) =>
(a -> b -> c -> d) -> m a -> m b -> m c -> m d
mrgLiftM3 a -> b -> c -> d
f m a
a m b
b m c
c = a -> b -> c -> d
f (a -> b -> c -> d) -> m a -> m (b -> c -> d)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
.<$> m a
a m (b -> c -> d) -> m b -> m (c -> d)
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
.<*> m b
b m (c -> d) -> m c -> m d
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
.<*> m c
c
{-# INLINE mrgLiftM3 #-}

-- | 'Control.Monad.liftM4' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgLiftM4 ::
  ( MonadTryMerge m,
    Mergeable a,
    Mergeable b,
    Mergeable c,
    Mergeable d,
    Mergeable e
  ) =>
  (a -> b -> c -> d -> e) ->
  m a ->
  m b ->
  m c ->
  m d ->
  m e
mrgLiftM4 :: forall (m :: * -> *) a b c d e.
(MonadTryMerge m, Mergeable a, Mergeable b, Mergeable c,
 Mergeable d, Mergeable e) =>
(a -> b -> c -> d -> e) -> m a -> m b -> m c -> m d -> m e
mrgLiftM4 a -> b -> c -> d -> e
f m a
a m b
b m c
c m d
d = a -> b -> c -> d -> e
f (a -> b -> c -> d -> e) -> m a -> m (b -> c -> d -> e)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
.<$> m a
a m (b -> c -> d -> e) -> m b -> m (c -> d -> e)
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
.<*> m b
b m (c -> d -> e) -> m c -> m (d -> e)
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
.<*> m c
c m (d -> e) -> m d -> m e
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
.<*> m d
d
{-# INLINE mrgLiftM4 #-}

-- | 'Control.Monad.liftM5' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgLiftM5 ::
  ( MonadTryMerge m,
    Mergeable a,
    Mergeable b,
    Mergeable c,
    Mergeable d,
    Mergeable e,
    Mergeable f
  ) =>
  (a -> b -> c -> d -> e -> f) ->
  m a ->
  m b ->
  m c ->
  m d ->
  m e ->
  m f
mrgLiftM5 :: forall (m :: * -> *) a b c d e f.
(MonadTryMerge m, Mergeable a, Mergeable b, Mergeable c,
 Mergeable d, Mergeable e, Mergeable f) =>
(a -> b -> c -> d -> e -> f)
-> m a -> m b -> m c -> m d -> m e -> m f
mrgLiftM5 a -> b -> c -> d -> e -> f
f m a
a m b
b m c
c m d
d m e
e = a -> b -> c -> d -> e -> f
f (a -> b -> c -> d -> e -> f) -> m a -> m (b -> c -> d -> e -> f)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
.<$> m a
a m (b -> c -> d -> e -> f) -> m b -> m (c -> d -> e -> f)
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
.<*> m b
b m (c -> d -> e -> f) -> m c -> m (d -> e -> f)
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
.<*> m c
c m (d -> e -> f) -> m d -> m (e -> f)
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
.<*> m d
d m (e -> f) -> m e -> m f
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
.<*> m e
e
{-# INLINE mrgLiftM5 #-}

-- | 'Control.Monad.<*>' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgAp ::
  (MonadTryMerge m, Mergeable a, Mergeable b) => m (a -> b) -> m a -> m b
mrgAp :: forall (m :: * -> *) a b.
(MonadTryMerge m, Mergeable a, Mergeable b) =>
m (a -> b) -> m a -> m b
mrgAp = m (a -> b) -> m a -> m b
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f (a -> b) -> f a -> f b
(.<*>)
{-# INLINE mrgAp #-}

infixl 4 .<$!>

-- | 'Control.Monad.<$!>' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation. Merging is always strict so we can directly use
-- 'Grisette.Internal.Unified.Lib.Data.Functor..<$>'.
(.<$!>) ::
  (MonadTryMerge m, Mergeable a, Mergeable b) => (a -> b) -> m a -> m b
a -> b
f .<$!> :: forall (m :: * -> *) a b.
(MonadTryMerge m, Mergeable a, Mergeable b) =>
(a -> b) -> m a -> m b
.<$!> m a
a = a -> b
f (a -> b) -> m a -> m b
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
.<$> m a
a
{-# INLINE (.<$!>) #-}