What4.Partial

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.

Partial

data Partial p v

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

• _partialPred :: !p
• _partialValue :: !v

Instances

Bifoldable Partial

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

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

Bitraversable Partial

Defined in What4.Partial

Methods

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

Eq2 Partial

Defined in What4.Partial

Methods

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

Ord2 Partial

Defined in What4.Partial

Methods

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

Show2 Partial

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

Generic1 (Partial p :: Type -> Type)

Defined in What4.Partial

Associated Types

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

Methods

from1 :: forall (a :: k). Partial p a -> Rep1 (Partial p) a

to1 :: forall (a :: k). Rep1 (Partial p) a -> Partial p a

Foldable (Partial p)

Defined in What4.Partial

Methods

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

foldMap :: Monoid m => (a -> m) -> Partial p a -> 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

Eq p => Eq1 (Partial p)

Defined in What4.Partial

Methods

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

Ord p => Ord1 (Partial p)

Defined in What4.Partial

Methods

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

Show p => Show1 (Partial p)

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

Traversable (Partial p)

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)

Functor (Partial p)

Defined in What4.Partial

Methods

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

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

(Data p, Data v) => Data (Partial p v)

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 :: forall r r'. (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)

Generic (Partial p v)

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

(Show p, Show v) => Show (Partial p v)

Defined in What4.Partial

Methods

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

show :: Partial p v -> String

showList :: [Partial p v] -> ShowS

(Eq p, Eq v) => Eq (Partial p v)

Defined in What4.Partial

Methods

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

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

(Ord p, Ord v) => Ord (Partial p v)

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

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

Defined in What4.Partial

type Rep1 (Partial p :: Type -> Type) = D1 ('MetaData "Partial" "What4.Partial" "what4-1.6.1-FJi93cuUq8WJprgqcgGmcU" '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)

Defined in What4.Partial

type Rep (Partial p v) = D1 ('MetaData "Partial" "What4.Partial" "what4-1.6.1-FJi93cuUq8WJprgqcgGmcU" '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

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

PartialWithErr

data PartialWithErr e p v

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

Constructors

NoErr (Partial p v)

Err e

Instances

Generic1 (PartialWithErr e p :: Type -> Type)

Defined in What4.Partial

Associated Types

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

Methods

from1 :: forall (a :: k). PartialWithErr e p a -> Rep1 (PartialWithErr e p) a

to1 :: forall (a :: k). Rep1 (PartialWithErr e p) a -> PartialWithErr e p a

Bifoldable (PartialWithErr e)

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)

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

Bitraversable (PartialWithErr e)

Defined in What4.Partial

Methods

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

Eq e => Eq2 (PartialWithErr e)

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)

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)

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

Foldable (PartialWithErr e p)

Defined in What4.Partial

Methods

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

foldMap :: Monoid m => (a -> m) -> PartialWithErr e p a -> 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

(Eq e, Eq p) => Eq1 (PartialWithErr e p)

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)

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)

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

Traversable (PartialWithErr e p)

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)

Functor (PartialWithErr e p)

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

(Data p, Data v, Data e) => Data (PartialWithErr e p v)

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 :: forall r r'. (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)

Generic (PartialWithErr e p v)

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

(Show p, Show v, Show e) => Show (PartialWithErr e p v)

Defined in What4.Partial

Methods

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

show :: PartialWithErr e p v -> String

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

(Eq p, Eq v, Eq e) => Eq (PartialWithErr e p v)

Defined in What4.Partial

Methods

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

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

(Ord p, Ord v, Ord e) => Ord (PartialWithErr e p v)

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

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

Defined in What4.Partial

type Rep1 (PartialWithErr e p :: Type -> Type) = D1 ('MetaData "PartialWithErr" "What4.Partial" "what4-1.6.1-FJi93cuUq8WJprgqcgGmcU" '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)

Defined in What4.Partial

type Rep (PartialWithErr e p v) = D1 ('MetaData "PartialWithErr" "What4.Partial" "what4-1.6.1-FJi93cuUq8WJprgqcgGmcU" '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

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

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

pattern Unassigned :: PartExpr p v

mkPE :: IsExpr p => p BaseBoolType -> a -> PartExpr (p BaseBoolType) a

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

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

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

Create a part expression from a maybe value.

joinMaybePE :: Maybe (PartExpr p v) -> PartExpr p v

joinMaybePE = fromMaybe Unassigned.

PartialT

newtype PartialT sym m a

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

Constructors

PartialT

Fields

• unPartial :: sym -> Pred sym -> m (PartExpr (Pred sym) a)

Instances

IsExpr (SymExpr sym) => MonadTrans (PartialT sym)

Defined in What4.Partial

Methods

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

(IsExpr (SymExpr sym), MonadFail m) => MonadFail (PartialT sym m)

Defined in What4.Partial

Methods

fail :: String -> PartialT sym m a

(IsExpr (SymExpr sym), MonadIO m) => MonadIO (PartialT sym m)

Defined in What4.Partial

Methods

liftIO :: IO a -> PartialT sym m a

(IsExpr (SymExpr sym), Monad m) => Applicative (PartialT sym m)

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

Functor m => Functor (PartialT sym m)

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), Monad m) => Monad (PartialT sym m)

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

runPartialT

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

End the partial computation and just return the unassigned value.

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

Lift a Maybe value to a partial expression.

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

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

Add an extra condition to the current partial computation.

mergePartial

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

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