what4-1.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2019-2020
LicenseBSD3
MaintainerLangston Barrett <langston@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

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

Documentation

data LabeledPred pred msg Source #

Information about an assertion that was previously made.

Constructors

LabeledPred 

Fields

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