what4-1.0: Solver-agnostic symbolic values support for issuing queries

Copyright(c) Galois Inc 2014-2020
LicenseBSD3
MaintainerLangston Barrett <langston@galois.com>
Safe HaskellNone
LanguageHaskell2010

What4.Partial

Contents

Description

Often, various operations on values are only partially defined (in the case of Crucible expressions, consider loading a value from a pointer - this is only defined in the case that the pointer is valid and non-null). The PartExpr type allows for packaging values together with predicates that express their partiality: the value is only valid if the predicate is true.

Synopsis

Partial

data Partial p v Source #

A partial value represents a value that may or may not be valid.

The _partialPred field represents a predicate (optionally with additional provenance information) embodying the value's partiality.

Constructors

Partial 

Fields

Instances
Bitraversable Partial Source # 
Instance details

Defined in What4.Partial

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Partial a b -> f (Partial c d) #

Bifoldable Partial Source # 
Instance details

Defined in What4.Partial

Methods

bifold :: Monoid m => Partial m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Partial a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Partial a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Partial a b -> c #

Bifunctor Partial Source # 
Instance details

Defined in What4.Partial

Methods

bimap :: (a -> b) -> (c -> d) -> Partial a c -> Partial b d #

first :: (a -> b) -> Partial a c -> Partial b c #

second :: (b -> c) -> Partial a b -> Partial a c #

Eq2 Partial Source # 
Instance details

Defined in What4.Partial

Methods

liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Partial a c -> Partial b d -> Bool #

Ord2 Partial Source # 
Instance details

Defined in What4.Partial

Methods

liftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> Partial a c -> Partial b d -> Ordering #

Show2 Partial Source # 
Instance details

Defined in What4.Partial

Methods

liftShowsPrec2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> Int -> Partial a b -> ShowS #

liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [Partial a b] -> ShowS #

Functor (Partial p) Source # 
Instance details

Defined in What4.Partial

Methods

fmap :: (a -> b) -> Partial p a -> Partial p b #

(<$) :: a -> Partial p b -> Partial p a #

Foldable (Partial p) Source # 
Instance details

Defined in What4.Partial

Methods

fold :: Monoid m => Partial p m -> m #

foldMap :: Monoid m => (a -> m) -> Partial p a -> m #

foldr :: (a -> b -> b) -> b -> Partial p a -> b #

foldr' :: (a -> b -> b) -> b -> Partial p a -> b #

foldl :: (b -> a -> b) -> b -> Partial p a -> b #

foldl' :: (b -> a -> b) -> b -> Partial p a -> b #

foldr1 :: (a -> a -> a) -> Partial p a -> a #

foldl1 :: (a -> a -> a) -> Partial p a -> a #

toList :: Partial p a -> [a] #

null :: Partial p a -> Bool #

length :: Partial p a -> Int #

elem :: Eq a => a -> Partial p a -> Bool #

maximum :: Ord a => Partial p a -> a #

minimum :: Ord a => Partial p a -> a #

sum :: Num a => Partial p a -> a #

product :: Num a => Partial p a -> a #

Traversable (Partial p) Source # 
Instance details

Defined in What4.Partial

Methods

traverse :: Applicative f => (a -> f b) -> Partial p a -> f (Partial p b) #

sequenceA :: Applicative f => Partial p (f a) -> f (Partial p a) #

mapM :: Monad m => (a -> m b) -> Partial p a -> m (Partial p b) #

sequence :: Monad m => Partial p (m a) -> m (Partial p a) #

Eq p => Eq1 (Partial p) Source # 
Instance details

Defined in What4.Partial

Methods

liftEq :: (a -> b -> Bool) -> Partial p a -> Partial p b -> Bool #

Ord p => Ord1 (Partial p) Source # 
Instance details

Defined in What4.Partial

Methods

liftCompare :: (a -> b -> Ordering) -> Partial p a -> Partial p b -> Ordering #

Show p => Show1 (Partial p) Source # 
Instance details

Defined in What4.Partial

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Partial p a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Partial p a] -> ShowS #

