-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Maybe
-- Copyright : (c) Joel Burget
--                 Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Symbolic option type, symbolic version of Haskell's 'Maybe' type.
-----------------------------------------------------------------------------

{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Maybe (
  -- * Constructing optional values
    sJust, sNothing, liftMaybe
  -- * Destructing optionals
  , maybe
  -- * Mapping functions
  , map
  -- * Scrutinizing the branches of an option
  , isNothing, isJust, fromMaybe, fromJust
  ) where

import           Prelude hiding (maybe, map)
import qualified Prelude

import Data.Proxy (Proxy(Proxy))

import Data.SBV.Core.Data
import Data.SBV.Core.Model () -- instances only

-- For doctest use only
--
-- $setup
-- >>> import Data.SBV.Core.Model
-- >>> import Data.SBV.Provers.Prover

-- | The symbolic 'Nothing'
--
-- >>> sNothing :: SMaybe Integer
-- Nothing :: SMaybe Integer
sNothing :: forall a. SymVal a => SMaybe a
sNothing :: SMaybe a
sNothing = SVal -> SMaybe a
forall a. SVal -> SBV a
SBV (SVal -> SMaybe a) -> SVal -> SMaybe a
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Maybe CVal -> CVal
CMaybe Maybe CVal
forall a. Maybe a
Nothing
  where k :: Kind
k = Proxy (Maybe a) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (Maybe a)
forall k (t :: k). Proxy t
Proxy @(Maybe a))

-- | Check if the symbolic value is nothing.
--
-- >>> isNothing (sNothing :: SMaybe Integer)
-- True
-- >>> isNothing (sJust (literal "nope"))
-- False
isNothing :: SymVal a => SMaybe a -> SBool
isNothing :: SMaybe a -> SBool
isNothing = SBool -> (SBV a -> SBool) -> SMaybe a -> SBool
forall a b.
(SymVal a, SymVal b) =>
SBV b -> (SBV a -> SBV b) -> SMaybe a -> SBV b
maybe SBool
sTrue (SBool -> SBV a -> SBool
forall a b. a -> b -> a
const SBool
sFalse)

-- | Construct an @SMaybe a@ from an @SBV a@
--
-- >>> sJust 3
-- Just 3 :: SMaybe Integer
sJust :: forall a. SymVal a => SBV a -> SMaybe a
sJust :: SBV a -> SMaybe a
sJust SBV a
sa
  | Just a
a <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa
  = Maybe a -> SMaybe a
forall a. SymVal a => a -> SBV a
literal (a -> Maybe a
forall a. a -> Maybe a
Just a
a)
  | Bool
True
  = SVal -> SMaybe a
