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

Copyright | (c) Joel Burget Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Either

Contents

- Constructing sums
- Destructing sums
- Mapping functions
- Scrutinizing branches of a sum

Description

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

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.