-----------------------------------------------------------------------
-- |
-- 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
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
$c== :: forall pred msg.
(Eq pred, Eq msg) =>
LabeledPred pred msg -> LabeledPred pred msg -> Bool
Eq, LabeledPred pred msg -> DataType
LabeledPred pred msg -> Constr
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 {pred} {msg}.
(Data pred, Data msg) =>
Typeable (LabeledPred pred msg)
forall pred msg.
(Data pred, Data msg) =>
LabeledPred pred msg -> DataType
forall pred msg.
(Data pred, Data msg) =>
LabeledPred pred msg -> Constr
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 (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 -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (LabeledPred pred msg))
gmapMo :: 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)
gmapMp :: forall (m :: Type -> Type).
MonadPlus 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)
gmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d)
-> LabeledPred pred msg -> m (LabeledPred pred msg)
$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)
gmapQi :: forall u.
Int -> (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
gmapQ :: forall u.
(forall d. Data d => d -> u) -> LabeledPred pred msg -> [u]
$cgmapQ :: forall pred msg u.
(Data pred, Data msg) =>
(forall d. Data d => d -> u) -> LabeledPred pred msg -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r
$cgmapQl :: forall pred msg r r'.
(Data pred, Data msg) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r
gmapT :: (forall b. Data b => b -> b)
-> LabeledPred pred msg -> LabeledPred pred msg
$cgmapT :: forall pred msg.
(Data pred, Data msg) =>
(forall b. Data b => b -> b)
-> LabeledPred pred msg -> 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))
$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))
dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (LabeledPred pred msg))
$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))
dataTypeOf :: LabeledPred pred msg -> DataType
$cdataTypeOf :: forall pred msg.
(Data pred, Data msg) =>
LabeledPred pred msg -> DataType
toConstr :: LabeledPred pred msg -> Constr
$ctoConstr :: forall pred msg.
(Data pred, Data msg) =>
LabeledPred pred msg -> Constr
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)
$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)
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)
$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)
Data, 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
<$ :: forall a b. a -> LabeledPred pred b -> LabeledPred pred a
$c<$ :: forall pred a b. a -> LabeledPred pred b -> LabeledPred pred a
fmap :: forall a b. (a -> b) -> LabeledPred pred a -> LabeledPred pred b
$cfmap :: forall pred a b.
(a -> b) -> LabeledPred pred a -> LabeledPred pred b
Functor, forall a. LabeledPred pred a -> Bool
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 m a. Monoid m => (a -> m) -> LabeledPred pred a -> m
forall pred m. Monoid m => LabeledPred pred m -> m
forall pred a. LabeledPred pred a -> Bool
forall pred a. LabeledPred pred a -> Int
forall pred a. LabeledPred pred a -> [a]
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
product :: forall a. Num a => LabeledPred pred a -> a
$cproduct :: forall pred a. Num a => LabeledPred pred a -> a
sum :: forall a. Num a => LabeledPred pred a -> a
$csum :: forall pred a. Num a => LabeledPred pred a -> a
minimum :: forall a. Ord a => LabeledPred pred a -> a
$cminimum :: forall pred a. Ord a => LabeledPred pred a -> a
maximum :: forall a. Ord a => LabeledPred pred a -> a
$cmaximum :: forall pred a. Ord a => LabeledPred pred a -> a
elem :: forall a. Eq a => a -> LabeledPred pred a -> Bool
$celem :: forall pred a. Eq a => a -> LabeledPred pred a -> Bool
length :: forall a. LabeledPred pred a -> Int
$clength :: forall pred a. LabeledPred pred a -> Int
null :: forall a. LabeledPred pred a -> Bool
$cnull :: forall pred a. LabeledPred pred a -> Bool
toList :: forall a. LabeledPred pred a -> [a]
$ctoList :: forall pred a. LabeledPred pred a -> [a]
foldl1 :: forall a. (a -> a -> a) -> LabeledPred pred a -> a
$cfoldl1 :: forall pred a. (a -> a -> a) -> LabeledPred pred a -> a
foldr1 :: forall a. (a -> a -> a) -> LabeledPred pred a -> a
$cfoldr1 :: forall pred a. (a -> a -> a) -> LabeledPred pred a -> a
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
$cfoldl :: forall pred b a. (b -> a -> 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
$cfoldr :: forall pred a b. (a -> b -> b) -> b -> LabeledPred pred a -> b
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
$cfoldMap :: forall pred m a. Monoid m => (a -> m) -> LabeledPred pred a -> m
fold :: forall m. Monoid m => LabeledPred pred m -> m
$cfold :: forall pred m. Monoid m => LabeledPred pred m -> m
Foldable, 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
$cto :: forall pred msg x.
Rep (LabeledPred pred msg) x -> LabeledPred pred msg
$cfrom :: forall pred msg x.
LabeledPred pred msg -> Rep (LabeledPred pred msg) x
Generic, 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
$cto1 :: forall pred a. Rep1 (LabeledPred pred) a -> LabeledPred pred a
$cfrom1 :: forall pred a. LabeledPred pred a -> Rep1 (LabeledPred pred) a
Generic1, LabeledPred pred msg -> LabeledPred pred msg -> Bool
LabeledPred pred msg -> LabeledPred pred msg -> Ordering
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
min :: 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
max :: LabeledPred pred msg
-> LabeledPred pred msg -> LabeledPred pred msg
$cmax :: forall pred msg.
(Ord pred, Ord msg) =>
LabeledPred pred msg
-> LabeledPred pred msg -> LabeledPred pred msg
>= :: 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
$c< :: forall pred msg.
(Ord pred, Ord msg) =>
LabeledPred pred msg -> LabeledPred pred msg -> Bool
compare :: LabeledPred pred msg -> LabeledPred pred msg -> Ordering
$ccompare :: forall pred msg.
(Ord pred, Ord msg) =>
LabeledPred pred msg -> LabeledPred pred msg -> Ordering
Ord, Int -> LabeledPred pred msg -> ShowS
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
showList :: [LabeledPred pred msg] -> ShowS
$cshowList :: forall pred msg.
(Show pred, Show msg) =>
[LabeledPred pred msg] -> ShowS
show :: LabeledPred pred msg -> String
$cshow :: forall pred msg.
(Show pred, Show msg) =>
LabeledPred pred msg -> String
showsPrec :: Int -> LabeledPred pred msg -> ShowS
$cshowsPrec :: forall pred msg.
(Show pred, Show msg) =>
Int -> LabeledPred pred msg -> ShowS
Show, 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 (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> LabeledPred pred a -> f (LabeledPred pred b)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
LabeledPred pred (m a) -> m (LabeledPred pred a)
$csequence :: forall pred (m :: Type -> Type) a.
Monad m =>
LabeledPred pred (m a) -> m (LabeledPred pred a)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> LabeledPred pred a -> m (LabeledPred pred b)
$cmapM :: forall pred (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> LabeledPred pred a -> m (LabeledPred pred b)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
LabeledPred pred (f a) -> f (LabeledPred pred a)
$csequenceA :: forall pred (f :: Type -> Type) a.
Applicative f =>
LabeledPred pred (f a) -> f (LabeledPred pred a)
traverse :: 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)
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'.
Lens (LabeledPred pred msg) (LabeledPred pred' msg) pred pred'
labeledPred = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall pred msg. LabeledPred pred msg -> pred
_labeledPred (\LabeledPred pred msg
s pred'
v -> LabeledPred pred msg
s { _labeledPred :: pred'
_labeledPred = pred'
v })

-- | Message added when assumption/assertion was made.
labeledPredMsg :: Lens (LabeledPred pred msg) (LabeledPred pred msg') msg msg'
labeledPredMsg :: forall pred msg msg'.
Lens (LabeledPred pred msg) (LabeledPred pred msg') msg msg'
labeledPredMsg = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall pred msg. LabeledPred pred msg -> msg
_labeledPredMsg (\LabeledPred pred msg
s msg'
v -> LabeledPred pred msg
s { _labeledPredMsg :: msg'
_labeledPredMsg = msg'
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 forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \Pred sym
p ->
        case forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
p of
          Just Bool
True  -> (a
xforall a. a -> [a] -> [a]
:[a]
true, [a]
false, [a]
unknown)
          Just Bool
False -> ([a]
true, a
xforall a. a -> [a] -> [a]
:[a]
false, [a]
unknown)
          Maybe Bool
Nothing    -> ([a]
true, [a]
false, a
xforall a. a -> [a] -> [a]
:[a]
unknown)
  in 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 =
  forall a. Identity a -> a
runIdentity (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 (coerce :: 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 = 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 (forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view forall pred msg pred'.
Lens (LabeledPred pred msg) (LabeledPred pred' msg) pred pred'
labeledPred)