1-----------------------------------------------------------------------------
2-- |
3-- Module    : Data.SBV.Maybe
4-- Copyright : (c) Joel Burget
5--                 Levent Erkok
6-- License   : BSD3
7-- Maintainer: erkokl@gmail.com
8-- Stability : experimental
9--
10-- Symbolic option type, symbolic version of Haskell's 'Maybe' type.
11-----------------------------------------------------------------------------
12
13{-# LANGUAGE Rank2Types          #-}
14{-# LANGUAGE ScopedTypeVariables #-}
15{-# LANGUAGE TypeApplications    #-}
16
17{-# OPTIONS_GHC -Wall -Werror #-}
18
19module Data.SBV.Maybe (
20  -- * Constructing optional values
21    sJust, sNothing, liftMaybe
22  -- * Destructing optionals
23  , maybe
24  -- * Mapping functions
25  , map
26  -- * Scrutinizing the branches of an option
27  , isNothing, isJust, fromMaybe, fromJust
28  ) where
29
30import           Prelude hiding (maybe, map)
31import qualified Prelude
32
33import Data.Proxy (Proxy(Proxy))
34
35import Data.SBV.Core.Data
36import Data.SBV.Core.Model () -- instances only
37
38-- For doctest use only
39--
40-- $setup
41-- >>> import Data.SBV.Core.Model
42-- >>> import Data.SBV.Provers.Prover
43
44-- | The symbolic 'Nothing'
45--
46-- >>> sNothing :: SMaybe Integer
47-- Nothing :: SMaybe Integer
48sNothing :: forall a. SymVal a => SMaybe a
49sNothing = SBV $ SVal k $ Left $ CV k $ CMaybe Nothing
50  where k = kindOf (Proxy @(Maybe a))
51
52-- | Check if the symbolic value is nothing.
53--
54-- >>> isNothing (sNothing :: SMaybe Integer)
55-- True
56-- >>> isNothing (sJust (literal "nope"))
57-- False
58isNothing :: SymVal a => SMaybe a -> SBool
59isNothing = maybe sTrue (const sFalse)
60
61-- | Construct an @SMaybe a@ from an @SBV a@
62--
63-- >>> sJust 3
64-- Just 3 :: SMaybe Integer
65sJust :: forall a. SymVal a => SBV a -> SMaybe a
66sJust sa
67  | Just a <- unliteral sa
68  = literal (Just a)
69  | True
70  = SBV $ SVal kMaybe $ Right $ cache res
71  where ka     = kindOf (Proxy @a)
72        kMaybe = KMaybe ka
73
74        res st = do asv <- sbvToSV st sa
75                    newExpr st kMaybe $ SBVApp (MaybeConstructor ka True) [asv]
76
77-- | Check if the symbolic value is not nothing.
78--
79-- >>> isJust (sNothing :: SMaybe Integer)
80-- False
81-- >>> isJust (sJust (literal "yep"))
82-- True
83-- >>> prove $ \x -> isJust (sJust (x :: SInteger))
84-- Q.E.D.
85isJust :: SymVal a => SMaybe a -> SBool
86isJust = maybe sFalse (const sTrue)
87
88-- | Return the value of an optional value. The default is returned if Nothing. Compare to 'fromJust'.
89--
90-- >>> fromMaybe 2 (sNothing :: SMaybe Integer)
91-- 2 :: SInteger
92-- >>> fromMaybe 2 (sJust 5 :: SMaybe Integer)
93-- 5 :: SInteger
94-- >>> prove $ \x -> fromMaybe x (sNothing :: SMaybe Integer) .== x
95-- Q.E.D.
96-- >>> prove $ \x -> fromMaybe (x+1) (sJust x :: SMaybe Integer) .== x
97-- Q.E.D.
98fromMaybe :: SymVal a => SBV a -> SMaybe a -> SBV a
99fromMaybe def = maybe def id
100
101-- | Return the value of an optional value. The behavior is undefined if
102-- passed Nothing, i.e., it can return any value. Compare to 'fromMaybe'.
103--
104-- >>> fromJust (sJust (literal 'a'))
105-- 'a' :: SChar
106-- >>> prove $ \x -> fromJust (sJust x) .== (x :: SChar)
107-- Q.E.D.
108-- >>> sat $ \x -> x .== (fromJust sNothing :: SChar)
109-- Satisfiable. Model:
110--   s0 = 'A' :: Char
111--
112-- Note how we get a satisfying assignment in the last case: The behavior
113-- is unspecified, thus the SMT solver picks whatever satisfies the
114-- constraints, if there is one.
115fromJust :: forall a. SymVal a => SMaybe a -> SBV a
116fromJust ma
117  | Just (Just x) <- unliteral ma
118  = literal x
119  | True
120  = SBV $ SVal ka $ Right $ cache res
121  where ka     = kindOf (Proxy @a)
122        kMaybe = KMaybe ka
123
124        -- We play the usual trick here of creating a just value
125        -- and asserting equivalence under implication. This will
126        -- be underspecified as required should the value
127        -- received be `Nothing`.
128        res st = do -- grab an internal variable and make a Maybe out of it
129                    e  <- internalVariable st ka
130                    es <- newExpr st kMaybe (SBVApp (MaybeConstructor ka True) [e])
131
132                    -- Create the condition that it is equal to the input
133                    ms <- sbvToSV st ma
134                    eq <- newExpr st KBool (SBVApp Equal [es, ms])
135
136                    -- Gotta make sure we do this only when input is not nothing
137                    caseNothing <- sbvToSV st (isNothing ma)
138                    require     <- newExpr st KBool (SBVApp Or [caseNothing, eq])
139
140                    -- register the constraint:
141                    internalConstraint st False [] $ SVal KBool $ Right $ cache $ \_ -> return require
142
143                    -- We're good to go:
144                    return e
145
146-- | Construct an @SMaybe a@ from a @Maybe (SBV a)@
147--
148-- >>> liftMaybe (Just (3 :: SInteger))
149-- Just 3 :: SMaybe Integer
150-- >>> liftMaybe (Nothing :: Maybe SInteger)
151-- Nothing :: SMaybe Integer
152liftMaybe :: SymVal a => Maybe (SBV a) -> SMaybe a
153liftMaybe = Prelude.maybe (literal Nothing) sJust
154
155-- | Map over the 'Just' side of a 'Maybe'
156--
157-- >>> prove $ \x -> fromJust (map (+1) (sJust x)) .== x+1
158-- Q.E.D.
159-- >>> let f = uninterpret "f" :: SInteger -> SBool
160-- >>> prove $ \x -> map f (sJust x) .== sJust (f x)
161-- Q.E.D.
162-- >>> map f sNothing .== sNothing
163-- True
164map :: forall a b.  (SymVal a, SymVal b)
165    => (SBV a -> SBV b)
166    -> SMaybe a
167    -> SMaybe b
168map f = maybe (literal Nothing) (sJust . f)
169
170-- | Case analysis for symbolic 'Maybe's. If the value 'isNothing', return the
171-- default value; if it 'isJust', apply the function.
172--
173-- >>> maybe 0 (`sMod` 2) (sJust (3 :: SInteger))
174-- 1 :: SInteger
175-- >>> maybe 0 (`sMod` 2) (sNothing :: SMaybe Integer)
176-- 0 :: SInteger
177-- >>> let f = uninterpret "f" :: SInteger -> SBool
178-- >>> prove $ \x d -> maybe d f (sJust x) .== f x
179-- Q.E.D.
180-- >>> prove $ \d -> maybe d f sNothing .== d
181-- Q.E.D.
182maybe :: forall a b.  (SymVal a, SymVal b)
183      => SBV b
184      -> (SBV a -> SBV b)
185      -> SMaybe a
186      -> SBV b
187maybe brNothing brJust ma
188  | Just (Just a) <- unliteral ma
189  = brJust (literal a)
190  | Just Nothing  <- unliteral ma
191  = brNothing
192  | True
193  = SBV $ SVal kb $ Right $ cache res
194  where ka = kindOf (Proxy @a)
195        kb = kindOf (Proxy @b)
196
197        res st = do mav <- sbvToSV st ma
198
199                    let justVal = SBV $ SVal ka $ Right $ cache $ \_ -> newExpr st ka $ SBVApp MaybeAccess [mav]
200
201                        justRes = brJust justVal
202
203                    br1 <- sbvToSV st brNothing
204                    br2 <- sbvToSV st justRes
205
206                    -- Do we have a value?
207                    noVal <- newExpr st KBool $ SBVApp (MaybeIs ka False) [mav]
208                    newExpr st kb $ SBVApp Ite [noVal, br1, br2]
209