-----------------------------------------------------------------------------
-- |
-- 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 SBV a
sa
  | Just 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 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 SBV b
sb
  | Just 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 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 SBV a -> SBV c
brA SBV b -> SBV c
brB SEither a b
sab
  | Just (Left  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) <- 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 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
_ -> 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
_ -> 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 SBV a -> SBV b
brA 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 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 SEither a b
sab
  | Just (Left 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 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
$ \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

-- | 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 SEither a b
sab
  | Just (Right 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 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
$ \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

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