-----------------------------------------------------------------------
-- |
-- 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 DeriveFunctor #-}
{-# 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.
       LabeledPred pred msg -> pred
_labeledPred    :: !pred
       -- | Message added when assumption/assertion was made.
     , 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
/= :: 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, Typeable (LabeledPred pred msg)
DataType
Constr
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 -> DataType
LabeledPred pred msg -> Constr
(forall b. Data b => b -> b)
-> LabeledPred pred msg -> LabeledPred pred 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 b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (LabeledPred pred msg)
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (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 -> 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 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))
$cLabeledPred :: Constr
$tLabeledPred :: DataType
gmapMo :: (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 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 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 :: 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 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 :: (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 :: (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 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 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 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 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)
$cp1Data :: forall pred msg.
(Data pred, Data msg) =>
Typeable (LabeledPred pred msg)
Data, a -> LabeledPred pred b -> LabeledPred pred a
(a -> b) -> LabeledPred pred a -> LabeledPred pred b
(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
<$ :: a -> LabeledPred pred b -> LabeledPred pred a
$c<$ :: forall pred a b. a -> LabeledPred pred b -> LabeledPred pred a
fmap :: (a -> b) -> LabeledPred pred a -> LabeledPred pred b
$cfmap :: forall pred a b.
(a -> b) -> LabeledPred pred a -> LabeledPred pred b
Functor, (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
$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 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
$cto1 :: forall pred a. Rep1 (LabeledPred pred) a -> LabeledPred pred a
$cfrom1 :: forall pred a. LabeledPred pred a -> Rep1 (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
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
$cp1Ord :: forall pred msg. (Ord pred, Ord msg) => Eq (LabeledPred pred msg)
Ord, 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 :: (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 :: pred'
_labeledPred = pred'
v })

-- | Message added when assumption/assertion was made.
labeledPredMsg :: Lens (LabeledPred pred msg) (LabeledPred pred msg') msg msg'
labeledPredMsg :: (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 :: 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 :: 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 :: proxy sym -> (a -> Pred sym) -> t a -> ([a], [a], [a])
partitionByPreds proxy sym
proxy a -> Pred sym
getPred t a
xs =
  Identity ([a], [a], [a]) -> ([a], [a], [a])
forall a. Identity a -> a
runIdentity (proxy sym
-> (a -> Identity (Pred sym)) -> 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 -> Pred sym) -> a -> Identity (Pred sym)
coerce a -> Pred sym
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 :: 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 (Pred sym) msg -> Pred sym)
-> t (LabeledPred (Pred sym) msg)
-> ([LabeledPred (Pred sym) msg], [LabeledPred (Pred sym) msg],
    [LabeledPred (Pred sym) 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 (Pred sym) (LabeledPred (Pred sym) msg) (Pred sym)
-> LabeledPred (Pred sym) msg -> Pred sym
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting (Pred sym) (LabeledPred (Pred sym) msg) (Pred sym)
forall pred msg pred'.
Lens (LabeledPred pred msg) (LabeledPred pred' msg) pred pred'
labeledPred)