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

Copyright | (c) Galois Inc 2014-2020
License | BSD3
Maintainer | Langston Barrett <langston@galois.com>
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Partial

Contents

- Partial
- PartialWithErr
- PartExpr
- PartialT

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

- data Partial p v = Partial {
  - _partialPred :: !p
  - _partialValue :: !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
- data PartialWithErr e p v
  - = NoErr (Partial p v)
  - | Err e
- type PartExpr p v = PartialWithErr () p v
- 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
- maybePartExpr :: IsExprBuilder sym => sym -> Maybe a -> PartExpr (Pred sym) a
- joinMaybePE :: Maybe (PartExpr p v) -> PartExpr p v
- newtype PartialT sym m a = PartialT {
  - unPartial :: sym -> Pred sym -> m (PartExpr (Pred sym) a)
  }
- runPartialT :: sym -> Pred sym -> PartialT sym m a -> m (PartExpr (Pred sym) a)
- returnUnassigned :: Applicative m => PartialT sym m a
- returnMaybe :: (IsExpr (SymExpr sym), Applicative m) => Maybe a -> PartialT sym m a
- returnPartial :: (IsExprBuilder sym, MonadIO m) => PartExpr (Pred sym) a -> PartialT sym m a
- addCondition :: (IsExprBuilder sym, MonadIO m) => Pred sym -> PartialT sym m ()
- mergePartial :: (IsExprBuilder sym, MonadIO m) => sym -> (Pred sym -> a -> a -> PartialT sym m a) -> Pred sym -> PartExpr (Pred sym) a -> PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a)
- mergePartials :: (IsExprBuilder sym, MonadIO m) => sym -> (Pred sym -> a -> a -> PartialT sym m a) -> [(Pred sym, PartExpr (Pred sym) a)] -> m (PartExpr (Pred sym) a)

## 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

- _partialPred :: !p
- _partialValue :: !v

#### Instances

Instances details

Bifoldable Partial Source # |
Instance details Defined in What4.Partial Methods bifold :: Monoid m => Partial m m -> m Source # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Partial a b -> m Source # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Partial a b -> c Source # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Partial a b -> c Source #
Bifunctor Partial Source # |
Instance details Defined in What4.Partial Methods bimap :: (a -> b) -> (c -> d) -> Partial a c -> Partial b d Source # first :: (a -> b) -> Partial a c -> Partial b c Source # second :: (b -> c) -> Partial a b -> Partial a c Source #
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) Source #
Eq2 Partial Source # |
Instance details Defined in What4.Partial Methods liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Partial a c -> Partial b d -> Bool Source #
Ord2 Partial Source # |
Instance details Defined in What4.Partial Methods liftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> Partial a c -> Partial b d -> Ordering Source #
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 Source # liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [Partial a b] -> ShowS Source #
Generic1 (Partial p :: Type -> Type) Source # |
Instance details Defined in What4.Partial Associated Types type Rep1 (Partial p) :: k -> Type Source # Methods from1 :: forall (a :: k). Partial p a -> Rep1 (Partial p) a Source # to1 :: forall (a :: k). Rep1 (Partial p) a -> Partial p a Source #
Foldable (Partial p) Source # |

Instance details

Defined in What4.Partial

Methods

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

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

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

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

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

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

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

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

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

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

null :: Partial p a -> Bool Source #

length :: Partial p a -> Int Source #

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

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

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

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

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

Eq p => Eq1 (Partial p) Source # |
Instance details Defined in What4.Partial Methods liftEq :: (a -> b -> Bool) -> Partial p a -> Partial p b -> Bool Source #
Ord p => Ord1 (Partial p) Source # |
Instance details Defined in What4.Partial Methods liftCompare :: (a -> b -> Ordering) -> Partial p a -> Partial p b -> Ordering Source #
Show p => Show1 (Partial p) Source # |
Instance details Defined in What4.Partial Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Partial p a -> ShowS Source # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Partial p a] -> ShowS Source #
Traversable (Partial p) Source # |
Instance details Defined in What4.Partial Methods traverse :: Applicative f => (a -> f b) -> Partial p a -> f (Partial p b) Source # sequenceA :: Applicative f => Partial p (f a) -> f (Partial p a) Source # mapM :: Monad m => (a -> m b) -> Partial p a -> m (Partial p b) Source # sequence :: Monad m => Partial p (m a) -> m (Partial p a) Source #
Functor (Partial p) Source # |
Instance details Defined in What4.Partial Methods fmap :: (a -> b) -> Partial p a -> Partial p b Source # (<$) :: a -> Partial p b -> Partial p a Source #
(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) Source #

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

toConstr :: Partial p v -> Constr Source #

