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