    -----------------------------------------------------------------------------
    -- |
    -- 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 sa :: SBV a
    sa
      | Just a :: 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 st :: 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 def :: 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. 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.
    fromJust :: forall a. SymVal a => SMaybe a -> SBV a
    fromJust :: SMaybe a -> SBV a
    fromJust ma :: SMaybe a
    ma
      | Just (Just x :: 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 st :: 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
    $ \_ -> 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 f :: 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 brNothing :: SBV b
    brNothing brJust :: SBV a -> SBV b
    brJust ma :: SMaybe a
    ma
      | Just (Just a :: 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 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 st :: 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 -> 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]