Data.SBV.Either

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

Constructing sums

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

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

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

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

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

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

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

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

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

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

Return the value from the left component. The behavior is undefined if passed a right value, i.e., it can return any 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 = 'A' :: 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

Return the value from the right component. The behavior is undefined if passed a left value, i.e., it can return any 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.