Generic1 (Partial p :: Type -> Type) Source # 
Instance details

Defined in What4.Partial

Associated Types

type Rep1 (Partial p) :: k -> Type #

Methods

from1 :: Partial p a -> Rep1 (Partial p) a #

to1 :: Rep1 (Partial p) a -> Partial p a #

(Eq p, Eq v) => Eq (Partial p v) Source # 
Instance details

Defined in What4.Partial

Methods

(==) :: Partial p v -> Partial p v -> Bool #

(/=) :: Partial p v -> Partial p v -> Bool #

(Data p, Data v) => Data (Partial p v) Source # 
Instance details

Defined in What4.Partial

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Partial p v -> c (Partial p v) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Partial p v) #

toConstr :: Partial p v -> Constr #

dataTypeOf :: Partial p v -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Partial p v)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Partial p v)) #

gmapT :: (forall b. Data b => b -> b) -> Partial p v -> Partial p v #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Partial p v -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Partial p v -> r #

gmapQ :: (forall d. Data d => d -> u) -> Partial p v -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Partial p v -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v) #

(Ord p, Ord v) => Ord (Partial p v) Source # 
Instance details

Defined in What4.Partial

Methods

compare :: Partial p v -> Partial p v -> Ordering #

(<) :: Partial p v -> Partial p v -> Bool #

(<=) :: Partial p v -> Partial p v -> Bool #

(>) :: Partial p v -> Partial p v -> Bool #

(>=) :: Partial p v -> Partial p v -> Bool #

max :: Partial p v -> Partial p v -> Partial p v #

min :: Partial p v -> Partial p v -> Partial p v #

(Show p, Show v) => Show (Partial p v) Source # 
Instance details

Defined in What4.Partial

Methods

showsPrec :: Int -> Partial p v -> ShowS #

show :: Partial p v -> String #

showList :: [Partial p v] -> ShowS #

Generic (Partial p v) Source # 
Instance details

Defined in What4.Partial

Associated Types

type Rep (Partial p v) :: Type -> Type #

Methods

from :: Partial p v -> Rep (Partial p v) x #

to :: Rep (Partial p v) x -> Partial p v #

type Rep1 (Partial p :: Type -> Type) Source # 
Instance details

Defined in What4.Partial

type Rep1 (Partial p :: Type -> Type) = D1 (MetaData "Partial" "What4.Partial" "what4-1.0-IcCGmY3T3YeXUBLCM24Pe" False) (C1 (MetaCons "Partial" PrefixI True) (S1 (MetaSel (Just "_partialPred") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 p) :*: S1 (MetaSel (Just "_partialValue") NoSourceUnpackedness SourceStrict DecidedStrict) Par1))
type Rep (Partial p v) Source # 
Instance details

Defined in What4.Partial

type Rep (Partial p v) = D1 (MetaData "Partial" "What4.Partial" "what4-1.0-IcCGmY3T3YeXUBLCM24Pe" False) (C1 (MetaCons "Partial" PrefixI True) (S1 (MetaSel (Just "_partialPred") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 p) :*: S1 (MetaSel (Just "_partialValue") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 v)))

partialPred :: forall p v p. Lens (Partial p v) (Partial p v) p p Source #

partialValue :: forall p v v. Lens (Partial p v) (Partial p v) v v Source #

PartialWithErr

data PartialWithErr e p v Source #

Either a partial value, or a straight-up error.

Constructors

NoErr (Partial p v) 
Err e 
Instances
Bitraversable (PartialWithErr e) Source # 
Instance details

Defined in What4.Partial

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> PartialWithErr e a b -> f (PartialWithErr e c d) #

Bifoldable (PartialWithErr e) Source # 
Instance details

Defined in What4.Partial

Methods

bifold :: Monoid m => PartialWithErr e m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> PartialWithErr e a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> PartialWithErr e a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> PartialWithErr e a b -> c #

Bifunctor (PartialWithErr e) Source # 
Instance details

Defined in What4.Partial

Methods

