Copyright	(c) Galois Inc 2014-2020
License	BSD3
Maintainer	Langston Barrett <langston@galois.com>
Safe Haskell	None
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

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 # 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 :: forall (a :: k). Partial p a -> Rep1 (Partial p) a # to1 :: forall (a :: k). 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 :: 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) #
(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.1-F6JmVDCUG2e4tsAmUzrLc2" '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.1-F6JmVDCUG2e4tsAmUzrLc2" '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

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 :: 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 #
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 # 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 :: 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) #
(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.1-F6JmVDCUG2e4tsAmUzrLc2" '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.1-F6JmVDCUG2e4tsAmUzrLc2" '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

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