    -----------------------------------------------------------------------
    -- |
    -- Module           : What4.LabeledPred
    -- Description      : Predicates with some metadata (a tag or label).
    -- Copyright        : (c) Galois, Inc 2019-2020
    -- License          : BSD3
    -- Maintainer       : Langston Barrett <langston@galois.com>
    -- Stability        : provisional
    --
    -- Predicates alone do not record their semantic content, thus it is often
    -- useful to attach some sort of descriptor to them.
    ------------------------------------------------------------------------

    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE DeriveFoldable #-}
    {-# LANGUAGE DeriveFunctor #-}
    {-# LANGUAGE DeriveTraversable #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE TemplateHaskell #-}

    module What4.LabeledPred
      ( LabeledPred(..)
      , labeledPred
      , labeledPredMsg
      , partitionByPreds
      , partitionByPredsM
      , partitionLabeledPreds
      ) where

    import Control.Lens
    import Data.Bifunctor.TH (deriveBifunctor, deriveBifoldable, deriveBitraversable)
    import Data.Data (Data)
    import Data.Coerce (coerce)
    import Data.Data (Typeable)
    import Data.Eq.Deriving (deriveEq1, deriveEq2)
    import Data.Foldable (foldrM)
    import Data.Ord.Deriving (deriveOrd1, deriveOrd2)
    import GHC.Generics (Generic, Generic1)
    import Text.Show.Deriving (deriveShow1, deriveShow2)

    import What4.Interface (IsExprBuilder, Pred, asConstantPred)

    -- | Information about an assertion that was previously made.
    data LabeledPred pred msg
       = LabeledPred
         { -- | Predicate that was asserted.
           forall pred msg. LabeledPred pred msg -> pred
    _labeledPred    :: !pred
           -- | Message added when assumption/assertion was made.
         , forall pred msg. LabeledPred pred msg -> msg
    _labeledPredMsg :: !msg
         }
       deriving (LabeledPred pred msg -> LabeledPred pred msg -> Bool
    (LabeledPred pred msg -> LabeledPred pred msg -> Bool)
    -> (LabeledPred pred msg -> LabeledPred pred msg -> Bool)
    -> Eq (LabeledPred pred msg)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall pred msg.
    (Eq pred, Eq msg) =>
    LabeledPred pred msg -> LabeledPred pred msg -> Bool
    $c== :: forall pred msg.
    (Eq pred, Eq msg) =>
    LabeledPred pred msg -> LabeledPred pred msg -> Bool
    == :: LabeledPred pred msg -> LabeledPred pred msg -> Bool
    $c/= :: forall pred msg.
    (Eq pred, Eq msg) =>
    LabeledPred pred msg -> LabeledPred pred msg -> Bool
    /= :: LabeledPred pred msg -> LabeledPred pred msg -> Bool
    Eq, Typeable (LabeledPred pred msg)
    Typeable (LabeledPred pred msg) =>
    (forall (c :: Type -> Type).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g)
     -> LabeledPred pred msg
     -> c (LabeledPred pred msg))
    -> (forall (c :: Type -> Type).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c (LabeledPred pred msg))
    -> (LabeledPred pred msg -> Constr)
    -> (LabeledPred pred msg -> DataType)
    -> (forall (t :: Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c (LabeledPred pred msg)))
    -> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c (LabeledPred pred msg)))
    -> ((forall b. Data b => b -> b)
        -> LabeledPred pred msg -> LabeledPred pred msg)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r)
    -> (forall u.
        (forall d. Data d => d -> u) -> LabeledPred pred msg -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> LabeledPred pred msg -> u)
    -> (forall (m :: Type -> Type).
        Monad m =>
        (forall d. Data d => d -> m d)
        -> LabeledPred pred msg -> m (LabeledPred pred msg))
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> LabeledPred pred msg -> m (LabeledPred pred msg))
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> LabeledPred pred msg -> m (LabeledPred pred msg))
    -> Data (LabeledPred pred msg)
    LabeledPred pred msg -> Constr
    LabeledPred pred msg -> DataType
    (forall b. Data b => b -> b)
    -> LabeledPred pred msg -> LabeledPred pred msg
    forall a.
    Typeable a =>
    (forall (c :: Type -> Type).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: Type -> Type).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: Type -> Type).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u.
    Int -> (forall d. Data d => d -> u) -> LabeledPred pred msg -> u
    forall u.
    (forall d. Data d => d -> u) -> LabeledPred pred msg -> [u]
    forall pred msg.
    (Data pred, Data msg) =>
    Typeable (LabeledPred pred msg)
    forall pred msg.
    (Data pred, Data msg) =>
    LabeledPred pred msg -> Constr
    forall pred msg.
    (Data pred, Data msg) =>
    LabeledPred pred msg -> DataType
    forall pred msg.
    (Data pred, Data msg) =>
    (forall b. Data b => b -> b)
    -> LabeledPred pred msg -> LabeledPred pred msg
    forall pred msg u.
    (Data pred, Data msg) =>
    Int -> (forall d. Data d => d -> u) -> LabeledPred pred msg -> u
    forall pred msg u.
    (Data pred, Data msg) =>
    (forall d. Data d => d -> u) -> LabeledPred pred msg -> [u]
    forall pred msg r r'.
    (Data pred, Data msg) =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r
    forall pred msg r r'.
    (Data pred, Data msg) =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r
    forall pred msg (m :: Type -> Type).
    (Data pred, Data msg, Monad m) =>
    (forall d. Data d => d -> m d)
    -> LabeledPred pred msg -> m (LabeledPred pred msg)
    forall pred msg (m :: Type -> Type).
    (Data pred, Data msg, MonadPlus m) =>
    (forall d. Data d => d -> m d)
    -> LabeledPred pred msg -> m (LabeledPred pred msg)
    forall pred msg (c :: Type -> Type).
    (Data pred, Data msg) =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (LabeledPred pred msg)
    forall pred msg (c :: Type -> Type).
    (Data pred, Data msg) =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> LabeledPred pred msg
    -> c (LabeledPred pred msg)
    forall pred msg (t :: Type -> Type) (c :: Type -> Type).
    (Data pred, Data msg, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (LabeledPred pred msg))
    forall pred msg (t :: Type -> Type -> Type) (c :: Type -> Type).
    (Data pred, Data msg, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (LabeledPred pred msg))
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r
    forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> LabeledPred pred msg -> m (LabeledPred pred msg)
    forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LabeledPred pred msg -> m (LabeledPred pred msg)
    forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (LabeledPred pred msg)
    forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> LabeledPred pred msg
    -> c (LabeledPred pred msg)
    forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (LabeledPred pred msg))
    forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (LabeledPred pred msg))
    $cgfoldl :: forall pred msg (c :: Type -> Type).
    (Data pred, Data msg) =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> LabeledPred pred msg
    -> c (LabeledPred pred msg)
    gfoldl :: forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> LabeledPred pred msg
    -> c (LabeledPred pred msg)
    $cgunfold :: forall pred msg (c :: Type -> Type).
    (Data pred, Data msg) =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (LabeledPred pred msg)
    gunfold :: forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (LabeledPred pred msg)
    $ctoConstr :: forall pred msg.
    (Data pred, Data msg) =>
    LabeledPred pred msg -> Constr
    toConstr :: LabeledPred pred msg -> Constr
    $cdataTypeOf :: forall pred msg.
    (Data pred, Data msg) =>
    LabeledPred pred msg -> DataType
    dataTypeOf :: LabeledPred pred msg -> DataType
    $cdataCast1 :: forall pred msg (t :: Type -> Type) (c :: Type -> Type).
    (Data pred, Data msg, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (LabeledPred pred msg))
    dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (LabeledPred pred msg))
    $cdataCast2 :: forall pred msg (t :: Type -> Type -> Type) (c :: Type -> Type).
    (Data pred, Data msg, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (LabeledPred pred msg))
    dataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (LabeledPred pred msg))
    $cgmapT :: forall pred msg.
    (Data pred, Data msg) =>
    (forall b. Data b => b -> b)
    -> LabeledPred pred msg -> LabeledPred pred msg
    gmapT :: (forall b. Data b => b -> b)
    -> LabeledPred pred msg -> LabeledPred pred msg
    $cgmapQl :: forall pred msg r r'.
    (Data pred, Data msg) =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r
    $cgmapQr :: forall pred msg r r'.
    (Data pred, Data msg) =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r
    $cgmapQ :: forall pred msg u.
    (Data pred, Data msg) =>
    (forall d. Data d => d -> u) -> LabeledPred pred msg -> [u]
    gmapQ :: forall u.
    (forall d. Data d => d -> u) -> LabeledPred pred msg -> [u]
    $cgmapQi :: forall pred msg u.
    (Data pred, Data msg) =>
    Int -> (forall d. Data d => d -> u) -> LabeledPred pred msg -> u
    gmapQi :: forall u.
    Int -> (forall d. Data d => d -> u) -> LabeledPred pred msg -> u
    $cgmapM :: forall pred msg (m :: Type -> Type).
    (Data pred, Data msg, Monad m) =>
    (forall d. Data d => d -> m d)
    -> LabeledPred pred msg -> m (LabeledPred pred msg)
    gmapM :: forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> LabeledPred pred msg -> m (LabeledPred pred msg)
    $cgmapMp :: forall pred msg (m :: Type -> Type).
    (Data pred, Data msg, MonadPlus m) =>
    (forall d. Data d => d -> m d)
    -> LabeledPred pred msg -> m (LabeledPred pred msg)
    gmapMp :: forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LabeledPred pred msg -> m (LabeledPred pred msg)
    $cgmapMo :: forall pred msg (m :: Type -> Type).
    (Data pred, Data msg, MonadPlus m) =>
    (forall d. Data d => d -> m d)
    -> LabeledPred pred msg -> m (LabeledPred pred msg)
    gmapMo :: forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LabeledPred pred msg -> m (LabeledPred pred msg)
    Data, (forall a b. (a -> b) -> LabeledPred pred a -> LabeledPred pred b)
    -> (forall a b. a -> LabeledPred pred b -> LabeledPred pred a)
    -> Functor (LabeledPred pred)
    forall a b. a -> LabeledPred pred b -> LabeledPred pred a
    forall a b. (a -> b) -> LabeledPred pred a -> LabeledPred pred b
    forall pred a b. a -> LabeledPred pred b -> LabeledPred pred a
    forall pred a b.
    (a -> b) -> LabeledPred pred a -> LabeledPred pred b
    forall (f :: Type -> Type).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall pred a b.
    (a -> b) -> LabeledPred pred a -> LabeledPred pred b
    fmap :: forall a b. (a -> b) -> LabeledPred pred a -> LabeledPred pred b
    $c<$ :: forall pred a b. a -> LabeledPred pred b -> LabeledPred pred a
    <$ :: forall a b. a -> LabeledPred pred b -> LabeledPred pred a
    Functor, (forall m. Monoid m => LabeledPred pred m -> m)
    -> (forall m a. Monoid m => (a -> m) -> LabeledPred pred a -> m)
    -> (forall m a. Monoid m => (a -> m) -> LabeledPred pred a -> m)
    -> (forall a b. (a -> b -> b) -> b -> LabeledPred pred a -> b)
    -> (forall a b. (a -> b -> b) -> b -> LabeledPred pred a -> b)
    -> (forall b a. (b -> a -> b) -> b -> LabeledPred pred a -> b)
    -> (forall b a. (b -> a -> b) -> b -> LabeledPred pred a -> b)
    -> (forall a. (a -> a -> a) -> LabeledPred pred a -> a)
    -> (forall a. (a -> a -> a) -> LabeledPred pred a -> a)
    -> (forall a. LabeledPred pred a -> [a])
    -> (forall a. LabeledPred pred a -> Bool)
    -> (forall a. LabeledPred pred a -> Int)
    -> (forall a. Eq a => a -> LabeledPred pred a -> Bool)
    -> (forall a. Ord a => LabeledPred pred a -> a)
    -> (forall a. Ord a => LabeledPred pred a -> a)
    -> (forall a. Num a => LabeledPred pred a -> a)
    -> (forall a. Num a => LabeledPred pred a -> a)
    -> Foldable (LabeledPred pred)
    forall a. Eq a => a -> LabeledPred pred a -> Bool
    forall a. Num a => LabeledPred pred a -> a
    forall a. Ord a => LabeledPred pred a -> a
    forall m. Monoid m => LabeledPred pred m -> m
    forall a. LabeledPred pred a -> Bool
    forall a. LabeledPred pred a -> Int
    forall a. LabeledPred pred a -> [a]
    forall a. (a -> a -> a) -> LabeledPred pred a -> a
    forall pred a. Eq a => a -> LabeledPred pred a -> Bool
    forall pred a. Num a => LabeledPred pred a -> a
    forall pred a. Ord a => LabeledPred pred a -> a
    forall pred m. Monoid m => LabeledPred pred m -> m
    forall m a. Monoid m => (a -> m) -> LabeledPred pred a -> m
    forall pred a. LabeledPred pred a -> Bool
    forall pred a. LabeledPred pred a -> Int
    forall pred a. LabeledPred pred a -> [a]
    forall b a. (b -> a -> b) -> b -> LabeledPred pred a -> b
    forall a b. (a -> b -> b) -> b -> LabeledPred pred a -> b
    forall pred a. (a -> a -> a) -> LabeledPred pred a -> a
    forall pred m a. Monoid m => (a -> m) -> LabeledPred pred a -> m
    forall pred b a. (b -> a -> b) -> b -> LabeledPred pred a -> b
    forall pred a b. (a -> b -> b) -> b -> LabeledPred pred a -> b
    forall (t :: Type -> Type).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall pred m. Monoid m => LabeledPred pred m -> m
    fold :: forall m. Monoid m => LabeledPred pred m -> m
    $cfoldMap :: forall pred m a. Monoid m => (a -> m) -> LabeledPred pred a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> LabeledPred pred a -> m
    $cfoldMap' :: forall pred m a. Monoid m => (a -> m) -> LabeledPred pred a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> LabeledPred pred a -> m
    $cfoldr :: forall pred a b. (a -> b -> b) -> b -> LabeledPred pred a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> LabeledPred pred a -> b
    $cfoldr' :: forall pred a b. (a -> b -> b) -> b -> LabeledPred pred a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> LabeledPred pred a -> b
    $cfoldl :: forall pred b a. (b -> a -> b) -> b -> LabeledPred pred a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> LabeledPred pred a -> b
    $cfoldl' :: forall pred b a. (b -> a -> b) -> b -> LabeledPred pred a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> LabeledPred pred a -> b
    $cfoldr1 :: forall pred a. (a -> a -> a) -> LabeledPred pred a -> a
    foldr1 :: forall a. (a -> a -> a) -> LabeledPred pred a -> a
    $cfoldl1 :: forall pred a. (a -> a -> a) -> LabeledPred pred a -> a
    foldl1 :: forall a. (a -> a -> a) -> LabeledPred pred a -> a
    $ctoList :: forall pred a. LabeledPred pred a -> [a]
    toList :: forall a. LabeledPred pred a -> [a]
    $cnull :: forall pred a. LabeledPred pred a -> Bool
    null :: forall a. LabeledPred pred a -> Bool
    $clength :: forall pred a. LabeledPred pred a -> Int
    length :: forall a. LabeledPred pred a -> Int
    $celem :: forall pred a. Eq a => a -> LabeledPred pred a -> Bool
    elem :: forall a. Eq a => a -> LabeledPred pred a -> Bool
    $cmaximum :: forall pred a. Ord a => LabeledPred pred a -> a
    maximum :: forall a. Ord a => LabeledPred pred a -> a
    $cminimum :: forall pred a. Ord a => LabeledPred pred a -> a
    minimum :: forall a. Ord a => LabeledPred pred a -> a
    $csum :: forall pred a. Num a => LabeledPred pred a -> a
    sum :: forall a. Num a => LabeledPred pred a -> a
    $cproduct :: forall pred a. Num a => LabeledPred pred a -> a
    product :: forall a. Num a => LabeledPred pred a -> a
    Foldable, (forall x. LabeledPred pred msg -> Rep (LabeledPred pred msg) x)
    -> (forall x. Rep (LabeledPred pred msg) x -> LabeledPred pred msg)
    -> Generic (LabeledPred pred msg)
    forall x. Rep (LabeledPred pred msg) x -> LabeledPred pred msg
    forall x. LabeledPred pred msg -> Rep (LabeledPred pred msg) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall pred msg x.
    Rep (LabeledPred pred msg) x -> LabeledPred pred msg
    forall pred msg x.
    LabeledPred pred msg -> Rep (LabeledPred pred msg) x
    $cfrom :: forall pred msg x.
    LabeledPred pred msg -> Rep (LabeledPred pred msg) x
    from :: forall x. LabeledPred pred msg -> Rep (LabeledPred pred msg) x
    $cto :: forall pred msg x.
    Rep (LabeledPred pred msg) x -> LabeledPred pred msg
    to :: forall x. Rep (LabeledPred pred msg) x -> LabeledPred pred msg
    Generic, (forall a. LabeledPred pred a -> Rep1 (LabeledPred pred) a)
    -> (forall a. Rep1 (LabeledPred pred) a -> LabeledPred pred a)
    -> Generic1 (LabeledPred pred)
    forall a. Rep1 (LabeledPred pred) a -> LabeledPred pred a
    forall a. LabeledPred pred a -> Rep1 (LabeledPred pred) a
    forall pred a. Rep1 (LabeledPred pred) a -> LabeledPred pred a
    forall pred a. LabeledPred pred a -> Rep1 (LabeledPred pred) a
    forall k (f :: k -> Type).
    (forall (a :: k). f a -> Rep1 f a)
    -> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
    $cfrom1 :: forall pred a. LabeledPred pred a -> Rep1 (LabeledPred pred) a
    from1 :: forall a. LabeledPred pred a -> Rep1 (LabeledPred pred) a
    $cto1 :: forall pred a. Rep1 (LabeledPred pred) a -> LabeledPred pred a
    to1 :: forall a. Rep1 (LabeledPred pred) a -> LabeledPred pred a
    Generic1, Eq (LabeledPred pred msg)
    Eq (LabeledPred pred msg) =>
    (LabeledPred pred msg -> LabeledPred pred msg -> Ordering)
    -> (LabeledPred pred msg -> LabeledPred pred msg -> Bool)
    -> (LabeledPred pred msg -> LabeledPred pred msg -> Bool)
    -> (LabeledPred pred msg -> LabeledPred pred msg -> Bool)
    -> (LabeledPred pred msg -> LabeledPred pred msg -> Bool)
    -> (LabeledPred pred msg
        -> LabeledPred pred msg -> LabeledPred pred msg)
    -> (LabeledPred pred msg
        -> LabeledPred pred msg -> LabeledPred pred msg)
    -> Ord (LabeledPred pred msg)
    LabeledPred pred msg -> LabeledPred pred msg -> Bool
    LabeledPred pred msg -> LabeledPred pred msg -> Ordering
    LabeledPred pred msg
    -> LabeledPred pred msg -> LabeledPred pred msg
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall pred msg. (Ord pred, Ord msg) => Eq (LabeledPred pred msg)
    forall pred msg.
    (Ord pred, Ord msg) =>
    LabeledPred pred msg -> LabeledPred pred msg -> Bool
    forall pred msg.
    (Ord pred, Ord msg) =>
    LabeledPred pred msg -> LabeledPred pred msg -> Ordering
    forall pred msg.
    (Ord pred, Ord msg) =>
    LabeledPred pred msg
    -> LabeledPred pred msg -> LabeledPred pred msg
    $ccompare :: forall pred msg.
    (Ord pred, Ord msg) =>
    LabeledPred pred msg -> LabeledPred pred msg -> Ordering
    compare :: LabeledPred pred msg -> LabeledPred pred msg -> Ordering
    $c< :: forall pred msg.
    (Ord pred, Ord msg) =>
    LabeledPred pred msg -> LabeledPred pred msg -> Bool
    < :: LabeledPred pred msg -> LabeledPred pred msg -> Bool
    $c<= :: forall pred msg.
    (Ord pred, Ord msg) =>
    LabeledPred pred msg -> LabeledPred pred msg -> Bool
    <= :: LabeledPred pred msg -> LabeledPred pred msg -> Bool
    $c> :: forall pred msg.
    (Ord pred, Ord msg) =>
    LabeledPred pred msg -> LabeledPred pred msg -> Bool
    > :: LabeledPred pred msg -> LabeledPred pred msg -> Bool
    $c>= :: forall pred msg.
    (Ord pred, Ord msg) =>
    LabeledPred pred msg -> LabeledPred pred msg -> Bool
    >= :: LabeledPred pred msg -> LabeledPred pred msg -> Bool
    $cmax :: forall pred msg.
    (Ord pred, Ord msg) =>
    LabeledPred pred msg
    -> LabeledPred pred msg -> LabeledPred pred msg
    max :: LabeledPred pred msg
    -> LabeledPred pred msg -> LabeledPred pred msg
    $cmin :: forall pred msg.
    (Ord pred, Ord msg) =>
    LabeledPred pred msg
    -> LabeledPred pred msg -> LabeledPred pred msg
    min :: LabeledPred pred msg
    -> LabeledPred pred msg -> LabeledPred pred msg
    Ord, Int -> LabeledPred pred msg -> ShowS
    [LabeledPred pred msg] -> ShowS
    LabeledPred pred msg -> String
    (Int -> LabeledPred pred msg -> ShowS)
    -> (LabeledPred pred msg -> String)
    -> ([LabeledPred pred msg] -> ShowS)
    -> Show (LabeledPred pred msg)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall pred msg.
    (Show pred, Show msg) =>
    Int -> LabeledPred pred msg -> ShowS
    forall pred msg.
    (Show pred, Show msg) =>
    [LabeledPred pred msg] -> ShowS
    forall pred msg.
    (Show pred, Show msg) =>
    LabeledPred pred msg -> String
    $cshowsPrec :: forall pred msg.
    (Show pred, Show msg) =>
    Int -> LabeledPred pred msg -> ShowS
    showsPrec :: Int -> LabeledPred pred msg -> ShowS
    $cshow :: forall pred msg.
    (Show pred, Show msg) =>
    LabeledPred pred msg -> String
    show :: LabeledPred pred msg -> String
    $cshowList :: forall pred msg.
    (Show pred, Show msg) =>
    [LabeledPred pred msg] -> ShowS
    showList :: [LabeledPred pred msg] -> ShowS
    Show, Functor (LabeledPred pred)
    Foldable (LabeledPred pred)
    (Functor (LabeledPred pred), Foldable (LabeledPred pred)) =>
    (forall (f :: Type -> Type) a b.
     Applicative f =>
     (a -> f b) -> LabeledPred pred a -> f (LabeledPred pred b))
    -> (forall (f :: Type -> Type) a.
        Applicative f =>
        LabeledPred pred (f a) -> f (LabeledPred pred a))
    -> (forall (m :: Type -> Type) a b.
        Monad m =>
        (a -> m b) -> LabeledPred pred a -> m (LabeledPred pred b))
    -> (forall (m :: Type -> Type) a.
        Monad m =>
        LabeledPred pred (m a) -> m (LabeledPred pred a))
    -> Traversable (LabeledPred pred)
    forall pred. Functor (LabeledPred pred)
    forall pred. Foldable (LabeledPred pred)
    forall pred (m :: Type -> Type) a.
    Monad m =>
    LabeledPred pred (m a) -> m (LabeledPred pred a)
    forall pred (f :: Type -> Type) a.
    Applicative f =>
    LabeledPred pred (f a) -> f (LabeledPred pred a)
    forall pred (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> LabeledPred pred a -> m (LabeledPred pred b)
    forall pred (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> LabeledPred pred a -> f (LabeledPred pred b)
    forall (t :: Type -> Type).
    (Functor t, Foldable t) =>
    (forall (f :: Type -> Type) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: Type -> Type) a.
        Applicative f =>
        t (f a) -> f (t a))
    -> (forall (m :: Type -> Type) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: Type -> Type) a.
    Monad m =>
    LabeledPred pred (m a) -> m (LabeledPred pred a)
    forall (f :: Type -> Type) a.
    Applicative f =>
    LabeledPred pred (f a) -> f (LabeledPred pred a)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> LabeledPred pred a -> m (LabeledPred pred b)
    forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> LabeledPred pred a -> f (LabeledPred pred b)
    $ctraverse :: forall pred (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> LabeledPred pred a -> f (LabeledPred pred b)
    traverse :: forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> LabeledPred pred a -> f (LabeledPred pred b)
    $csequenceA :: forall pred (f :: Type -> Type) a.
    Applicative f =>
    LabeledPred pred (f a) -> f (LabeledPred pred a)
    sequenceA :: forall (f :: Type -> Type) a.
    Applicative f =>
    LabeledPred pred (f a) -> f (LabeledPred pred a)
    $cmapM :: forall pred (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> LabeledPred pred a -> m (LabeledPred pred b)
    mapM :: forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> LabeledPred pred a -> m (LabeledPred pred b)
    $csequence :: forall pred (m :: Type -> Type) a.
    Monad m =>
    LabeledPred pred (m a) -> m (LabeledPred pred a)
    sequence :: forall (m :: Type -> Type) a.
    Monad m =>
    LabeledPred pred (m a) -> m (LabeledPred pred a)
    Traversable, Typeable)

    $(deriveBifunctor     ''LabeledPred)
    $(deriveBifoldable    ''LabeledPred)
    $(deriveBitraversable ''LabeledPred)
    $(deriveEq1           ''LabeledPred)
    $(deriveEq2           ''LabeledPred)
    $(deriveOrd1          ''LabeledPred)
    $(deriveOrd2          ''LabeledPred)
    $(deriveShow1         ''LabeledPred)
    $(deriveShow2         ''LabeledPred)

    -- | Predicate that was asserted.
    labeledPred :: Lens (LabeledPred pred msg) (LabeledPred pred' msg) pred pred'
    labeledPred :: forall pred msg pred' (f :: Type -> Type).
    Functor f =>
    (pred -> f pred')
    -> LabeledPred pred msg -> f (LabeledPred pred' msg)
    labeledPred = (LabeledPred pred msg -> pred)
    -> (LabeledPred pred msg -> pred' -> LabeledPred pred' msg)
    -> Lens (LabeledPred pred msg) (LabeledPred pred' msg) pred pred'
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    lens LabeledPred pred msg -> pred
    forall pred msg. LabeledPred pred msg -> pred
    _labeledPred (\LabeledPred pred msg
    s pred'
    v -> LabeledPred pred msg
    s { _labeledPred = v })

    -- | Message added when assumption/assertion was made.
    labeledPredMsg :: Lens (LabeledPred pred msg) (LabeledPred pred msg') msg msg'
    labeledPredMsg :: forall pred msg msg' (f :: Type -> Type).
    Functor f =>
    (msg -> f msg')
    -> LabeledPred pred msg -> f (LabeledPred pred msg')
    labeledPredMsg = (LabeledPred pred msg -> msg)
    -> (LabeledPred pred msg -> msg' -> LabeledPred pred msg')
    -> Lens (LabeledPred pred msg) (LabeledPred pred msg') msg msg'
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    lens LabeledPred pred msg -> msg
    forall pred msg. LabeledPred pred msg -> msg
    _labeledPredMsg (\LabeledPred pred msg
    s msg'
    v -> LabeledPred pred msg
    s { _labeledPredMsg = v })

    -- | Partition datastructures containing predicates by their possibly concrete
    --   values.
    --
    --   The output format is (constantly true, constantly false, unknown/symbolic).
    partitionByPredsM ::
      (Monad m, Foldable t, IsExprBuilder sym) =>
      proxy sym {- ^ avoid \"ambiguous type variable\" errors -}->
      (a -> m (Pred sym)) ->
      t a ->
      m ([a], [a], [a])
    partitionByPredsM :: forall (m :: Type -> Type) (t :: Type -> Type) sym
           (proxy :: Type -> Type) a.
    (Monad m, Foldable t, IsExprBuilder sym) =>
    proxy sym -> (a -> m (Pred sym)) -> t a -> m ([a], [a], [a])
    partitionByPredsM proxy sym
    _proxy a -> m (Pred sym)
    getPred t a
    xs =
      let step :: a -> ([a], [a], [a]) -> m ([a], [a], [a])
    step a
    x ([a]
    true, [a]
    false, [a]
    unknown) = a -> m (Pred sym)
    getPred a
    x m (Pred sym) -> (Pred sym -> ([a], [a], [a])) -> m ([a], [a], [a])
    forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
    <&> \Pred sym
    p ->
            case Pred sym -> Maybe Bool
    forall (e :: BaseType -> Type).
    IsExpr e =>
    e BaseBoolType -> Maybe Bool
    asConstantPred Pred sym
    p of
              Just Bool
    True  -> (a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    true, [a]
    false, [a]
    unknown)
              Just Bool
    False -> ([a]
    true, a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    false, [a]
    unknown)
              Maybe Bool
    Nothing    -> ([a]
    true, [a]
    false, a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    unknown)
      in (a -> ([a], [a], [a]) -> m ([a], [a], [a]))
    -> ([a], [a], [a]) -> t a -> m ([a], [a], [a])
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    (a -> b -> m b) -> b -> t a -> m b
    foldrM a -> ([a], [a], [a]) -> m ([a], [a], [a])
    step ([], [], []) t a
    xs

    -- | Partition datastructures containing predicates by their possibly concrete
    --   values.
    --
    --   The output format is (constantly true, constantly false, unknown/symbolic).
    partitionByPreds ::
      (Foldable t, IsExprBuilder sym) =>
      proxy sym {- ^ avoid \"ambiguous type variable\" errors -}->
      (a -> Pred sym) ->
      t a ->
      ([a], [a], [a])
    partitionByPreds :: forall (t :: Type -> Type) sym (proxy :: Type -> Type) a.
    (Foldable t, IsExprBuilder sym) =>
    proxy sym -> (a -> Pred sym) -> t a -> ([a], [a], [a])
    partitionByPreds proxy sym
    proxy a -> SymExpr sym BaseBoolType
    getPred t a
    xs =
      Identity ([a], [a], [a]) -> ([a], [a], [a])
    forall a. Identity a -> a
    runIdentity (proxy sym
    -> (a -> Identity (SymExpr sym BaseBoolType))
    -> t a
    -> Identity ([a], [a], [a])
    forall (m :: Type -> Type) (t :: Type -> Type) sym
           (proxy :: Type -> Type) a.
    (Monad m, Foldable t, IsExprBuilder sym) =>
    proxy sym -> (a -> m (Pred sym)) -> t a -> m ([a], [a], [a])
    partitionByPredsM proxy sym
    proxy ((a -> SymExpr sym BaseBoolType)
    -> a -> Identity (SymExpr sym BaseBoolType)
    forall a b. Coercible a b => a -> b
    coerce a -> SymExpr sym BaseBoolType
    getPred) t a
    xs)

    -- | Partition labeled predicates by their possibly concrete values.
    --
    --   The output format is (constantly true, constantly false, unknown/symbolic).
    partitionLabeledPreds ::
      (Foldable t, IsExprBuilder sym) =>
      proxy sym {- ^ avoid \"ambiguous type variable\" errors -}->
      t (LabeledPred (Pred sym) msg) ->
      ([LabeledPred (Pred sym) msg], [LabeledPred (Pred sym) msg], [LabeledPred (Pred sym) msg])
    partitionLabeledPreds :: forall (t :: Type -> Type) sym (proxy :: Type -> Type) msg.
    (Foldable t, IsExprBuilder sym) =>
    proxy sym
    -> t (LabeledPred (Pred sym) msg)
    -> ([LabeledPred (Pred sym) msg], [LabeledPred (Pred sym) msg],
        [LabeledPred (Pred sym) msg])
    partitionLabeledPreds proxy sym
    proxy = proxy sym
    -> (LabeledPred (SymExpr sym BaseBoolType) msg
        -> SymExpr sym BaseBoolType)
    -> t (LabeledPred (SymExpr sym BaseBoolType) msg)
    -> ([LabeledPred (SymExpr sym BaseBoolType) msg],
        [LabeledPred (SymExpr sym BaseBoolType) msg],
        [LabeledPred (SymExpr sym BaseBoolType) msg])
    forall (t :: Type -> Type) sym (proxy :: Type -> Type) a.
    (Foldable t, IsExprBuilder sym) =>
    proxy sym -> (a -> Pred sym) -> t a -> ([a], [a], [a])
    partitionByPreds proxy sym
    proxy (Getting
      (SymExpr sym BaseBoolType)
      (LabeledPred (SymExpr sym BaseBoolType) msg)
      (SymExpr sym BaseBoolType)
    -> LabeledPred (SymExpr sym BaseBoolType) msg
    -> SymExpr sym BaseBoolType
    forall s (m :: Type -> Type) a.
    MonadReader s m =>
    Getting a s a -> m a
    view Getting
      (SymExpr sym BaseBoolType)
      (LabeledPred (SymExpr sym BaseBoolType) msg)
      (SymExpr sym BaseBoolType)
    forall pred msg pred' (f :: Type -> Type).
    Functor f =>
    (pred -> f pred')
    -> LabeledPred pred msg -> f (LabeledPred pred' msg)
    labeledPred)