Copyright	(c) Galois Inc 2019-2020
License	BSD3
Maintainer	Langston Barrett <langston@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

What4.LabeledPred

Description

Predicates alone do not record their semantic content, thus it is often useful to attach some sort of descriptor to them.

Synopsis

data LabeledPred pred msg = LabeledPred {
- _labeledPred :: !pred
- _labeledPredMsg :: !msg
}
labeledPred :: Lens (LabeledPred pred msg) (LabeledPred pred' msg) pred pred'
labeledPredMsg :: Lens (LabeledPred pred msg) (LabeledPred pred msg') msg msg'
partitionByPreds :: (Foldable t, IsExprBuilder sym) => proxy sym -> (a -> Pred sym) -> t a -> ([a], [a], [a])
partitionByPredsM :: (Monad m, Foldable t, IsExprBuilder sym) => proxy sym -> (a -> m (Pred sym)) -> t a -> m ([a], [a], [a])
partitionLabeledPreds :: (Foldable t, IsExprBuilder sym) => proxy sym -> t (LabeledPred (Pred sym) msg) -> ([LabeledPred (Pred sym) msg], [LabeledPred (Pred sym) msg], [LabeledPred (Pred sym) msg])

Documentation

data LabeledPred pred msg Source #

Information about an assertion that was previously made.

Constructors

LabeledPred
Fields _labeledPred :: !pred Predicate that was asserted. _labeledPredMsg :: !msg Message added when assumption/assertion was made.

Instances

Instances details

Bitraversable LabeledPred Source #
Instance details Defined in What4.LabeledPred Methods bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> LabeledPred a b -> f (LabeledPred c d) #
Bifoldable LabeledPred Source #
Instance details Defined in What4.LabeledPred Methods bifold :: Monoid m => LabeledPred m m -> m # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> LabeledPred a b -> m # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> LabeledPred a b -> c # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> LabeledPred a b -> c #
Bifunctor LabeledPred Source #
Instance details Defined in What4.LabeledPred Methods bimap :: (a -> b) -> (c -> d) -> LabeledPred a c -> LabeledPred b d # first :: (a -> b) -> LabeledPred a c -> LabeledPred b c # second :: (b -> c) -> LabeledPred a b -> LabeledPred a c #
Eq2 LabeledPred Source #
Instance details Defined in What4.LabeledPred Methods liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> LabeledPred a c -> LabeledPred b d -> Bool #
Ord2 LabeledPred Source #
Instance details Defined in What4.LabeledPred Methods liftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> LabeledPred a c -> LabeledPred b d -> Ordering #
Show2 LabeledPred Source #
Instance details Defined in What4.LabeledPred Methods liftShowsPrec2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> Int -> LabeledPred a b -> ShowS # liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [LabeledPred a b] -> ShowS #
Functor (LabeledPred pred) Source #
Instance details Defined in What4.LabeledPred Methods fmap :: (a -> b) -> LabeledPred pred a -> LabeledPred pred b # (<$) :: a -> LabeledPred pred b -> LabeledPred pred a #
Eq pred => Eq1 (LabeledPred pred) Source #
Instance details Defined in What4.LabeledPred Methods liftEq :: (a -> b -> Bool) -> LabeledPred pred a -> LabeledPred pred b -> Bool #
Ord pred => Ord1 (LabeledPred pred) Source #
Instance details Defined in What4.LabeledPred Methods liftCompare :: (a -> b -> Ordering) -> LabeledPred pred a -> LabeledPred pred b -> Ordering #
Show pred => Show1 (LabeledPred pred) Source #
Instance details Defined in What4.LabeledPred Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> LabeledPred pred a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [LabeledPred pred a] -> ShowS #
Generic1 (LabeledPred pred :: Type -> Type) Source #
Instance details Defined in What4.LabeledPred Associated Types type Rep1 (LabeledPred pred) :: k -> Type # Methods from1 :: forall (a :: k). LabeledPred pred a -> Rep1 (LabeledPred pred) a # to1 :: forall (a :: k). Rep1 (LabeledPred pred) a -> LabeledPred pred a #
(Eq pred, Eq msg) => Eq (LabeledPred pred msg) Source #
Instance details Defined in What4.LabeledPred Methods (==) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool # (/=) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool #
(Data pred, Data msg) => Data (LabeledPred pred msg) Source #
Instance details Defined in What4.LabeledPred Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LabeledPred pred msg -> c (LabeledPred pred msg) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LabeledPred pred msg) # toConstr :: LabeledPred pred msg -> Constr # dataTypeOf :: LabeledPred pred msg -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LabeledPred pred msg)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LabeledPred pred msg)) # gmapT :: (forall b. Data b => b -> b) -> LabeledPred pred msg -> LabeledPred pred msg # gmapQl :: (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 # gmapQ :: (forall d. Data d => d -> u) -> LabeledPred pred msg -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LabeledPred pred msg -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LabeledPred pred msg -> m (LabeledPred pred msg) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LabeledPred pred msg -> m (LabeledPred pred msg) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LabeledPred pred msg -> m (LabeledPred pred msg) #
(Ord pred, Ord msg) => Ord (LabeledPred pred msg) Source #
Instance details Defined in What4.LabeledPred Methods compare :: 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 # max :: LabeledPred pred msg -> LabeledPred pred msg -> LabeledPred pred msg # min :: LabeledPred pred msg -> LabeledPred pred msg -> LabeledPred pred msg #
Generic (LabeledPred pred msg) Source #
Instance details Defined in What4.LabeledPred Associated Types type Rep (LabeledPred pred msg) :: Type -> Type # Methods from :: LabeledPred pred msg -> Rep (LabeledPred pred msg) x # to :: Rep (LabeledPred pred msg) x -> LabeledPred pred msg #
type Rep1 (LabeledPred pred :: Type -> Type) Source #
Instance details Defined in What4.LabeledPred type Rep1 (LabeledPred pred :: Type -> Type) = D1 ('MetaData "LabeledPred" "What4.LabeledPred" "what4-1.1-F6JmVDCUG2e4tsAmUzrLc2" 'False) (C1 ('MetaCons "LabeledPred" 'PrefixI 'True) (S1 ('MetaSel ('Just "_labeledPred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 pred) :*: S1 ('MetaSel ('Just "_labeledPredMsg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) Par1))
type Rep (LabeledPred pred msg) Source #
Instance details Defined in What4.LabeledPred type Rep (LabeledPred pred msg) = D1 ('MetaData "LabeledPred" "What4.LabeledPred" "what4-1.1-F6JmVDCUG2e4tsAmUzrLc2" 'False) (C1 ('MetaCons "LabeledPred" 'PrefixI 'True) (S1 ('MetaSel ('Just "_labeledPred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 pred) :*: S1 ('MetaSel ('Just "_labeledPredMsg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 msg)))

labeledPred :: Lens (LabeledPred pred msg) (LabeledPred pred' msg) pred pred' Source #

Predicate that was asserted.

labeledPredMsg :: Lens (LabeledPred pred msg) (LabeledPred pred msg') msg msg' Source #

Message added when assumption/assertion was made.

partitionByPreds Source #

Arguments

:: (Foldable t, IsExprBuilder sym)
=> proxy sym	avoid "ambiguous type variable" errors
-> (a -> Pred sym)
-> t a
-> ([a], [a], [a])

Partition datastructures containing predicates by their possibly concrete values.

The output format is (constantly true, constantly false, unknown/symbolic).

partitionByPredsM Source #

Arguments

:: (Monad m, Foldable t, IsExprBuilder sym)
=> proxy sym	avoid "ambiguous type variable" errors
-> (a -> m (Pred sym))
-> t a
-> m ([a], [a], [a])

Partition datastructures containing predicates by their possibly concrete values.

The output format is (constantly true, constantly false, unknown/symbolic).

partitionLabeledPreds Source #

Arguments

:: (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])

Partition labeled predicates by their possibly concrete values.

The output format is (constantly true, constantly false, unknown/symbolic).