sbv-10.2: 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 | Safe-Inferred
Language | Haskell2010

Data.SBV.Maybe

Contents

- Constructing optional values
- Destructing optionals
- Mapping functions
- Scrutinizing the branches of an option
- Orphan instances

Description

Symbolic option type, symbolic version of Haskell's `Maybe` type.

Synopsis

- sJust :: forall a. SymVal a => SBV a -> SMaybe a
- sNothing :: forall a. SymVal a => SMaybe a
- liftMaybe :: SymVal a => Maybe (SBV a) -> SMaybe a
- maybe :: forall a b. (SymVal a, SymVal b) => SBV b -> (SBV a -> SBV b) -> SMaybe a -> SBV b
- map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> SMaybe a -> SMaybe b
- map2 :: forall a b c. (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b -> SBV c) -> SMaybe a -> SMaybe b -> SMaybe c
- isNothing :: SymVal a => SMaybe a -> SBool
- isJust :: SymVal a => SMaybe a -> SBool
- fromMaybe :: SymVal a => SBV a -> SMaybe a -> SBV a
- fromJust :: forall a. SymVal a => SMaybe a -> SBV a

# Constructing optional values

sJust :: forall a. SymVal a => SBV a -> SMaybe a Source #

Construct an `SMaybe a` from an `SBV a`.

    >>> sJust (3 :: SInteger)
    Just 3 :: SMaybe Integer

sNothing :: forall a. SymVal a => SMaybe a Source #

The symbolic `Nothing`.

    >>> sNothing :: SMaybe Integer
    Nothing :: SMaybe Integer

liftMaybe :: SymVal a => Maybe (SBV a) -> SMaybe a Source #

Construct an `SMaybe a` from a `Maybe (SBV a)`.

    >>> liftMaybe (Just (3 :: SInteger))
    Just 3 :: SMaybe Integer
    >>> liftMaybe (Nothing :: Maybe SInteger)
    Nothing :: SMaybe Integer

# Destructing optionals

maybe :: forall a b. (SymVal a, SymVal b) => SBV b -> (SBV a -> SBV b) -> SMaybe a -> SBV b Source #

Case analysis for symbolic `Maybe`s. If the value `isNothing`, return the default value; if it `isJust`, apply the function.

    >>> maybe 0 (`sMod` 2) (sJust (3 :: SInteger))
    1 :: SInteger
    >>> maybe 0 (`sMod` 2) (sNothing :: SMaybe Integer)
    0 :: SInteger
    >>> let f = uninterpret "f" :: SInteger -> SBool
    >>> prove $ \x d -> maybe d f (sJust x) .== f x
    Q.E.D.
    >>> prove $ \d -> maybe d f sNothing .== d
    Q.E.D.

# Mapping functions

map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> SMaybe a -> SMaybe b Source #

Map over the `Just` side of a `Maybe`.

    >>> prove $ \x -> fromJust (map (+1) (sJust x)) .== x+(1::SInteger)
    Q.E.D.
    >>> let f = uninterpret "f" :: SInteger -> SBool
    >>> prove $ \x -> map f (sJust x) .== sJust (f x)
    Q.E.D.
    >>> map f sNothing .== sNothing
    True

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

Map over two maybe values.

# Scrutinizing the branches of an option

isNothing :: SymVal a => SMaybe a -> SBool Source #

Check if the symbolic value is nothing.

    >>> isNothing (sNothing :: SMaybe Integer)
    True
    >>> isNothing (sJust (literal "nope"))
    False

isJust :: SymVal a => SMaybe a -> SBool Source #

Check if the symbolic value is not nothing.

    >>> isJust (sNothing :: SMaybe Integer)
    False
    >>> isJust (sJust (literal "yep"))
    True
    >>> prove $ \x -> isJust (sJust (x :: SInteger))
    Q.E.D.

fromMaybe :: SymVal a => SBV a -> SMaybe a -> SBV a Source #

Return the value of an optional value. The default is returned if Nothing. Compare to `fromJust`.

    >>> fromMaybe 2 (sNothing :: SMaybe Integer)
    2 :: SInteger
    >>> fromMaybe 2 (sJust 5 :: SMaybe Integer)
    5 :: SInteger
    >>> prove $ \x -> fromMaybe x (sNothing :: SMaybe Integer) .== x
    Q.E.D.
    >>> prove $ \x -> fromMaybe (x+1) (sJust x :: SMaybe Integer) .== x
    Q.E.D.

fromJust :: forall a. SymVal a => SMaybe a -> SBV a Source #

Return the value of an optional value. The behavior is undefined if passed Nothing, i.e., it can return any value. Compare to `fromMaybe`.

    >>> fromJust (sJust (literal 'a'))
    'a' :: SChar
    >>> prove $ \x -> fromJust (sJust x) .== (x :: SChar)
    Q.E.D.
    >>> sat $ \x -> x .== (fromJust sNothing :: SChar)
    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.

# Orphan instances

(Ord a, SymVal a, Num a) => Num (SBV (Maybe a)) Source # | Custom `Num` instance over `SMaybe`

Instance details

Methods

(+) :: SBV (Maybe a) -> SBV (Maybe a) -> SBV (Maybe a) Source #

(-) :: SBV (Maybe a) -> SBV (Maybe a) -> SBV (Maybe a) Source #

(*) :: SBV (Maybe a) -> SBV (Maybe a) -> SBV (Maybe a) Source #

negate :: SBV (Maybe a) -> SBV (Maybe a) Source #

abs :: SBV (Maybe a) -> SBV (Maybe a) Source #

signum :: SBV (Maybe a) -> SBV (Maybe a) Source #

fromInteger :: Integer -> SBV (Maybe a) Source #