Copyright | (c) Joel Burget Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Symbolic coproduct, symbolic version of Haskell's Either
type.
Synopsis
- sLeft :: forall a b. (SymVal a, SymVal b) => SBV a -> SEither a b
- sRight :: forall a b. (SymVal a, SymVal b) => SBV b -> SEither a b
- liftEither :: (SymVal a, SymVal b) => Either (SBV a) (SBV b) -> SEither a b
- either :: forall a b c. (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV c) -> (SBV b -> SBV c) -> SEither a b -> SBV c
- 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
- first :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b) -> SEither a c -> SEither b c
- second :: (SymVal a, SymVal b, SymVal c) => (SBV b -> SBV c) -> SEither a b -> SEither a c
- isLeft :: (SymVal a, SymVal b) => SEither a b -> SBV Bool
- isRight :: (SymVal a, SymVal b) => SEither a b -> SBV Bool
- fromLeft :: forall a b. (SymVal a, SymVal b) => SEither a b -> SBV a
- fromRight :: forall a b. (SymVal a, SymVal b) => SEither a b -> SBV b
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 Either
s. 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
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, 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 Source #
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.