1----------------------------------------------------------------------------- 2-- | 3-- Module : Data.SBV.Either 4-- Copyright : (c) Joel Burget 5-- Levent Erkok 6-- License : BSD3 7-- Maintainer: erkokl@gmail.com 8-- Stability : experimental 9-- 10-- Symbolic coproduct, symbolic version of Haskell's 'Either' type. 11----------------------------------------------------------------------------- 12 13{-# LANGUAGE Rank2Types #-} 14{-# LANGUAGE ScopedTypeVariables #-} 15{-# LANGUAGE TypeApplications #-} 16 17{-# OPTIONS_GHC -Wall -Werror #-} 18 19module Data.SBV.Either ( 20 -- * Constructing sums 21 sLeft, sRight, liftEither 22 -- * Destructing sums 23 , either 24 -- * Mapping functions 25 , bimap, first, second 26 -- * Scrutinizing branches of a sum 27 , isLeft, isRight, fromLeft, fromRight 28 ) where 29 30import Prelude hiding (either) 31import qualified Prelude 32 33import Data.Proxy (Proxy(Proxy)) 34 35import Data.SBV.Core.Data 36import Data.SBV.Core.Model () -- instances only 37 38-- For doctest use only 39-- 40-- $setup 41-- >>> import Data.SBV.Core.Model 42-- >>> import Data.SBV.Provers.Prover 43 44-- | Construct an @SEither a b@ from an @SBV a@ 45-- 46-- >>> sLeft 3 :: SEither Integer Bool 47-- Left 3 :: SEither Integer Bool 48sLeft :: forall a b. (SymVal a, SymVal b) => SBV a -> SEither a b 49sLeft sa 50 | Just a <- unliteral sa 51 = literal (Left a) 52 | True 53 = SBV $ SVal k $ Right $ cache res 54 where k1 = kindOf (Proxy @a) 55 k2 = kindOf (Proxy @b) 56 k = KEither k1 k2 57 58 res st = do asv <- sbvToSV st sa 59 newExpr st k $ SBVApp (EitherConstructor k1 k2 False) [asv] 60 61-- | Return 'sTrue' if the given symbolic value is 'Left', 'sFalse' otherwise 62-- 63-- >>> isLeft (sLeft 3 :: SEither Integer Bool) 64-- True 65-- >>> isLeft (sRight sTrue :: SEither Integer Bool) 66-- False 67isLeft :: (SymVal a, SymVal b) => SEither a b -> SBV Bool 68isLeft = either (const sTrue) (const sFalse) 69 70-- | Construct an @SEither a b@ from an @SBV b@ 71-- 72-- >>> sRight sFalse :: SEither Integer Bool 73-- Right False :: SEither Integer Bool 74sRight :: forall a b. (SymVal a, SymVal b) => SBV b -> SEither a b 75sRight sb 76 | Just b <- unliteral sb 77 = literal (Right b) 78 | True 79 = SBV $ SVal k $ Right $ cache res 80 where k1 = kindOf (Proxy @a) 81 k2 = kindOf (Proxy @b) 82 k = KEither k1 k2 83 84 res st = do bsv <- sbvToSV st sb 85 newExpr st k $ SBVApp (EitherConstructor k1 k2 True) [bsv] 86 87-- | Return 'sTrue' if the given symbolic value is 'Right', 'sFalse' otherwise 88-- 89-- >>> isRight (sLeft 3 :: SEither Integer Bool) 90-- False 91-- >>> isRight (sRight sTrue :: SEither Integer Bool) 92-- True 93isRight :: (SymVal a, SymVal b) => SEither a b -> SBV Bool 94isRight = either (const sFalse) (const sTrue) 95 96-- | Construct an @SEither a b@ from an @Either (SBV a) (SBV b)@ 97-- 98-- >>> liftEither (Left 3 :: Either SInteger SBool) 99-- Left 3 :: SEither Integer Bool 100-- >>> liftEither (Right sTrue :: Either SInteger SBool) 101-- Right True :: SEither Integer Bool 102liftEither :: (SymVal a, SymVal b) => Either (SBV a) (SBV b) -> SEither a b 103liftEither = Prelude.either sLeft sRight 104 105-- | Case analysis for symbolic 'Either's. If the value 'isLeft', apply the 106-- first function; if it 'isRight', apply the second function. 107-- 108-- >>> either (*2) (*3) (sLeft 3) 109-- 6 :: SInteger 110-- >>> either (*2) (*3) (sRight 3) 111-- 9 :: SInteger 112-- >>> let f = uninterpret "f" :: SInteger -> SInteger 113-- >>> let g = uninterpret "g" :: SInteger -> SInteger 114-- >>> prove $ \x -> either f g (sLeft x) .== f x 115-- Q.E.D. 116-- >>> prove $ \x -> either f g (sRight x) .== g x 117-- Q.E.D. 118either :: forall a b c. (SymVal a, SymVal b, SymVal c) 119 => (SBV a -> SBV c) 120 -> (SBV b -> SBV c) 121 -> SEither a b 122 -> SBV c 123either brA brB sab 124 | Just (Left a) <- unliteral sab 125 = brA $ literal a 126 | Just (Right b) <- unliteral sab 127 = brB $ literal b 128 | True 129 = SBV $ SVal kc $ Right $ cache res 130 where ka = kindOf (Proxy @a) 131 kb = kindOf (Proxy @b) 132 kc = kindOf (Proxy @c) 133 134 res st = do abv <- sbvToSV st sab 135 136 let leftVal = SBV $ SVal ka $ Right $ cache $ \_ -> newExpr st ka $ SBVApp (EitherAccess False) [abv] 137 rightVal = SBV $ SVal kb $ Right $ cache $ \_ -> newExpr st kb $ SBVApp (EitherAccess True) [abv] 138 139 leftRes = brA leftVal 140 rightRes = brB rightVal 141 142 br1 <- sbvToSV st leftRes 143 br2 <- sbvToSV st rightRes 144 145 -- Which branch are we in? Return the appropriate value: 146 onLeft <- newExpr st KBool $ SBVApp (EitherIs ka kb False) [abv] 147 newExpr st kc $ SBVApp Ite [onLeft, br1, br2] 148 149-- | Map over both sides of a symbolic 'Either' at the same time 150-- 151-- >>> let f = uninterpret "f" :: SInteger -> SInteger 152-- >>> let g = uninterpret "g" :: SInteger -> SInteger 153-- >>> prove $ \x -> fromLeft (bimap f g (sLeft x)) .== f x 154-- Q.E.D. 155-- >>> prove $ \x -> fromRight (bimap f g (sRight x)) .== g x 156-- Q.E.D. 157bimap :: forall a b c d. (SymVal a, SymVal b, SymVal c, SymVal d) 158 => (SBV a -> SBV b) 159 -> (SBV c -> SBV d) 160 -> SEither a c 161 -> SEither b d 162bimap brA brC = either (sLeft . brA) (sRight . brC) 163 164-- | Map over the left side of an 'Either' 165-- 166-- >>> let f = uninterpret "f" :: SInteger -> SInteger 167-- >>> prove $ \x -> first f (sLeft x :: SEither Integer Integer) .== sLeft (f x) 168-- Q.E.D. 169-- >>> prove $ \x -> first f (sRight x :: SEither Integer Integer) .== sRight x 170-- Q.E.D. 171first :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b) -> SEither a c -> SEither b c 172first f = bimap f id 173 174-- | Map over the right side of an 'Either' 175-- 176-- >>> let f = uninterpret "f" :: SInteger -> SInteger 177-- >>> prove $ \x -> second f (sRight x :: SEither Integer Integer) .== sRight (f x) 178-- Q.E.D. 179-- >>> prove $ \x -> second f (sLeft x :: SEither Integer Integer) .== sLeft x 180-- Q.E.D. 181second :: (SymVal a, SymVal b, SymVal c) => (SBV b -> SBV c) -> SEither a b -> SEither a c 182second = bimap id 183 184-- | Return the value from the left component. The behavior is undefined if 185-- passed a right value, i.e., it can return any value. 186-- 187-- >>> fromLeft (sLeft (literal 'a') :: SEither Char Integer) 188-- 'a' :: SChar 189-- >>> prove $ \x -> fromLeft (sLeft x :: SEither Char Integer) .== (x :: SChar) 190-- Q.E.D. 191-- >>> sat $ \x -> x .== (fromLeft (sRight 4 :: SEither Char Integer)) 192-- Satisfiable. Model: 193-- s0 = 'A' :: Char 194-- 195-- Note how we get a satisfying assignment in the last case: The behavior 196-- is unspecified, thus the SMT solver picks whatever satisfies the 197-- constraints, if there is one. 198fromLeft :: forall a b. (SymVal a, SymVal b) => SEither a b -> SBV a 199fromLeft sab 200 | Just (Left a) <- unliteral sab 201 = literal a 202 | True 203 = SBV $ SVal ka $ Right $ cache res 204 where ka = kindOf (Proxy @a) 205 kb = kindOf (Proxy @b) 206 kEither = KEither ka kb 207 208 -- We play the usual trick here of creating a left value and asserting equivalence 209 -- under implication. This will be underspecified as required should the value 210 -- received be a right thing. 211 res st = do -- grab an internal variable and make a left out of it 212 e <- internalVariable st ka 213 es <- newExpr st kEither (SBVApp (EitherConstructor ka kb False) [e]) 214 215 -- Create the condition that it is equal to the input 216 ms <- sbvToSV st sab 217 eq <- newExpr st KBool (SBVApp Equal [es, ms]) 218 219 -- Gotta make sure we do this only when input is not right 220 caseRight <- sbvToSV st (isRight sab) 221 require <- newExpr st KBool (SBVApp Or [caseRight, eq]) 222 223 -- register the constraint: 224 internalConstraint st False [] $ SVal KBool $ Right $ cache $ \_ -> return require 225 226 -- We're good to go 227 return e 228 229-- | Return the value from the right component. The behavior is undefined if 230-- passed a left value, i.e., it can return any value. 231-- 232-- >>> fromRight (sRight (literal 'a') :: SEither Integer Char) 233-- 'a' :: SChar 234-- >>> prove $ \x -> fromRight (sRight x :: SEither Char Integer) .== (x :: SInteger) 235-- Q.E.D. 236-- >>> sat $ \x -> x .== (fromRight (sLeft (literal 'a') :: SEither Char Integer)) 237-- Satisfiable. Model: 238-- s0 = 0 :: Integer 239-- 240-- Note how we get a satisfying assignment in the last case: The behavior 241-- is unspecified, thus the SMT solver picks whatever satisfies the 242-- constraints, if there is one. 243fromRight :: forall a b. (SymVal a, SymVal b) => SEither a b -> SBV b 244fromRight sab 245 | Just (Right b) <- unliteral sab 246 = literal b 247 | True 248 = SBV $ SVal kb $ Right $ cache res 249 where ka = kindOf (Proxy @a) 250 kb = kindOf (Proxy @b) 251 kEither = KEither ka kb 252 253 -- We play the usual trick here of creating a right value and asserting equivalence 254 -- under implication. This will be underspecified as required should the value 255 -- received be a right thing. 256 res st = do -- grab an internal variable and make a right out of it 257 e <- internalVariable st kb 258 es <- newExpr st kEither (SBVApp (EitherConstructor ka kb True) [e]) 259 260 -- Create the condition that it is equal to the input 261 ms <- sbvToSV st sab 262 eq <- newExpr st KBool (SBVApp Equal [es, ms]) 263 264 -- Gotta make sure we do this only when input is not left 265 caseLeft <- sbvToSV st (isLeft sab) 266 require <- newExpr st KBool (SBVApp Or [caseLeft, eq]) 267 268 -- register the constraint: 269 internalConstraint st False [] $ SVal KBool $ Right $ cache $ \_ -> return require 270 271 -- We're good to go 272 return e 273 274{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-} 275