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

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

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Either (
        -- * Constructing sums
          sLeft, sRight, liftEither
        -- * Destructing sums
        , either
        -- * Mapping functions
        , bimap, first, second
        -- * Scrutinizing branches of a sum
        , isLeft, isRight, fromLeft, fromRight
      ) where

    import           Prelude hiding (either)
    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

    -- | Construct an @SEither a b@ from an @SBV a@
    --
    -- >>> sLeft 3 :: SEither Integer Bool
    -- Left 3 :: SEither Integer Bool
    sLeft :: forall a b. (SymVal a, SymVal b) => SBV a -> SEither a b
    sLeft :: SBV a -> SEither a b
    sLeft sa :: SBV a
    sa
      | Just a :: a
    a <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    sa
      = Either a b -> SEither a b
    forall a. SymVal a => a -> SBV a
    literal (a -> Either a b
    forall a b. a -> Either a b
    Left a
    a)
      | Bool
    True
      = SVal -> SEither a b
    forall a. SVal -> SBV a
    SBV (SVal -> SEither a b) -> SVal -> SEither a b
    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
    $ 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 k1 :: Kind
    k1 = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)
            k2 :: Kind
    k2 = Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)
            k :: Kind
    k  = Kind -> Kind -> Kind
    KEither Kind
    k1 Kind
    k2

            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
    k (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp (Kind -> Kind -> Bool -> Op
    EitherConstructor Kind
    k1 Kind
    k2 Bool
    False) [SV
    asv]

    -- | Return 'sTrue' if the given symbolic value is 'Left', 'sFalse' otherwise
    --
    -- >>> isLeft (sLeft 3 :: SEither Integer Bool)
    -- True
    -- >>> isLeft (sRight sTrue :: SEither Integer Bool)
    -- False
    isLeft :: (SymVal a, SymVal b) => SEither a b -> SBV Bool
    isLeft :: SEither a b -> SBV Bool
    isLeft = (SBV a -> SBV Bool)
    -> (SBV b -> SBV Bool) -> SEither a b -> SBV Bool
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    (SBV a -> SBV c) -> (SBV b -> SBV c) -> SEither a b -> SBV c
    either (SBV Bool -> SBV a -> SBV Bool
    forall a b. a -> b -> a
    const SBV Bool
    sTrue) (SBV Bool -> SBV b -> SBV Bool
    forall a b. a -> b -> a
    const SBV Bool
    sFalse)

    -- | Construct an @SEither a b@ from an @SBV b@
    --
    -- >>> sRight sFalse :: SEither Integer Bool
    -- Right False :: SEither Integer Bool
    sRight :: forall a b. (SymVal a, SymVal b) => SBV b -> SEither a b
    sRight :: SBV b -> SEither a b
    sRight sb :: SBV b
    sb
      | Just b :: b
    b <- SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    sb
      = Either a b -> SEither a b
    forall a. SymVal a => a -> SBV a
    literal (b -> Either a b
    forall a b. b -> Either a b
    Right b
    b)
      | Bool
    True
      = SVal -> SEither a b
    forall a. SVal -> SBV a
    SBV (SVal -> SEither a b) -> SVal -> SEither a b
    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
    $ 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 k1 :: Kind
    k1 = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)
            k2 :: Kind
    k2 = Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)
            k :: Kind
    k  = Kind -> Kind -> Kind
    KEither Kind
    k1 Kind
    k2

            res :: State -> IO SV
    res st :: State
    st = do SV
    bsv <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    sb
                        State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp (Kind -> Kind -> Bool -> Op
    EitherConstructor Kind
    k1 Kind
    k2 Bool
    True) [SV
    bsv]

    -- | Return 'sTrue' if the given symbolic value is 'Right', 'sFalse' otherwise
    --
    -- >>> isRight (sLeft 3 :: SEither Integer Bool)
    -- False
    -- >>> isRight (sRight sTrue :: SEither Integer Bool)
    -- True
    isRight :: (SymVal a, SymVal b) => SEither a b -> SBV Bool
    isRight :: SEither a b -> SBV Bool
    isRight = (SBV a -> SBV Bool)
    -> (SBV b -> SBV Bool) -> SEither a b -> SBV Bool
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    (SBV a -> SBV c) -> (SBV b -> SBV c) -> SEither a b -> SBV c
    either (SBV Bool -> SBV a -> SBV Bool
    forall a b. a -> b -> a
    const SBV Bool
    sFalse) (SBV Bool -> SBV b -> SBV Bool
    forall a b. a -> b -> a
    const SBV Bool
    sTrue)

    -- | Construct an @SEither a b@ from an @Either (SBV a) (SBV b)@
    --
    -- >>> liftEither (Left 3 :: Either SInteger SBool)
    -- Left 3 :: SEither Integer Bool
    -- >>> liftEither (Right sTrue :: Either SInteger SBool)
    -- Right True :: SEither Integer Bool
    liftEither :: (SymVal a, SymVal b) => Either (SBV a) (SBV b) -> SEither a b
    liftEither :: Either (SBV a) (SBV b) -> SEither a b
    liftEither = (SBV a -> SEither a b)
    -> (SBV b -> SEither a b) -> Either (SBV a) (SBV b) -> SEither a b
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    Prelude.either SBV a -> SEither a b
    forall a b. (SymVal a, SymVal b) => SBV a -> SEither a b
    sLeft SBV b -> SEither a b
    forall a b. (SymVal a, SymVal b) => SBV b -> SEither a b
    sRight

    -- | Case analysis for symbolic 'Either's. If the value 'isLeft', apply the
    -- first function; if it 'isRight', apply the second function.
    --
    -- >>> either (*2) (*3) (sLeft 3)
    -- 6 :: SInteger
    -- >>> either (*2) (*3) (sRight 3)
    -- 9 :: SInteger
    -- >>> let f = uninterpret "f" :: SInteger -> SInteger
    -- >>> let g = uninterpret "g" :: SInteger -> SInteger
    -- >>> prove $ \x -> either f g (sLeft x) .== f x
    -- Q.E.D.
    -- >>> prove $ \x -> either f g (sRight x) .== g x
    -- Q.E.D.
    either :: forall a b c. (SymVal a, SymVal b, SymVal c)
           => (SBV a -> SBV c)
           -> (SBV b -> SBV c)
           -> SEither a b
           -> SBV c
    either :: (SBV a -> SBV c) -> (SBV b -> SBV c) -> SEither a b -> SBV c
    either brA :: SBV a -> SBV c
    brA brB :: SBV b -> SBV c
    brB sab :: SEither a b
    sab
      | Just (Left  a :: a
    a) <- SEither a b -> Maybe (Either a b)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SEither a b
    sab
      = SBV a -> SBV c
    brA (SBV a -> SBV c) -> SBV a -> SBV c
    forall a b. (a -> b) -> a -> b
    $ a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    a
      | Just (Right b :: b
    b) <- SEither a b -> Maybe (Either a b)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SEither a b
    sab
      = SBV b -> SBV c
    brB (SBV b -> SBV c) -> SBV b -> SBV c
    forall a b. (a -> b) -> a -> b
    $ b -> SBV b
    forall a. SymVal a => a -> SBV a
    literal b
    b
      | Bool
    True
      = SVal -> SBV c
    forall a. SVal -> SBV a
    SBV (SVal -> SBV c) -> SVal -> SBV c
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    kc (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)
            kc :: Kind
    kc = Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c)

            res :: State -> IO SV
    res st :: State
    st = do SV
    abv <- State -> SEither a b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SEither a b
    sab

                        let leftVal :: SBV a
    leftVal  = 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 (Bool -> Op
    EitherAccess Bool
    False) [SV
    abv]
                            rightVal :: SBV a
    rightVal = 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
    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) -> Cached SV) -> (State -> IO SV) -> Cached SV
    forall a b. (a -> b) -> a -> b
    $ \_ -> 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 (Bool -> Op
    EitherAccess Bool
    True)  [SV
    abv]

                            leftRes :: SBV c
    leftRes  = SBV a -> SBV c
    brA SBV a
    forall a. SBV a
    leftVal
                            rightRes :: SBV c
    rightRes = SBV b -> SBV c
    brB SBV b
    forall a. SBV a
    rightVal

                        SV
    br1 <- State -> SBV c -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV c
    leftRes
                        SV
    br2 <- State -> SBV c -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV c
    rightRes

                        --  Which branch are we in? Return the appropriate value:
                        SV
    onLeft <- 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 -> Kind -> Bool -> Op
    EitherIs Kind
    ka Kind
    kb Bool
    False) [SV
    abv]
                        State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    kc (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp Op
    Ite [SV
    onLeft, SV
    br1, SV
    br2]

    -- | Map over both sides of a symbolic 'Either' at the same time
    --
    -- >>> let f = uninterpret "f" :: SInteger -> SInteger
    -- >>> let g = uninterpret "g" :: SInteger -> SInteger
    -- >>> prove $ \x -> fromLeft (bimap f g (sLeft x)) .== f x
    -- Q.E.D.
    -- >>> prove $ \x -> fromRight (bimap f g (sRight x)) .== g x
    -- Q.E.D.
    bimap :: forall a b c d.  (SymVal a, SymVal b, SymVal c, SymVal d)
          => (SBV a -> SBV b)
          -> (SBV c -> SBV d)
          -> SEither a c
          -> SEither b d
    bimap :: (SBV a -> SBV b) -> (SBV c -> SBV d) -> SEither a c -> SEither b d
    bimap brA :: SBV a -> SBV b
    brA brC :: SBV c -> SBV d
    brC = (SBV a -> SEither b d)
    -> (SBV c -> SEither b d) -> SEither a c -> SEither b d
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    (SBV a -> SBV c) -> (SBV b -> SBV c) -> SEither a b -> SBV c
    either (SBV b -> SEither b d
    forall a b. (SymVal a, SymVal b) => SBV a -> SEither a b
    sLeft (SBV b -> SEither b d) -> (SBV a -> SBV b) -> SBV a -> SEither b d
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV a -> SBV b
    brA) (SBV d -> SEither b d
    forall a b. (SymVal a, SymVal b) => SBV b -> SEither a b
    sRight (SBV d -> SEither b d) -> (SBV c -> SBV d) -> SBV c -> SEither b d
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV c -> SBV d
    brC)

    -- | Map over the left side of an 'Either'
    --
    -- >>> let f = uninterpret "f" :: SInteger -> SInteger
    -- >>> prove $ \x -> first f (sLeft x :: SEither Integer Integer) .== sLeft (f x)
    -- Q.E.D.
    -- >>> prove $ \x -> first f (sRight x :: SEither Integer Integer) .== sRight x
    -- Q.E.D.
    first :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b) -> SEither a c -> SEither b c
    first :: (SBV a -> SBV b) -> SEither a c -> SEither b c
    first f :: SBV a -> SBV b
    f = (SBV a -> SBV b) -> (SBV c -> SBV c) -> SEither a c -> SEither b c
    forall a b c d.
    (SymVal a, SymVal b, SymVal c, SymVal d) =>
    (SBV a -> SBV b) -> (SBV c -> SBV d) -> SEither a c -> SEither b d
    bimap SBV a -> SBV b
    f SBV c -> SBV c
    forall a. a -> a
    id

    -- | Map over the right side of an 'Either'
    --
    -- >>> let f = uninterpret "f" :: SInteger -> SInteger
    -- >>> prove $ \x -> second f (sRight x :: SEither Integer Integer) .== sRight (f x)
    -- Q.E.D.
    -- >>> prove $ \x -> second f (sLeft x :: SEither Integer Integer) .== sLeft x
    -- Q.E.D.
    second :: (SymVal a, SymVal b, SymVal c) => (SBV b -> SBV c) -> SEither a b -> SEither a c
    second :: (SBV b -> SBV c) -> SEither a b -> SEither a c
    second = (SBV a -> SBV a) -> (SBV b -> SBV c) -> SEither a b -> SEither a c
    forall a b c d.
    (SymVal a, SymVal b, SymVal c, SymVal d) =>
    (SBV a -> SBV b) -> (SBV c -> SBV d) -> SEither a c -> SEither b d
    bimap SBV a -> SBV a
    forall a. a -> a
    id

    -- | Return the value from the left component. The behavior is undefined if
    -- passed a right value.
    --
    -- >>> fromLeft (sLeft (literal 'a') :: SEither Char Integer)
    -- 'a' :: SChar
    -- >>> prove $ \x -> fromLeft (sLeft x :: SEither Char Integer) .== (x :: SChar)
    -- Q.E.D.
    -- >>> sat $ \x -> x .== (fromLeft (sRight 4 :: SEither Char Integer))
    -- 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.
    fromLeft :: forall a b. (SymVal a, SymVal b) => SEither a b -> SBV a
    fromLeft :: SEither a b -> SBV a
    fromLeft sab :: SEither a b
    sab
      | Just (Left a :: a
    a) <- SEither a b -> Maybe (Either a b)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SEither a b
    sab
      = a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    a
      | 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)
            kb :: Kind
    kb      = Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)
            kEither :: Kind
    kEither = Kind -> Kind -> Kind
    KEither Kind
    ka Kind
    kb

            -- We play the usual trick here of creating a left value and asserting equivalence
            -- under implication. This will be underspecified as required should the value
            -- received be a right thing.
            res :: State -> IO SV
    res st :: State
    st = do -- grab an internal variable and make a left 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
    kEither (Op -> [SV] -> SBVExpr
    SBVApp (Kind -> Kind -> Bool -> Op
    EitherConstructor Kind
    ka Kind
    kb Bool
    False) [SV
    e])

                        -- Create the condition that it is equal to the input
                        SV
    ms <- State -> SEither a b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SEither a b
    sab
                        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 right
                        SV
    caseRight <- State -> SBV Bool -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st (SEither a b -> SBV Bool
    forall a b. (SymVal a, SymVal b) => SEither a b -> SBV Bool
    isRight SEither a b
    sab)
                        SV
    require   <- State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (Op -> [SV] -> SBVExpr
    SBVApp Op
    Or [SV
    caseRight, 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

    -- | Return the value from the right component. The behavior is undefined if
    -- passed a left value.
    --
    -- >>> fromRight (sRight (literal 'a') :: SEither Integer Char)
    -- 'a' :: SChar
    -- >>> prove $ \x -> fromRight (sRight x :: SEither Char Integer) .== (x :: SInteger)
    -- Q.E.D.
    -- >>> sat $ \x -> x .== (fromRight (sLeft (literal 'a') :: SEither Char Integer))
    -- Satisfiable. Model:
    --   s0 = 0 :: Integer
    --
    -- 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.
    fromRight :: forall a b. (SymVal a, SymVal b) => SEither a b -> SBV b
    fromRight :: SEither a b -> SBV b
    fromRight sab :: SEither a b
    sab
      | Just (Right b :: b
    b) <- SEither a b -> Maybe (Either a b)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SEither a b
    sab
      = b -> SBV b
    forall a. SymVal a => a -> SBV a
    literal b
    b
      | 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)
            kEither :: Kind
    kEither = Kind -> Kind -> Kind
    KEither Kind
    ka Kind
    kb

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

                        -- Create the condition that it is equal to the input
                        SV
    ms <- State -> SEither a b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SEither a b
    sab
                        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 left
                        SV
    caseLeft <- State -> SBV Bool -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st (SEither a b -> SBV Bool
    forall a b. (SymVal a, SymVal b) => SEither a b -> SBV Bool
    isLeft SEither a b
    sab)
                        SV
    require  <- State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (Op -> [SV] -> SBVExpr
    SBVApp Op
    Or [SV
    caseLeft, 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

    {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}