    -----------------------------------------------------------------------------
    -- |
    -- 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 FlexibleInstances   #-}
    {-# LANGUAGE Rank2Types          #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications    #-}

    {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

    module Data.SBV.Maybe (
      -- * Constructing optional values
        sJust, sNothing, liftMaybe
      -- * Destructing optionals
      , maybe
      -- * Mapping functions
      , map, map2
      -- * 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 (ite)

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> import Prelude hiding (maybe, map)
    -- >>> import Data.SBV

    -- | The symbolic 'Nothing'.
    --
    -- >>> sNothing :: SMaybe Integer
    -- Nothing :: SMaybe Integer
    sNothing :: forall a. SymVal a => SMaybe a
    sNothing :: forall a. SymVal a => SMaybe a
    sNothing = SVal -> SBV (Maybe a)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (Maybe a)) -> SVal -> SBV (Maybe 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 (forall t. Proxy t
    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 :: forall a. SymVal a => 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 :: SInteger)
    -- Just 3 :: SMaybe Integer
    sJust :: forall a. SymVal a => SBV a -> SMaybe a
    sJust :: forall a. SymVal a => 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 -> SBV (Maybe a)
    forall a. SymVal a => a -> SBV a
    literal (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    a)
      | Bool
    True
      = SVal -> SBV (Maybe a)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (Maybe a)) -> SVal -> SBV (Maybe 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 (forall t. Proxy t
    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 :: forall a. SymVal a => 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 :: forall a. SymVal a => 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 :: forall a. SymVal a => 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 (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)
            res :: State -> IO SV
    res State
    st = do SV
    ms <- State -> SMaybe a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SMaybe a
    ma
                        State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    ka (Op -> [SV] -> SBVExpr
    SBVApp Op
    MaybeAccess [SV
    ms])

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

    -- | Map over two maybe values.
    map2 :: forall a b c. (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b -> SBV c) -> SMaybe a -> SMaybe b -> SMaybe c
    map2 :: forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    (SBV a -> SBV b -> SBV c) -> SMaybe a -> SMaybe b -> SMaybe c
    map2 SBV a -> SBV b -> SBV c
    op SMaybe a
    mx SMaybe b
    my = SBool -> SMaybe c -> SMaybe c -> SMaybe c
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SMaybe a -> SBool
    forall a. SymVal a => SMaybe a -> SBool
    isJust SMaybe a
    mx SBool -> SBool -> SBool
    .&& SMaybe b -> SBool
    forall a. SymVal a => SMaybe a -> SBool
    isJust SMaybe b
    my)
                        (SBV c -> SMaybe c
    forall a. SymVal a => SBV a -> SMaybe a
    sJust (SMaybe a -> SBV a
    forall a. SymVal a => SMaybe a -> SBV a
    fromJust SMaybe a
    mx SBV a -> SBV b -> SBV c
    `op` SMaybe b -> SBV b
    forall a. SymVal a => SMaybe a -> SBV a
    fromJust SMaybe b
    my))
                        SMaybe c
    forall a. SymVal a => SMaybe a
    sNothing

    -- | 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 :: forall a b.
    (SymVal a, SymVal b) =>
    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 (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)
            kb :: Kind
    kb = Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    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]

    -- | Custom 'Num' instance over 'SMaybe'
    instance {-# OVERLAPPING #-} (Ord a, SymVal a, Num a) => Num (SBV (Maybe a)) where
      + :: SBV (Maybe a) -> SBV (Maybe a) -> SBV (Maybe a)
    (+)         = (SBV a -> SBV a -> SBV a)
    -> SBV (Maybe a) -> SBV (Maybe a) -> SBV (Maybe a)
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    (SBV a -> SBV b -> SBV c) -> SMaybe a -> SMaybe b -> SMaybe c
    map2 SBV a -> SBV a -> SBV a
    forall a. Num a => a -> a -> a
    (+)
      (-)         = (SBV a -> SBV a -> SBV a)
    -> SBV (Maybe a) -> SBV (Maybe a) -> SBV (Maybe a)
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    (SBV a -> SBV b -> SBV c) -> SMaybe a -> SMaybe b -> SMaybe c
    map2 (-)
      * :: SBV (Maybe a) -> SBV (Maybe a) -> SBV (Maybe a)
    (*)         = (SBV a -> SBV a -> SBV a)
    -> SBV (Maybe a) -> SBV (Maybe a) -> SBV (Maybe a)
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    (SBV a -> SBV b -> SBV c) -> SMaybe a -> SMaybe b -> SMaybe c
    map2 SBV a -> SBV a -> SBV a
    forall a. Num a => a -> a -> a
    (*)
      abs :: SBV (Maybe a) -> SBV (Maybe a)
    abs         = (SBV a -> SBV a) -> SBV (Maybe a) -> SBV (Maybe a)
    forall a b.
    (SymVal a, SymVal b) =>
    (SBV a -> SBV b) -> SMaybe a -> SMaybe b
    map  SBV a -> SBV a
    forall a. Num a => a -> a
    abs
      signum :: SBV (Maybe a) -> SBV (Maybe a)
    signum      = (SBV a -> SBV a) -> SBV (Maybe a) -> SBV (Maybe a)
    forall a b.
    (SymVal a, SymVal b) =>
    (SBV a -> SBV b) -> SMaybe a -> SMaybe b
    map  SBV a -> SBV a
    forall a. Num a => a -> a
    signum
      fromInteger :: Integer -> SBV (Maybe a)
    fromInteger = SBV a -> SBV (Maybe a)
    forall a. SymVal a => SBV a -> SMaybe a
    sJust (SBV a -> SBV (Maybe a))
    -> (Integer -> SBV a) -> Integer -> SBV (Maybe a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> SBV a
    forall a. Num a => Integer -> a
    fromInteger