bimap :: (a -> b) -> (c -> d) -> PartialWithErr e a c -> PartialWithErr e b d #

first :: (a -> b) -> PartialWithErr e a c -> PartialWithErr e b c #

second :: (b -> c) -> PartialWithErr e a b -> PartialWithErr e a c #

Eq e => Eq2 (PartialWithErr e) Source # 
Instance details

Defined in What4.Partial

Methods

liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> PartialWithErr e a c -> PartialWithErr e b d -> Bool #

Ord e => Ord2 (PartialWithErr e) Source # 
Instance details

Defined in What4.Partial

Methods

liftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> PartialWithErr e a c -> PartialWithErr e b d -> Ordering #

Show e => Show2 (PartialWithErr e) Source # 
Instance details

Defined in What4.Partial

Methods

liftShowsPrec2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> Int -> PartialWithErr e a b -> ShowS #

liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [PartialWithErr e a b] -> ShowS #

Generic1 (PartialWithErr e p :: Type -> Type) Source # 
Instance details

Defined in What4.Partial

Associated Types

type Rep1 (PartialWithErr e p) :: k -> Type #

Methods

from1 :: PartialWithErr e p a -> Rep1 (PartialWithErr e p) a #

to1 :: Rep1 (PartialWithErr e p) a -> PartialWithErr e p a #

Functor (PartialWithErr e p) Source # 
Instance details

Defined in What4.Partial

Methods

fmap :: (a -> b) -> PartialWithErr e p a -> PartialWithErr e p b #

(<$) :: a -> PartialWithErr e p b -> PartialWithErr e p a #

Foldable (PartialWithErr e p) Source # 
Instance details

Defined in What4.Partial

Methods

fold :: Monoid m => PartialWithErr e p m -> m #

foldMap :: Monoid m => (a -> m) -> PartialWithErr e p a -> m #

foldr :: (a -> b -> b) -> b -> PartialWithErr e p a -> b #

foldr' :: (a -> b -> b) -> b -> PartialWithErr e p a -> b #

foldl :: (b -> a -> b) -> b -> PartialWithErr e p a -> b #

foldl' :: (b -> a -> b) -> b -> PartialWithErr e p a -> b #

foldr1 :: (a -> a -> a) -> PartialWithErr e p a -> a #

foldl1 :: (a -> a -> a) -> PartialWithErr e p a -> a #

toList :: PartialWithErr e p a -> [a] #

null :: PartialWithErr e p a -> Bool #

length :: PartialWithErr e p a -> Int #

elem :: Eq a => a -> PartialWithErr e p a -> Bool #

maximum :: Ord a => PartialWithErr e p a -> a #

minimum :: Ord a => PartialWithErr e p a -> a #

sum :: Num a => PartialWithErr e p a -> a #

product :: Num a => PartialWithErr e p a -> a #

Traversable (PartialWithErr e p) Source # 
Instance details

Defined in What4.Partial

Methods

traverse :: Applicative f => (a -> f b) -> PartialWithErr e p a -> f (PartialWithErr e p b) #

sequenceA :: Applicative f => PartialWithErr e p (f a) -> f (PartialWithErr e p a) #

mapM :: Monad m => (a -> m b) -> PartialWithErr e p a -> m (PartialWithErr e p b) #

sequence :: Monad m => PartialWithErr e p (m a) -> m (PartialWithErr e p a) #

(Eq e, Eq p) => Eq1 (PartialWithErr e p) Source # 
Instance details

Defined in What4.Partial

Methods

liftEq :: (a -> b -> Bool) -> PartialWithErr e p a -> PartialWithErr e p b -> Bool #

(Ord e, Ord p) => Ord1 (PartialWithErr e p) Source # 
Instance details

Defined in What4.Partial

Methods

liftCompare :: (a -> b -> Ordering) -> PartialWithErr e p a -> PartialWithErr e p b -> Ordering #

(Show e, Show p) => Show1 (PartialWithErr e p) Source # 
Instance details

Defined in What4.Partial

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> PartialWithErr e p a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [PartialWithErr e p a] -> ShowS #

