{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- |
-- Module      :   Grisette.Unified.Lib.Data.Foldable
-- 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.Data.Foldable
  ( symElem,
    symMaximum,
    mrgMaximum,
    symMinimum,
    mrgMinimum,

    -- * Special biased folds
    mrgFoldrM,
    mrgFoldlM,

    -- * Folding actions

    -- ** Applicative actions
    mrgTraverse_,
    mrgFor_,
    mrgSequenceA_,
    mrgAsum,

    -- ** Monadic actions
    mrgMapM_,
    mrgForM_,
    mrgSequence_,
    mrgMsum,

    -- * Folding actions
    symAnd,
    symOr,
    symAny,
    symAll,
    symMaximumBy,
    mrgMaximumBy,
    symMinimumBy,
    mrgMinimumBy,

    -- ** Searches
    symNotElem,
    mrgFind,
  )
where

import Control.Monad (MonadPlus)
import Data.Foldable (Foldable (foldl'))
import Grisette.Internal.Core.Data.Class.LogicalOp
  ( LogicalOp (symNot, (.&&), (.||)),
  )
import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)
import Grisette.Internal.Core.Data.Class.ToSym (ToSym (toSym))
import Grisette.Internal.Core.Data.Class.TryMerge
  ( MonadTryMerge,
    TryMerge,
    mrgSingle,
    tryMerge,
  )
import Grisette.Unified
  ( MonadWithMode,
    UnifiedITEOp,
    UnifiedSymOrd,
    liftBaseMonad,
    mrgIf,
    symIteMerge,
  )
import Grisette.Unified.Internal.BaseMonad (BaseMonad)
import Grisette.Unified.Internal.Class.UnifiedSymEq (UnifiedSymEq, (.==))
import Grisette.Unified.Internal.Class.UnifiedSymOrd (mrgMax, mrgMin)
import Grisette.Unified.Internal.EvalMode (EvalMode)
import Grisette.Unified.Internal.UnifiedBool (GetBool)
import Grisette.Unified.Lib.Control.Applicative (mrgAsum, mrgPure, (.*>))
import {-# SOURCE #-} Grisette.Unified.Lib.Control.Monad
  ( mrgMplus,
    mrgMzero,
    (.>>),
  )
import Grisette.Unified.Lib.Data.Functor (mrgFmap, mrgVoid)

-- | 'Data.Foldable.elem' with symbolic equality.
symElem ::
  forall mode t a.
  (Foldable t, EvalMode mode, UnifiedSymEq mode a) =>
  a ->
  t a ->
  GetBool mode
symElem :: forall (mode :: EvalModeTag) (t :: * -> *) a.
(Foldable t, EvalMode mode, UnifiedSymEq mode a) =>
a -> t a -> GetBool mode
symElem a
x = (a -> GetBool mode) -> t a -> GetBool mode
forall (mode :: EvalModeTag) (t :: * -> *) a.
(EvalMode mode, Foldable t) =>
(a -> GetBool mode) -> t a -> GetBool mode
symAny ((a -> a -> GetBool mode
forall (mode :: EvalModeTag) a.
(Typeable mode, UnifiedSymEq mode a) =>
a -> a -> GetBool mode
.== a
x))
{-# INLINE symElem #-}

-- | 'Data.Foldable.maximum' with unified comparison.
mrgMaximum ::
  forall mode a t m.
  (Foldable t, MonadWithMode mode m, Mergeable a, UnifiedSymOrd mode a) =>
  t a ->
  m a
mrgMaximum :: forall (mode :: EvalModeTag) a (t :: * -> *) (m :: * -> *).
(Foldable t, MonadWithMode mode m, Mergeable a,
 UnifiedSymOrd mode a) =>
t a -> m a
mrgMaximum t a
l = do
  Maybe a
r <- (Maybe a -> a -> m (Maybe a)) -> Maybe a -> t a -> m (Maybe a)
forall (m :: * -> *) b (t :: * -> *) a.
(MonadTryMerge m, Mergeable b, Foldable t) =>
(b -> a -> m b) -> b -> t a -> m b
mrgFoldlM Maybe a -> a -> m (Maybe a)
symMax' (Maybe a
forall a. Maybe a
Nothing :: Maybe a) t a
l
  case Maybe a
r of
    Maybe a
Nothing -> [Char] -> m a
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"mrgMaximum: empty structure"
    Just a
x -> a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure a
x
  where
    symMax' :: Maybe a -> a -> m (Maybe a)
    symMax' :: Maybe a -> a -> m (Maybe a)
symMax' Maybe a
mx a
y =
      case Maybe a
mx of
        Maybe a
Nothing -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
y
        Just a
x -> (a -> Maybe a) -> m a -> m (Maybe a)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap a -> Maybe a
forall a. a -> Maybe a
Just (m a -> m (Maybe a)) -> m a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a (m :: * -> *).
(UnifiedSymOrd mode a, UnifiedBranching mode m, Typeable mode,
 Applicative m, Mergeable a) =>
a -> a -> m a
mrgMax @mode a
x a
y
{-# INLINE mrgMaximum #-}

-- | 'Data.Foldable.maximum' with result merged with 'Grisette.Core.ITEOp'.
symMaximum ::
  forall mode a t.
  ( Foldable t,
    Mergeable a,
    UnifiedSymOrd mode a,
    UnifiedITEOp mode a,
    EvalMode mode
  ) =>
  t a ->
  a
symMaximum :: forall (mode :: EvalModeTag) a (t :: * -> *).
(Foldable t, Mergeable a, UnifiedSymOrd mode a,
 UnifiedITEOp mode a, EvalMode mode) =>
t a -> a
symMaximum t a
l = BaseMonad mode a -> a
forall (mode :: EvalModeTag) v.
(Typeable mode, UnifiedITEOp mode v, Mergeable v) =>
BaseMonad mode v -> v
symIteMerge (forall (mode :: EvalModeTag) a (t :: * -> *) (m :: * -> *).
(Foldable t, MonadWithMode mode m, Mergeable a,
 UnifiedSymOrd mode a) =>
t a -> m a
mrgMaximum @mode t a
l :: BaseMonad mode a)
{-# INLINE symMaximum #-}

-- | 'Data.Foldable.minimum' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgMinimum ::
  forall mode a t m.
  (Foldable t, MonadWithMode mode m, Mergeable a, UnifiedSymOrd mode a) =>
  t a ->
  m a
mrgMinimum :: forall (mode :: EvalModeTag) a (t :: * -> *) (m :: * -> *).
(Foldable t, MonadWithMode mode m, Mergeable a,
 UnifiedSymOrd mode a) =>
t a -> m a
mrgMinimum t a
l = do
  Maybe a
r <- (Maybe a -> a -> m (Maybe a)) -> Maybe a -> t a -> m (Maybe a)
forall (m :: * -> *) b (t :: * -> *) a.
(MonadTryMerge m, Mergeable b, Foldable t) =>
(b -> a -> m b) -> b -> t a -> m b
mrgFoldlM Maybe a -> a -> m (Maybe a)
symMin' (Maybe a
forall a. Maybe a
Nothing :: Maybe a) t a
l
  case Maybe a
r of
    Maybe a
Nothing -> [Char] -> m a
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"mrgMinimum: empty structure"
    Just a
x -> a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure a
x
  where
    symMin' :: Maybe a -> a -> m (Maybe a)
    symMin' :: Maybe a -> a -> m (Maybe a)
symMin' Maybe a
mx a
y =
      case Maybe a
mx of
        Maybe a
Nothing -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
y
        Just a
x -> (a -> Maybe a) -> m a -> m (Maybe a)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap a -> Maybe a
forall a. a -> Maybe a
Just (m a -> m (Maybe a)) -> m a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a (m :: * -> *).
(UnifiedSymOrd mode a, UnifiedBranching mode m, Typeable mode,
 Applicative m, Mergeable a) =>
a -> a -> m a
mrgMin @mode a
x a
y

-- | 'Data.Foldable.maximum' with result merged with 'Grisette.Core.ITEOp'.
symMinimum ::
  forall mode a t.
  ( Foldable t,
    Mergeable a,
    UnifiedSymOrd mode a,
    UnifiedITEOp mode a,
    EvalMode mode
  ) =>
  t a ->
  a
symMinimum :: forall (mode :: EvalModeTag) a (t :: * -> *).
(Foldable t, Mergeable a, UnifiedSymOrd mode a,
 UnifiedITEOp mode a, EvalMode mode) =>
t a -> a
symMinimum t a
l = BaseMonad mode a -> a
forall (mode :: EvalModeTag) v.
(Typeable mode, UnifiedITEOp mode v, Mergeable v) =>
BaseMonad mode v -> v
symIteMerge (forall (mode :: EvalModeTag) a (t :: * -> *) (m :: * -> *).
(Foldable t, MonadWithMode mode m, Mergeable a,
 UnifiedSymOrd mode a) =>
t a -> m a
mrgMinimum @mode t a
l :: BaseMonad mode a)
{-# INLINE symMinimum #-}

-- | 'Data.Foldable.foldrM' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgFoldrM ::
  (MonadTryMerge m, Mergeable b, Foldable t) =>
  (a -> b -> m b) ->
  b ->
  t a ->
  m b
mrgFoldrM :: forall (m :: * -> *) b (t :: * -> *) a.
(MonadTryMerge m, Mergeable b, Foldable t) =>
(a -> b -> m b) -> b -> t a -> m b
mrgFoldrM a -> b -> m b
f b
z0 t a
xs = ((b -> m b) -> a -> b -> m b) -> (b -> m b) -> t a -> b -> m b
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (b -> m b) -> a -> b -> m b
c b -> m b
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure t a
xs b
z0
  where
    c :: (b -> m b) -> a -> b -> m b
c b -> m b
k a
x b
z = m b -> m b
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (a -> b -> m b
f a
x b
z) m b -> (b -> m b) -> m b
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 b
k
{-# INLINE mrgFoldrM #-}

-- | 'Data.Foldable.foldlM' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgFoldlM ::
  (MonadTryMerge m, Mergeable b, Foldable t) =>
  (b -> a -> m b) ->
  b ->
  t a ->
  m b
mrgFoldlM :: 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
z0 t a
xs = (a -> (b -> m b) -> b -> m b) -> (b -> m b) -> t a -> b -> m b
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 -> (b -> m b) -> b -> m b
c b -> m b
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure t a
xs b
z0
  where
    c :: a -> (b -> m b) -> b -> m b
c a
x b -> m b
k b
z = m b -> m b
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (b -> a -> m b
f b
z a
x) m b -> (b -> m b) -> m b
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 b
k
{-# INLINE mrgFoldlM #-}

-- | 'Data.Foldable.traverse_' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgTraverse_ ::
  (Applicative m, TryMerge m, Foldable t) => (a -> m b) -> t a -> m ()
mrgTraverse_ :: forall (m :: * -> *) (t :: * -> *) a b.
(Applicative m, TryMerge m, Foldable t) =>
(a -> m b) -> t a -> m ()
mrgTraverse_ a -> m b
f = (a -> m () -> m ()) -> m () -> t a -> m ()
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 -> m () -> m ()
c (() -> m ()
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ())
  where
    c :: a -> m () -> m ()
c a
x m ()
k = m b -> m ()
forall (f :: * -> *) a. (TryMerge f, Functor f) => f a -> f ()
mrgVoid (a -> m b
f a
x) m () -> m () -> m ()
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f a -> f b -> f b
.*> m ()
k
{-# INLINE mrgTraverse_ #-}

-- | 'Data.Foldable.for_' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgFor_ ::
  (Applicative m, TryMerge m, Foldable t) => t a -> (a -> m b) -> m ()
mrgFor_ :: forall (m :: * -> *) (t :: * -> *) a b.
(Applicative m, TryMerge m, Foldable t) =>
t a -> (a -> m b) -> m ()
mrgFor_ = ((a -> m b) -> t a -> m ()) -> t a -> (a -> m b) -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> m b) -> t a -> m ()
forall (m :: * -> *) (t :: * -> *) a b.
(Applicative m, TryMerge m, Foldable t) =>
(a -> m b) -> t a -> m ()
mrgTraverse_
{-# INLINE mrgFor_ #-}

-- | 'Data.Foldable.sequence_' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgSequenceA_ ::
  (Foldable t, TryMerge m, Applicative m) => t (m a) -> m ()
mrgSequenceA_ :: forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, TryMerge m, Applicative m) =>
t (m a) -> m ()
mrgSequenceA_ = (m a -> m () -> m ()) -> m () -> t (m a) -> m ()
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr m a -> m () -> m ()
forall {f :: * -> *} {b} {a}.
(Applicative f, Mergeable b, TryMerge f) =>
f a -> f b -> f b
c (() -> m ()
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ())
  where
    c :: f a -> f b -> f b
c f a
m f b
k = f a -> f ()
forall (f :: * -> *) a. (TryMerge f, Functor f) => f a -> f ()
mrgVoid f a
m f () -> f b -> f b
forall (f :: * -> *) a b.
(Applicative f, TryMerge f, Mergeable a, Mergeable b) =>
f a -> f b -> f b
.*> f b
k
{-# INLINE mrgSequenceA_ #-}

-- | 'Data.Foldable.mapM_' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgMapM_ :: (MonadTryMerge m, Foldable t) => (a -> m b) -> t a -> m ()
mrgMapM_ :: forall (m :: * -> *) (t :: * -> *) a b.
(MonadTryMerge m, Foldable t) =>
(a -> m b) -> t a -> m ()
mrgMapM_ = (a -> m b) -> t a -> m ()
forall (m :: * -> *) (t :: * -> *) a b.
(Applicative m, TryMerge m, Foldable t) =>
(a -> m b) -> t a -> m ()
mrgTraverse_
{-# INLINE mrgMapM_ #-}

-- | 'Data.Foldable.forM_' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgForM_ :: (MonadTryMerge m, Foldable t) => t a -> (a -> m b) -> m ()
mrgForM_ :: forall (m :: * -> *) (t :: * -> *) a b.
(MonadTryMerge m, Foldable t) =>
t a -> (a -> m b) -> m ()
mrgForM_ = ((a -> m b) -> t a -> m ()) -> t a -> (a -> m b) -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> m b) -> t a -> m ()
forall (m :: * -> *) (t :: * -> *) a b.
(MonadTryMerge m, Foldable t) =>
(a -> m b) -> t a -> m ()
mrgMapM_
{-# INLINE mrgForM_ #-}

-- | 'Data.Foldable.sequence_' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgSequence_ :: (Foldable t, MonadTryMerge m) => t (m a) -> m ()
mrgSequence_ :: forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadTryMerge m) =>
t (m a) -> m ()
mrgSequence_ = (m a -> m () -> m ()) -> m () -> t (m a) -> m ()
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr m a -> m () -> m ()
forall {m :: * -> *} {b} {a}.
(Monad m, Mergeable b, TryMerge m) =>
m a -> m b -> m b
c (() -> m ()
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ())
  where
    c :: m a -> m b -> m b
c m a
m m b
k = m a -> m ()
forall (f :: * -> *) a. (TryMerge f, Functor f) => f a -> f ()
mrgVoid m a
m m () -> m b -> m b
forall (m :: * -> *) a b.
(MonadTryMerge m, Mergeable a, Mergeable b) =>
m a -> m b -> m b
.>> m b
k
{-# INLINE mrgSequence_ #-}

-- | 'Data.Foldable.msum' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgMsum ::
  (MonadTryMerge m, Mergeable a, MonadPlus m, Foldable t) => t (m a) -> m a
mrgMsum :: forall (m :: * -> *) a (t :: * -> *).
(MonadTryMerge m, Mergeable a, MonadPlus m, Foldable t) =>
t (m a) -> m a
mrgMsum = (m a -> m a -> m a) -> m a -> t (m 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 m a -> m a -> m a
forall (m :: * -> *) a.
(MonadTryMerge m, Mergeable a, MonadPlus m) =>
m a -> m a -> m a
mrgMplus m a
forall (m :: * -> *) a.
(MonadTryMerge m, Mergeable a, MonadPlus m) =>
m a
mrgMzero
{-# INLINE mrgMsum #-}

-- | 'Data.Foldable.and' on unified boolean.
symAnd :: (EvalMode mode, Foldable t) => t (GetBool mode) -> GetBool mode
symAnd :: forall (mode :: EvalModeTag) (t :: * -> *).
(EvalMode mode, Foldable t) =>
t (GetBool mode) -> GetBool mode
symAnd = (GetBool mode -> GetBool mode -> GetBool mode)
-> GetBool mode -> t (GetBool mode) -> GetBool mode
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' GetBool mode -> GetBool mode -> GetBool mode
forall b. LogicalOp b => b -> b -> b
(.&&) (Bool -> GetBool mode
forall a b. ToSym a b => a -> b
toSym Bool
True)
{-# INLINE symAnd #-}

-- | 'Data.Foldable.or' on unified boolean.
symOr :: (EvalMode mode, Foldable t) => t (GetBool mode) -> GetBool mode
symOr :: forall (mode :: EvalModeTag) (t :: * -> *).
(EvalMode mode, Foldable t) =>
t (GetBool mode) -> GetBool mode
symOr = (GetBool mode -> GetBool mode -> GetBool mode)
-> GetBool mode -> t (GetBool mode) -> GetBool mode
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' GetBool mode -> GetBool mode -> GetBool mode
forall b. LogicalOp b => b -> b -> b
(.||) (Bool -> GetBool mode
forall a b. ToSym a b => a -> b
toSym Bool
False)
{-# INLINE symOr #-}

-- | 'Data.Foldable.any' on unified boolean.
symAny ::
  (EvalMode mode, Foldable t) => (a -> GetBool mode) -> t a -> GetBool mode
symAny :: forall (mode :: EvalModeTag) (t :: * -> *) a.
(EvalMode mode, Foldable t) =>
(a -> GetBool mode) -> t a -> GetBool mode
symAny a -> GetBool mode
f = (GetBool mode -> a -> GetBool mode)
-> GetBool mode -> t a -> GetBool mode
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\GetBool mode
acc a
v -> GetBool mode
acc GetBool mode -> GetBool mode -> GetBool mode
forall b. LogicalOp b => b -> b -> b
.|| a -> GetBool mode
f a
v) (Bool -> GetBool mode
forall a b. ToSym a b => a -> b
toSym Bool
False)
{-# INLINE symAny #-}

-- | 'Data.Foldable.all' on unified boolean.
symAll ::
  (EvalMode mode, Foldable t) => (a -> GetBool mode) -> t a -> GetBool mode
symAll :: forall (mode :: EvalModeTag) (t :: * -> *) a.
(EvalMode mode, Foldable t) =>
(a -> GetBool mode) -> t a -> GetBool mode
symAll a -> GetBool mode
f = (GetBool mode -> a -> GetBool mode)
-> GetBool mode -> t a -> GetBool mode
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\GetBool mode
acc a
v -> GetBool mode
acc GetBool mode -> GetBool mode -> GetBool mode
forall b. LogicalOp b => b -> b -> b
.&& a -> GetBool mode
f a
v) (Bool -> GetBool mode
forall a b. ToSym a b => a -> b
toSym Bool
True)
{-# INLINE symAll #-}

-- | 'Data.Foldable.maximumBy' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgMaximumBy ::
  forall mode t a m.
  (Foldable t, Mergeable a, MonadWithMode mode m) =>
  (a -> a -> BaseMonad mode Ordering) ->
  t a ->
  m a
mrgMaximumBy :: forall (mode :: EvalModeTag) (t :: * -> *) a (m :: * -> *).
(Foldable t, Mergeable a, MonadWithMode mode m) =>
(a -> a -> BaseMonad mode Ordering) -> t a -> m a
mrgMaximumBy a -> a -> BaseMonad mode Ordering
cmp t a
l = do
  Maybe a
r <- (Maybe a -> a -> m (Maybe a)) -> Maybe a -> t a -> m (Maybe a)
forall (m :: * -> *) b (t :: * -> *) a.
(MonadTryMerge m, Mergeable b, Foldable t) =>
(b -> a -> m b) -> b -> t a -> m b
mrgFoldlM Maybe a -> a -> m (Maybe a)
symMax' (Maybe a
forall a. Maybe a
Nothing :: Maybe a) t a
l
  case Maybe a
r of
    Maybe a
Nothing -> [Char] -> m a
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"mrgMaximumBy: empty structure"
    Just a
x -> a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
x
  where
    symMax' :: Maybe a -> a -> m (Maybe a)
    symMax' :: Maybe a -> a -> m (Maybe a)
symMax' Maybe a
mx a
y =
      case Maybe a
mx of
        Maybe a
Nothing -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
y
        Just a
x -> do
          Ordering
cmpRes <- BaseMonad mode Ordering -> m Ordering
forall (mode :: EvalModeTag) a (m :: * -> *).
(Applicative m, UnifiedBranching mode m, Mergeable a) =>
BaseMonad mode a -> m a
liftBaseMonad (BaseMonad mode Ordering -> m Ordering)
-> BaseMonad mode Ordering -> m Ordering
forall a b. (a -> b) -> a -> b
$ a -> a -> BaseMonad mode Ordering
cmp a
x a
y
          case Ordering
cmpRes of
            Ordering
GT -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
x
            Ordering
_ -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
y

-- | 'Data.Foldable.maximumBy' with result merged with 'Grisette.Core.ITEOp'.
symMaximumBy ::
  forall mode t a.
  (Foldable t, Mergeable a, UnifiedITEOp mode a, EvalMode mode) =>
  (a -> a -> BaseMonad mode Ordering) ->
  t a ->
  a
symMaximumBy :: forall (mode :: EvalModeTag) (t :: * -> *) a.
(Foldable t, Mergeable a, UnifiedITEOp mode a, EvalMode mode) =>
(a -> a -> BaseMonad mode Ordering) -> t a -> a
symMaximumBy a -> a -> BaseMonad mode Ordering
cmp t a
l = BaseMonad mode a -> a
forall (mode :: EvalModeTag) v.
(Typeable mode, UnifiedITEOp mode v, Mergeable v) =>
BaseMonad mode v -> v
symIteMerge ((a -> a -> BaseMonad mode Ordering) -> t a -> BaseMonad mode a
forall (mode :: EvalModeTag) (t :: * -> *) a (m :: * -> *).
(Foldable t, Mergeable a, MonadWithMode mode m) =>
(a -> a -> BaseMonad mode Ordering) -> t a -> m a
mrgMaximumBy a -> a -> BaseMonad mode Ordering
cmp t a
l :: BaseMonad mode a)
{-# INLINE symMaximumBy #-}

-- | 'Data.Foldable.minimumBy' with 'Grisette.Core.MergingStrategy' knowledge
-- propagation.
mrgMinimumBy ::
  forall mode t a m.
  (Foldable t, Mergeable a, MonadWithMode mode m) =>
  (a -> a -> BaseMonad mode Ordering) ->
  t a ->
  m a
mrgMinimumBy :: forall (mode :: EvalModeTag) (t :: * -> *) a (m :: * -> *).
(Foldable t, Mergeable a, MonadWithMode mode m) =>
(a -> a -> BaseMonad mode Ordering) -> t a -> m a
mrgMinimumBy a -> a -> BaseMonad mode Ordering
cmp t a
l = do
  Maybe a
r <- (Maybe a -> a -> m (Maybe a)) -> Maybe a -> t a -> m (Maybe a)
forall (m :: * -> *) b (t :: * -> *) a.
(MonadTryMerge m, Mergeable b, Foldable t) =>
(b -> a -> m b) -> b -> t a -> m b
mrgFoldlM Maybe a -> a -> m (Maybe a)
symMin' (Maybe a
forall a. Maybe a
Nothing :: Maybe a) t a
l
  case Maybe a
r of
    Maybe a
Nothing -> [Char] -> m a
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"mrgMinimumBy: empty structure"
    Just a
x -> a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
x
  where
    symMin' :: Maybe a -> a -> m (Maybe a)
    symMin' :: Maybe a -> a -> m (Maybe a)
symMin' Maybe a
mx a
y =
      case Maybe a
mx of
        Maybe a
Nothing -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
y
        Just a
x -> do
          Ordering
cmpRes <- BaseMonad mode Ordering -> m Ordering
forall (mode :: EvalModeTag) a (m :: * -> *).
(Applicative m, UnifiedBranching mode m, Mergeable a) =>
BaseMonad mode a -> m a
liftBaseMonad (BaseMonad mode Ordering -> m Ordering)
-> BaseMonad mode Ordering -> m Ordering
forall a b. (a -> b) -> a -> b
$ a -> a -> BaseMonad mode Ordering
cmp a
x a
y
          case Ordering
cmpRes of
            Ordering
GT -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
y
            Ordering
_ -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
x

-- | 'Data.Foldable.minimumBy' with result merged with 'Grisette.Core.ITEOp'.
symMinimumBy ::
  forall mode t a.
  (Foldable t, Mergeable a, UnifiedITEOp mode a, EvalMode mode) =>
  (a -> a -> BaseMonad mode Ordering) ->
  t a ->
  a
symMinimumBy :: forall (mode :: EvalModeTag) (t :: * -> *) a.
(Foldable t, Mergeable a, UnifiedITEOp mode a, EvalMode mode) =>
(a -> a -> BaseMonad mode Ordering) -> t a -> a
symMinimumBy a -> a -> BaseMonad mode Ordering
cmp t a
l = BaseMonad mode a -> a
forall (mode :: EvalModeTag) v.
(Typeable mode, UnifiedITEOp mode v, Mergeable v) =>
BaseMonad mode v -> v
symIteMerge ((a -> a -> BaseMonad mode Ordering) -> t a -> BaseMonad mode a
forall (mode :: EvalModeTag) (t :: * -> *) a (m :: * -> *).
(Foldable t, Mergeable a, MonadWithMode mode m) =>
(a -> a -> BaseMonad mode Ordering) -> t a -> m a
mrgMinimumBy a -> a -> BaseMonad mode Ordering
cmp t a
l :: BaseMonad mode a)
{-# INLINE symMinimumBy #-}

-- | 'Data.Foldable.elem' with symbolic equality.
symNotElem ::
  (Foldable t, UnifiedSymEq mode a, EvalMode mode) =>
  a ->
  t a ->
  GetBool mode
symNotElem :: forall (t :: * -> *) (mode :: EvalModeTag) a.
(Foldable t, UnifiedSymEq mode a, EvalMode mode) =>
a -> t a -> GetBool mode
symNotElem a
x = GetBool mode -> GetBool mode
forall b. LogicalOp b => b -> b
symNot (GetBool mode -> GetBool mode)
-> (t a -> GetBool mode) -> t a -> GetBool mode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> t a -> GetBool mode
forall (mode :: EvalModeTag) (t :: * -> *) a.
(Foldable t, EvalMode mode, UnifiedSymEq mode a) =>
a -> t a -> GetBool mode
symElem a
x
{-# INLINE symNotElem #-}

-- | 'Data.Foldable.elem' with symbolic equality and
-- 'Grisette.Core.MergingStrategy' knowledge propagation.
mrgFind ::
  (Foldable t, MonadWithMode mode m, Mergeable a) =>
  (a -> GetBool mode) ->
  t a ->
  m (Maybe a)
mrgFind :: forall (t :: * -> *) (mode :: EvalModeTag) (m :: * -> *) a.
(Foldable t, MonadWithMode mode m, Mergeable a) =>
(a -> GetBool mode) -> t a -> m (Maybe a)
mrgFind a -> GetBool mode
f = (Maybe a -> a -> m (Maybe a)) -> Maybe a -> t a -> m (Maybe a)
forall (m :: * -> *) b (t :: * -> *) a.
(MonadTryMerge m, Mergeable b, Foldable t) =>
(b -> a -> m b) -> b -> t a -> m b
mrgFoldlM Maybe a -> a -> m (Maybe a)
fst (Maybe a
forall a. Maybe a
Nothing :: Maybe a)
  where
    fst :: Maybe a -> a -> m (Maybe a)
fst Maybe a
acc a
v = do
      case Maybe a
acc of
        Just a
_ -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure Maybe a
acc
        Maybe a
Nothing -> do
          GetBool mode -> m (Maybe a) -> m (Maybe a) -> m (Maybe a)
forall (mode :: EvalModeTag) a (m :: * -> *).
(Typeable mode, Mergeable a, UnifiedBranching mode m) =>
GetBool mode -> m a -> m a -> m a
mrgIf (a -> GetBool mode
f a
v) (Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
v) (Maybe a -> m (Maybe a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure Maybe a
forall a. Maybe a
Nothing)