forall a. SVal -> SBV a
SBV (SVal -> SMaybe a) -> SVal -> SMaybe a
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kMaybe (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
  where ka :: Kind
ka     = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
        kMaybe :: Kind
kMaybe = Kind -> Kind
KMaybe Kind
ka

        res :: State -> IO SV
res State
st = do SV
asv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                    State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kMaybe (SBVExpr -> IO SV) -> SBVExpr -> IO SV
forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (Kind -> Bool -> Op
MaybeConstructor Kind
ka Bool
True) [SV
asv]

-- | 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.
isJust :: SymVal a => SMaybe a -> SBool
isJust :: SMaybe a -> SBool
isJust = SBool -> (SBV a -> SBool) -> SMaybe a -> SBool
forall a b.
(SymVal a, SymVal b) =>
SBV b -> (SBV a -> SBV b) -> SMaybe a -> SBV b
maybe SBool
sFalse (SBool -> SBV a -> SBool
forall a b. a -> b -> a
const SBool
sTrue)

-- | 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.
fromMaybe :: SymVal a => SBV a -> SMaybe a -> SBV a
fromMaybe :: SBV a -> SMaybe a -> SBV a
fromMaybe SBV a
def = SBV a -> (SBV a -> SBV a) -> SMaybe a -> SBV a
forall a b.
(SymVal a, SymVal b) =>
SBV b -> (SBV a -> SBV b) -> SMaybe a -> SBV b
maybe SBV a
def SBV a -> SBV a
forall a. a -> a
id

-- | 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.
fromJust :: forall a. SymVal a => SMaybe a -> SBV a
fromJust :: SMaybe a -> SBV a
fromJust SMaybe a
ma
  | Just (Just a
x) <- SMaybe a -> Maybe (Maybe a)
forall a. SymVal a => SBV a -> Maybe a
unliteral SMaybe a
ma
  = a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
x
  | Bool
True
  = SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
ka (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
  where ka :: Kind
ka     = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
        kMaybe :: Kind
kMaybe = Kind -> Kind
KMaybe Kind
ka

        -- We play the usual trick here of creating a just value
        -- and asserting equivalence under implication. This will
        -- be underspecified as required should the value
        -- received be `Nothing`.
        res :: State -> IO SV
res State
st = do -- grab an internal variable and make a Maybe out of it
                    SV
e  <- State -> Kind -> IO SV
internalVariable State
st Kind
ka
                    SV
es <- State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kMaybe (Op -> [SV] -> SBVExpr
SBVApp (Kind -> Bool -> Op
MaybeConstructor Kind
ka Bool
True) [SV
e])

                    -- Create the condition that it is equal to the input
                    SV
ms <- State -> SMaybe a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SMaybe a
ma
                    SV
eq <- State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool (Op -> [SV] -> SBVExpr
SBVApp Op
Equal [SV
es, SV
ms])

                    -- Gotta make sure we do this only when input is not nothing
                    SV
caseNothing <- State -> SBool -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st (SMaybe a -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing SMaybe a
ma)
                    SV
require     <- State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool (Op -> [SV] -> SBVExpr
SBVApp Op
Or [SV
caseNothing, SV
eq])

                    -- register the constraint:
                    State -> Bool -> [(String, String)] -> SVal -> IO ()
internalConstraint State
st Bool
False [] (SVal -> IO ()) -> SVal -> IO ()
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache ((State -> IO SV) -> Cached SV) -> (State -> IO SV) -> Cached SV
forall a b. (a -> b) -> a -> b
$ \State
_ -> SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
require

                    -- We're good to go:
                    SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
e

-- | Construct an @SMaybe a@ from a @Maybe (SBV a)@
--
-- >>> liftMaybe (Just (3 :: SInteger))
-- Just 3 :: SMaybe Integer
-- >>> liftMaybe (Nothing :: Maybe SInteger)
-- Nothing :: SMaybe Integer
liftMaybe :: SymVal a => Maybe (SBV a) -> SMaybe a
liftMaybe :: Maybe (SBV a) -> SMaybe a
liftMaybe = SMaybe a -> (SBV a -> SMaybe a) -> Maybe (SBV a) -> SMaybe a
forall b a. b -> (a -> b) -> Maybe a -> b
Prelude.maybe (Maybe a -> SMaybe a
forall a. SymVal a => a -> SBV a
literal Maybe a
forall a. Maybe a
Nothing) SBV a -> SMaybe a
forall a. SymVal a => SBV a -> SMaybe a
sJust

-- | 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
map :: forall a b.  (SymVal a, SymVal b)
    => (SBV a -> SBV b)
    -> SMaybe a
    -> SMaybe b
map :: (SBV a -> SBV b) -> SMaybe a -> SMaybe b
map SBV a -> SBV b
f = SMaybe b -> (SBV a -> SMaybe b) -> SMaybe a -> SMaybe b
forall a b.
(SymVal a, SymVal b) =>
SBV b -> (SBV a -> SBV b) -> SMaybe a -> SBV b
maybe (Maybe b -> SMaybe b
forall a. SymVal a => a -> SBV a
literal Maybe b
forall a. Maybe a
Nothing) (SBV b -> SMaybe b
forall a. SymVal a => SBV a -> SMaybe a
sJust (SBV b -> SMaybe b) -> (SBV a -> SBV b) -> SBV a -> SMaybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SBV b
f)

-- | 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.
maybe :: forall a b.  (SymVal a, SymVal b)
      => SBV b
      -> (SBV a -> SBV b)
      -> SMaybe a
      -> SBV b
maybe :: SBV b -> (SBV a -> SBV b) -> SMaybe a -> SBV b
maybe SBV b
brNothing SBV a -> SBV b
brJust SMaybe a
ma
  | Just (Just a
a) <- SMaybe a -> Maybe (Maybe a)
forall a. SymVal a => SBV a -> Maybe a
unliteral SMaybe a
ma
  = SBV a -> SBV b
brJust (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
a)
  | Just Maybe a
Nothing  <- SMaybe a -> Maybe (Maybe a)
forall a. SymVal a => SBV a -> Maybe a
unliteral SMaybe a
ma
  = SBV b
brNothing
  | Bool
True
  = SVal -> SBV b
forall a. SVal -> SBV a
SBV (SVal -> SBV b) -> SVal -> SBV b
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kb (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
  where ka :: Kind
ka = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
        kb :: Kind
kb = Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)

        res :: State -> IO SV
res State
st = do SV
mav <- State -> SMaybe a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SMaybe a
ma

                    let justVal :: SBV a
justVal = SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
ka (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache ((State -> IO SV) -> Cached SV) -> (State -> IO SV) -> Cached SV
forall a b. (a -> b) -> a -> b
$ \State
_ -> State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
ka (SBVExpr -> IO SV) -> SBVExpr -> IO SV
forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp Op
MaybeAccess [SV
mav]

                        justRes :: SBV b
justRes = SBV a -> SBV b
brJust SBV a
forall a. SBV a
justVal

                    SV
br1 <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
brNothing
                    SV
br2 <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
justRes

                    -- Do we have a value?
                    SV
noVal <- State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool (SBVExpr -> IO SV) -> SBVExpr -> IO SV
forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (Kind -> Bool -> Op
MaybeIs Kind
ka Bool
False) [SV
mav]
                    State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kb (SBVExpr -> IO SV) -> SBVExpr -> IO SV
forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp Op
Ite [SV
noVal, SV
br1, SV
br2]