sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Data.SBV.Either

Description

Symbolic coproduct, symbolic version of Haskell's Either type.

Synopsis

# Constructing sums

sLeft :: forall a b. (SymVal a, SymVal b) => SBV a -> SEither a b Source #

Construct an SEither a b from an SBV a

>>> sLeft 3 :: SEither Integer Bool
Left 3 :: SEither Integer Bool


sRight :: forall a b. (SymVal a, SymVal b) => SBV b -> SEither a b Source #

Construct an SEither a b from an SBV b

>>> sRight sFalse :: SEither Integer Bool
Right False :: SEither Integer Bool


liftEither :: (SymVal a, SymVal b) => Either (SBV a) (SBV b) -> SEither a b Source #

Construct an SEither a b from an Either (SBV a) (SBV b)

>>> liftEither (Left 3 :: Either SInteger SBool)
Left 3 :: SEither Integer Bool
>>> liftEither (Right sTrue :: Either SInteger SBool)
Right True :: SEither Integer Bool


# Destructing sums

either :: forall a b c. (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV c) -> (SBV b -> SBV c) -> SEither a b -> SBV c Source #

Case analysis for symbolic Eithers. If the value isLeft, apply the first function; if it isRight, apply the second function.

>>> either (*2) (*3) (sLeft 3)
6 :: SInteger
>>> either (*2) (*3) (sRight 3)
9 :: SInteger
>>> let f = uninterpret "f" :: SInteger -> SInteger
>>> let g = uninterpret "g" :: SInteger -> SInteger
>>> prove $\x -> either f g (sLeft x) .== f x Q.E.D. >>> prove$ \x -> either f g (sRight x) .== g x
Q.E.D.


# Mapping functions

bimap :: forall a b c d. (SymVal a, SymVal b, SymVal c, SymVal d) => (SBV a -> SBV b) -> (SBV c -> SBV d) -> SEither a c -> SEither b d Source #

Map over both sides of a symbolic Either at the same time

>>> let f = uninterpret "f" :: SInteger -> SInteger
>>> let g = uninterpret "g" :: SInteger -> SInteger
>>> prove $\x -> fromLeft (bimap f g (sLeft x)) .== f x Q.E.D. >>> prove$ \x -> fromRight (bimap f g (sRight x)) .== g x
Q.E.D.


first :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b) -> SEither a c -> SEither b c Source #

Map over the left side of an Either

>>> let f = uninterpret "f" :: SInteger -> SInteger
>>> prove $\x -> first f (sLeft x :: SEither Integer Integer) .== sLeft (f x) Q.E.D. >>> prove$ \x -> first f (sRight x :: SEither Integer Integer) .== sRight x
Q.E.D.


second :: (SymVal a, SymVal b, SymVal c) => (SBV b -> SBV c) -> SEither a b -> SEither a c Source #

Map over the right side of an Either

>>> let f = uninterpret "f" :: SInteger -> SInteger
>>> prove $\x -> second f (sRight x :: SEither Integer Integer) .== sRight (f x) Q.E.D. >>> prove$ \x -> second f (sLeft x :: SEither Integer Integer) .== sLeft x
Q.E.D.


# Scrutinizing branches of a sum

isLeft :: (SymVal a, SymVal b) => SEither a b -> SBV Bool Source #

Return sTrue if the given symbolic value is Left, sFalse otherwise

>>> isLeft (sLeft 3 :: SEither Integer Bool)
True
>>> isLeft (sRight sTrue :: SEither Integer Bool)
False


isRight :: (SymVal a, SymVal b) => SEither a b -> SBV Bool Source #

Return sTrue if the given symbolic value is Right, sFalse otherwise

>>> isRight (sLeft 3 :: SEither Integer Bool)
False
>>> isRight (sRight sTrue :: SEither Integer Bool)
True


fromLeft :: forall a b. (SymVal a, SymVal b) => SEither a b -> SBV a Source #

Return the value from the left component. The behavior is undefined if passed a right value.

>>> fromLeft (sLeft (literal 'a') :: SEither Char Integer)
'a' :: SChar
>>> prove $\x -> fromLeft (sLeft x :: SEither Char Integer) .== (x :: SChar) Q.E.D. >>> sat$ \x -> x .== (fromLeft (sRight 4 :: SEither Char Integer))
Satisfiable. Model:
s0 = '\NUL' :: Char


Note how we get a satisfying assignment in the last case: The behavior is unspecified, thus the SMT solver picks whatever satisfies the constraints, if there is one.

fromRight :: forall a b. (SymVal a, SymVal b) => SEither a b -> SBV b Source #

Return the value from the right component. The behavior is undefined if passed a left value.

>>> fromRight (sRight (literal 'a') :: SEither Integer Char)
'a' :: SChar
>>> prove $\x -> fromRight (sRight x :: SEither Char Integer) .== (x :: SInteger) Q.E.D. >>> sat$ \x -> x .== (fromRight (sLeft (literal 'a') :: SEither Char Integer))
Satisfiable. Model:
s0 = 0 :: Integer


Note how we get a satisfying assignment in the last case: The behavior is unspecified, thus the SMT solver picks whatever satisfies the constraints, if there is one.