-----------------------------------------------------------------------
-- |
-- 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 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 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)