(Eq p, Eq v, Eq e) => Eq (PartialWithErr e p v) Source # 
Instance details

Defined in What4.Partial

Methods

(==) :: PartialWithErr e p v -> PartialWithErr e p v -> Bool #

(/=) :: PartialWithErr e p v -> PartialWithErr e p v -> Bool #

(Data e, Data p, Data v) => Data (PartialWithErr e p v) Source # 
Instance details

Defined in What4.Partial

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PartialWithErr e p v -> c (PartialWithErr e p v) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PartialWithErr e p v) #

toConstr :: PartialWithErr e p v -> Constr #

dataTypeOf :: PartialWithErr e p v -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (PartialWithErr e p v)) #

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (PartialWithErr e p v)) #

gmapT :: (forall b. Data b => b -> b) -> PartialWithErr e p v -> PartialWithErr e p v #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r #

gmapQ :: (forall d. Data d => d -> u) -> PartialWithErr e p v -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PartialWithErr e p v -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PartialWithErr e p v -> m (PartialWithErr e p v) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PartialWithErr e p v -> m (PartialWithErr e p v) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PartialWithErr e p v -> m (PartialWithErr e p v) #

(Ord p, Ord v, Ord e) => Ord (PartialWithErr e p v) Source # 
Instance details

Defined in What4.Partial

Methods

compare :: PartialWithErr e p v -> PartialWithErr e p v -> Ordering #

(<) :: PartialWithErr e p v -> PartialWithErr e p v -> Bool #

(<=) :: PartialWithErr e p v -> PartialWithErr e p v -> Bool #

(>) :: PartialWithErr e p v -> PartialWithErr e p v -> Bool #

(>=) :: PartialWithErr e p v -> PartialWithErr e p v -> Bool #

max :: PartialWithErr e p v -> PartialWithErr e p v -> PartialWithErr e p v #

min :: PartialWithErr e p v -> PartialWithErr e p v -> PartialWithErr e p v #

(Show p, Show v, Show e) => Show (PartialWithErr e p v) Source # 
Instance details

Defined in What4.Partial

Methods

showsPrec :: Int -> PartialWithErr e p v -> ShowS #

show :: PartialWithErr e p v -> String #

showList :: [PartialWithErr e p v] -> ShowS #

Generic (PartialWithErr e p v) Source # 
Instance details

Defined in What4.Partial

Associated Types

type Rep (PartialWithErr e p v) :: Type -> Type #

Methods

from :: PartialWithErr e p v -> Rep (PartialWithErr e p v) x #

to :: Rep (PartialWithErr e p v) x -> PartialWithErr e p v #

type Rep1 (PartialWithErr e p :: Type -> Type) Source # 
Instance details

Defined in What4.Partial