dataTypeOf :: Partial p v -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Generic (Partial p v) Source # |
Instance details Defined in What4.Partial Associated Types type Rep (Partial p v) :: Type -> Type Source # Methods from :: Partial p v -> Rep (Partial p v) x Source # to :: Rep (Partial p v) x -> Partial p v Source #
(Show p, Show v) => Show (Partial p v) Source # |
Instance details Defined in What4.Partial Methods showsPrec :: Int -> Partial p v -> ShowS Source # show :: Partial p v -> String Source # showList :: [Partial p v] -> ShowS Source #
(Eq p, Eq v) => Eq (Partial p v) Source # |
Instance details Defined in What4.Partial Methods (==) :: Partial p v -> Partial p v -> Bool Source # (/=) :: Partial p v -> Partial p v -> Bool Source #
(Ord p, Ord v) => Ord (Partial p v) Source # |

Instance details

Defined in What4.Partial

Methods

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

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

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

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

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

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

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

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.5.1-DBkqM8wdl409irRO83zDXw" '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.5.1-DBkqM8wdl409irRO83zDXw" '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

Instances details

Generic1 (PartialWithErr e p :: Type -> Type) Source # |
Instance details Defined in What4.Partial Associated Types type Rep1 (PartialWithErr e p) :: k -> Type Source # Methods from1 :: forall (a :: k). PartialWithErr e p a -> Rep1 (PartialWithErr e p) a Source # to1 :: forall (a :: k). Rep1 (PartialWithErr e p) a -> PartialWithErr e p a Source #
Bifoldable (PartialWithErr e) Source # |
Instance details Defined in What4.Partial Methods bifold :: Monoid m => PartialWithErr e m m -> m Source # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> PartialWithErr e a b -> m Source # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> PartialWithErr e a b -> c Source # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> PartialWithErr e a b -> c Source #
Bifunctor (PartialWithErr e) Source # |
Instance details Defined in What4.Partial Methods bimap :: (a -> b) -> (c -> d) -> PartialWithErr e a c -> PartialWithErr e b d Source # first :: (a -> b) -> PartialWithErr e a c -> PartialWithErr e b c Source # second :: (b -> c) -> PartialWithErr e a b -> PartialWithErr e a c Source #
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) Source #
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 Source #
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 Source #
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 Source # liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [PartialWithErr e a b] -> ShowS Source #
Foldable (PartialWithErr e p) Source # |

Instance details

Defined in What4.Partial

Methods

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

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

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

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

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

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

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

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

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

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

null :: PartialWithErr e p a -> Bool Source #

length :: PartialWithErr e p a -> Int Source #

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

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

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

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

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

(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 Source #
(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 Source #
(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 Source # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [PartialWithErr e p a] -> ShowS Source #
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) Source #

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

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

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

Functor (PartialWithErr e p) Source # |
Instance details Defined in What4.Partial Methods fmap :: (a -> b) -> PartialWithErr e p a -> PartialWithErr e p b Source # (<$) :: a -> PartialWithErr e p b -> PartialWithErr e p a Source #
(Data p, Data v, Data e) => 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) Source #

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

toConstr :: PartialWithErr e p v -> Constr Source #

dataTypeOf :: PartialWithErr e p v -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Generic (PartialWithErr e p v) Source # |
Instance details Defined in What4.Partial Associated Types type Rep (PartialWithErr e p v) :: Type -> Type Source # Methods from :: PartialWithErr e p v -> Rep (PartialWithErr e p v) x Source # to :: Rep (PartialWithErr e p v) x -> PartialWithErr e p v Source #
(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 Source # show :: PartialWithErr e p v -> String Source # showList :: [PartialWithErr e p v] -> ShowS Source #
(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 Source # (/=) :: PartialWithErr e p v -> PartialWithErr e p v -> Bool Source #
(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 Source #

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

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

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

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

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

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

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.5.1-DBkqM8wdl409irRO83zDXw" '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.5.1-DBkqM8wdl409irRO83zDXw" '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 #

mkPE :: IsExpr p => p BaseBoolType -> a -> PartExpr (p BaseBoolType) a 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.

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

``joinMaybePE` = `fromMaybe` `Unassigned``.

## 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

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

#### Instances

Instances details

IsExpr (SymExpr sym) => MonadTrans (PartialT sym) Source # |
Instance details Defined in What4.Partial Methods lift :: Monad m => m a -> PartialT sym m a Source #
(IsExpr (SymExpr sym), MonadFail m) => MonadFail (PartialT sym m) Source # |
Instance details Defined in What4.Partial Methods fail :: String -> PartialT sym m a Source #
(IsExpr (SymExpr sym), MonadIO m) => MonadIO (PartialT sym m) Source # |
Instance details Defined in What4.Partial Methods liftIO :: IO a -> PartialT sym m a Source #
(IsExpr (SymExpr sym), Monad m) => Applicative (PartialT sym m) Source # |

Instance details

Defined in What4.Partial

Methods

pure :: a -> PartialT sym m a Source #

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

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

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

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

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 Source # (<$) :: a -> PartialT sym m b -> PartialT sym m a Source #
(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 Source # (>>) :: PartialT sym m a -> PartialT sym m b -> PartialT sym m b Source # return :: a -> PartialT sym m a Source #

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