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

Data.SBV.Maybe

Description

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

Synopsis

# Constructing optional values

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

Construct an SMaybe a from an SBV a

>>> sJust 3
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 Maybes. 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 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


# 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. 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 = '\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.