type Rep1 (PartialWithErr e p :: Type -> Type) = D1 (MetaData "PartialWithErr" "What4.Partial" "what4-1.0-IcCGmY3T3YeXUBLCM24Pe" False) (C1 (MetaCons "NoErr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec1 (Partial p))) :+: C1 (MetaCons "Err" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 e)))
type Rep (PartialWithErr e p v) Source # 
Instance details

Defined in What4.Partial

type Rep (PartialWithErr e p v) = D1 (MetaData "PartialWithErr" "What4.Partial" "what4-1.0-IcCGmY3T3YeXUBLCM24Pe" False) (C1 (MetaCons "NoErr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Partial p v))) :+: C1 (MetaCons "Err" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 e)))

PartExpr

type PartExpr p v = PartialWithErr () p v Source #

A PartExpr is a PartialWithErr that provides no information about what went wrong. Its name is historic.

pattern PE :: p -> v -> PartExpr p v Source #

pattern Unassigned :: PartExpr p v Source #

justPartExpr :: IsExprBuilder sym => sym -> v -> PartExpr (Pred sym) v Source #

Create a part expression from a value that is always defined.

maybePartExpr :: IsExprBuilder sym => sym -> Maybe a -> PartExpr (Pred sym) a Source #

Create a part expression from a maybe value.

PartialT

newtype PartialT sym m a Source #

A monad transformer which enables symbolic partial computations to run by maintaining a predicate on the value.

Constructors

PartialT 

Fields

Instances
MonadTrans (PartialT sym) Source # 
Instance details

Defined in What4.Partial

Methods

lift :: Monad m => m a -> PartialT sym m a #

(IsExpr (SymExpr sym), Monad m) => Monad (PartialT sym m) Source # 
Instance details

Defined in What4.Partial

Methods

(>>=) :: PartialT sym m a -> (a -> PartialT sym m b) -> PartialT sym m b #

(>>) :: PartialT sym m a -> PartialT sym m b -> PartialT sym m b #

return :: a -> PartialT sym m a #

fail :: String -> PartialT sym m a #

Functor m => Functor (PartialT sym m) Source # 
Instance details

Defined in What4.Partial

Methods

fmap :: (a -> b) -> PartialT sym m a -> PartialT sym m b #

(<$) :: a -> PartialT sym m b -> PartialT sym m a #

(IsExpr (SymExpr sym), MonadFail m) => MonadFail (PartialT sym m) Source # 
Instance details

Defined in What4.Partial

Methods

fail :: String -> PartialT sym m a #

(IsExpr (SymExpr sym), Monad m) => Applicative (PartialT sym m) Source # 
Instance details

Defined in What4.Partial

Methods

pure :: a -> PartialT sym m a #

(<*>) :: PartialT sym m (a -> b) -> PartialT sym m a -> PartialT sym m b #

liftA2 :: (a -> b -> c) -> PartialT sym m a -> PartialT sym m b -> PartialT sym m c #

(*>) :: PartialT sym m a -> PartialT sym m b -> PartialT sym m b #

(<*) :: PartialT sym m a -> PartialT sym m b -> PartialT sym m a #

(IsExpr (SymExpr sym), MonadIO m) => MonadIO (PartialT sym m) Source # 
Instance details

Defined in What4.Partial

Methods

liftIO :: IO a -> PartialT sym m a #

runPartialT Source #

Arguments

:: sym

Solver interface

-> Pred sym

Initial condition

-> PartialT sym m a

Computation to run.

-> m (PartExpr (Pred sym) a) 

Run a partial computation.

returnUnassigned :: Applicative m => PartialT sym m a Source #

End the partial computation and just return the unassigned value.

returnMaybe :: (IsExpr (SymExpr sym), Applicative m) => Maybe a -> PartialT sym m a Source #

Lift a Maybe value to a partial expression.

returnPartial :: (IsExprBuilder sym, MonadIO m) => PartExpr (Pred sym) a -> PartialT sym m a Source #

Return a partial expression.

This joins the partial expression with the current constraints on the current computation.

addCondition :: (IsExprBuilder sym, MonadIO m) => Pred sym -> PartialT sym m () Source #

Add an extra condition to the current partial computation.

mergePartial Source #

Arguments

:: (IsExprBuilder sym, MonadIO m) 
=> sym 
-> (Pred sym -> a -> a -> PartialT sym m a)

Operation to combine inner values. The Pred parameter is the if-then-else condition.

-> Pred sym

condition to merge on

-> PartExpr (Pred sym) a

'if' value

-> PartExpr (Pred sym) a

'then' value

-> m (PartExpr (Pred sym) a) 

If-then-else on partial expressions.

mergePartials Source #

Arguments

:: (IsExprBuilder sym, MonadIO m) 
=> sym 
-> (Pred sym -> a -> a -> PartialT sym m a)

Operation to combine inner values. The Pred parameter is the if-then-else condition.

-> [(Pred sym, PartExpr (Pred sym) a)]

values to merge

-> m (PartExpr (Pred sym) a) 

Merge a collection of partial values in an if-then-else tree. For example, if we merge a list like [(xp,x),(yp,y),(zp,z)], we get a value that is morally equivalent to: if xp then x else (if yp then y else (if zp then z else undefined)).