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

Data.SBV.Maybe

Contents

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

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
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
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, 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.