{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Grisette.Core.Data.Class.EvaluateSymTests (evaluateSymTests) where import Control.Monad.Except (ExceptT (ExceptT)) import Control.Monad.Identity ( Identity (Identity), IdentityT (IdentityT), ) import Control.Monad.Trans.Maybe (MaybeT (MaybeT)) import qualified Control.Monad.Writer.Lazy as WriterLazy import qualified Control.Monad.Writer.Strict as WriterStrict import qualified Data.ByteString as B import Data.Functor.Sum (Sum (InL, InR)) import Data.Int (Int16, Int32, Int64, Int8) import Data.Word (Word16, Word32, Word64, Word8) import GHC.Stack (HasCallStack) import Grisette (TypedSymbol (IndexedSymbol)) import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym)) import Grisette.Core.Data.Class.ITEOp (ITEOp (symIte)) import Grisette.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.&&), (.||))) import Grisette.Core.Data.Class.ModelOps ( ModelOps (emptyModel), ModelRep (buildModel), ) import Grisette.Core.Data.Class.SEq (SEq ((.==))) import Grisette.Core.Data.Class.Solvable (Solvable (con, isym, ssym)) import Grisette.IR.SymPrim.Data.Prim.Model ( ModelValuePair ((::=)), ) import Grisette.IR.SymPrim.Data.SymPrim (SymBool) import Test.Framework (Test, testGroup) import Test.Framework.Providers.HUnit (testCase) import Test.Framework.Providers.QuickCheck2 (testProperty) import Test.HUnit (Assertion, (@?=)) import Test.QuickCheck (ioProperty) concreteEvaluateSymOkProp :: (HasCallStack, EvaluateSym a, Show a, Eq a) => a -> Assertion concreteEvaluateSymOkProp x = evaluateSym True emptyModel x @?= x evaluateSymTests :: Test evaluateSymTests = testGroup "EvaluateSym" [ testGroup "EvaluateSym for common types" [ testGroup "SymBool" [ let model = emptyModel eval :: SymBool -> SymBool eval = evaluateSym False model in testGroup "Empty model / no fill default" [ testCase "con" $ eval (con True) @?= con True, testCase "ssym" $ eval (ssym "a") @?= ssym "a", testCase "isym" $ eval (isym "a" 1) @?= isym "a" 1, testCase ".||" $ eval (ssym "a" .|| ssym "b") @?= ssym "a" .|| ssym "b", testCase ".&&" $ eval (ssym "a" .&& ssym "b") @?= ssym "a" .&& ssym "b", testCase ".==" $ eval ((ssym "a" :: SymBool) .== ssym "b") @?= (ssym "a" :: SymBool) .== ssym "b", testCase "symNot" $ eval (symNot (ssym "a")) @?= symNot (ssym "a"), testCase "symIte" $ eval (symIte (ssym "a") (ssym "b") (ssym "c")) @?= symIte (ssym "a") (ssym "b") (ssym "c") ], let model = emptyModel eval :: SymBool -> SymBool eval = evaluateSym True model in testGroup "Empty model / with fill default" [ testCase "con" $ eval (con True) @?= con True, testCase "ssym" $ eval (ssym "a") @?= con False, testCase "isym" $ eval (isym "a" 1) @?= con False, testCase ".||" $ eval (ssym "a" .|| ssym "b") @?= con False, testCase ".&&" $ eval (ssym "a" .&& ssym "b") @?= con False, testCase ".==" $ eval ((ssym "a" :: SymBool) .== ssym "b") @?= con True, testCase "symNot" $ eval (symNot (ssym "a")) @?= con True, testCase "symIte" $ eval (symIte (ssym "a") (ssym "b") (ssym "c")) @?= con False ], let model = buildModel ( "a" ::= True, IndexedSymbol "a" 1 ::= False, "b" ::= False, "c" ::= True ) eval :: SymBool -> SymBool eval = evaluateSym True model in testGroup "Some model" [ testCase "con" $ eval (con True) @?= con True, testCase "ssym" $ eval (ssym "a") @?= con True, testCase "isym" $ eval (isym "a" 1) @?= con False, testCase ".||" $ eval (ssym "a" .|| ssym "b") @?= con True, testCase ".&&" $ eval (ssym "a" .&& ssym "b") @?= con False, testCase ".==" $ eval ((ssym "a" :: SymBool) .== ssym "b") @?= con False, testCase "symNot" $ eval (symNot (ssym "a")) @?= con False, testCase "symIte" $ eval (symIte (ssym "a") (ssym "b") (ssym "c")) @?= con False ] ], testProperty "Bool" $ ioProperty . concreteEvaluateSymOkProp @Bool, testProperty "Integer" $ ioProperty . concreteEvaluateSymOkProp @Integer, testProperty "Char" $ ioProperty . concreteEvaluateSymOkProp @Char, testProperty "Int" $ ioProperty . concreteEvaluateSymOkProp @Int, testProperty "Int8" $ ioProperty . concreteEvaluateSymOkProp @Int8, testProperty "Int16" $ ioProperty . concreteEvaluateSymOkProp @Int16, testProperty "Int32" $ ioProperty . concreteEvaluateSymOkProp @Int32, testProperty "Int64" $ ioProperty . concreteEvaluateSymOkProp @Int64, testProperty "Word" $ ioProperty . concreteEvaluateSymOkProp @Word, testProperty "Word8" $ ioProperty . concreteEvaluateSymOkProp @Word8, testProperty "Word16" $ ioProperty . concreteEvaluateSymOkProp @Word16, testProperty "Word32" $ ioProperty . concreteEvaluateSymOkProp @Word32, testProperty "Word64" $ ioProperty . concreteEvaluateSymOkProp @Word64, testGroup "List" [ testProperty "[Integer]" $ ioProperty . concreteEvaluateSymOkProp @[Integer], let model = buildModel ("a" ::= True, "b" ::= False) eval :: Bool -> [SymBool] -> [SymBool] eval = flip evaluateSym model in testGroup "[SymBool]" [ testGroup "No fill default" [ testCase "Empty list" $ eval False [] @?= [], testCase "Non-empty list" $ eval False [ssym "a", ssym "b", ssym "c"] @?= [con True, con False, ssym "c"] ], testGroup "Fill default" [ testCase "Empty list" $ eval True [] @?= [], testCase "Non-empty list" $ eval True [ssym "a", ssym "b", ssym "c"] @?= [con True, con False, con False] ] ] ], testGroup "Maybe" [ testProperty "Maybe Integer" $ ioProperty . concreteEvaluateSymOkProp @(Maybe Integer), let model = buildModel ("a" ::= True) eval :: Bool -> Maybe SymBool -> Maybe SymBool eval = flip evaluateSym model in testGroup "Maybe SymBool" [ testGroup "No fill default" [ testCase "Nothing" $ eval False Nothing @?= Nothing, testCase "Just v: v in model" $ eval False (Just (ssym "a")) @?= Just (con True), testCase "Just v: v not in model" $ eval False (Just (ssym "b")) @?= Just (ssym "b") ], testGroup "Fill default" [ testCase "Nothing" $ eval True (Nothing) @?= Nothing, testCase "Just v: v in model" $ eval True (Just (ssym "a")) @?= Just (con True), testCase "Just v: v not in model" $ eval True (Just (ssym "b")) @?= Just (con False) ] ] ], testGroup "Either" [ testProperty "Either Integer Integer" $ ioProperty . concreteEvaluateSymOkProp @(Either Integer Integer), let model = buildModel ("a" ::= True) eval :: Bool -> Either SymBool SymBool -> Either SymBool SymBool eval = flip evaluateSym model in testGroup "Either SymBool SymBool" [ testGroup "No fill default" [ testCase "Left v: v in model" $ eval False (Left (ssym "a")) @?= Left (con True), testCase "Left v: v not in model" $ eval False (Left (ssym "b")) @?= Left (ssym "b"), testCase "Right v: v in model" $ eval False (Right (ssym "a")) @?= Right (con True), testCase "Right v: v not in model" $ eval False (Right (ssym "b")) @?= Right (ssym "b") ], testGroup "Fill default" [ testCase "Left v: v in model" $ eval True (Left (ssym "a")) @?= Left (con True), testCase "Left v: v not in model" $ eval True (Left (ssym "b")) @?= Left (con False), testCase "Right v: v in model" $ eval True (Right (ssym "a")) @?= Right (con True), testCase "Right v: v not in model" $ eval True (Right (ssym "b")) @?= Right (con False) ] ] ], testGroup "MaybeT" [ testProperty "MaybeT Maybe Integer" $ ioProperty . concreteEvaluateSymOkProp @(MaybeT Maybe Integer) . MaybeT, let model = buildModel ("a" ::= True) eval :: Bool -> MaybeT Maybe SymBool -> MaybeT Maybe SymBool eval = flip evaluateSym model in testGroup "MaybeT should work" [ testGroup "No fill default" [ testCase "MaybeT Nothing" $ eval False (MaybeT Nothing) @?= MaybeT Nothing, testCase "MaybeT (Just Nothing)" $ eval False (MaybeT $ Just Nothing) @?= MaybeT (Just Nothing), testCase "MaybeT (Just v): v in model" $ eval False (MaybeT $ Just $ Just (ssym "a")) @?= MaybeT (Just (Just (con True))), testCase "MaybeT (Just v): v not in model" $ eval False (MaybeT $ Just $ Just (ssym "b")) @?= MaybeT (Just (Just (ssym "b"))) ], testGroup "Fill default" [ testCase "MaybeT Nothing" $ eval True (MaybeT Nothing) @?= MaybeT Nothing, testCase "MaybeT (Just Nothing)" $ eval True (MaybeT $ Just Nothing) @?= MaybeT (Just Nothing), testCase "MaybeT (Just v): v in model" $ eval True (MaybeT $ Just $ Just (ssym "a")) @?= MaybeT (Just (Just (con True))), testCase "MaybeT (Just v): v not in model" $ eval True (MaybeT $ Just $ Just (ssym "b")) @?= MaybeT (Just (Just (con False))) ] ] ], testGroup "ExceptT" [ testProperty "ExceptT Integer Maybe Integer" $ ioProperty . concreteEvaluateSymOkProp @(ExceptT Integer Maybe Integer) . ExceptT, let model = buildModel ("a" ::= True) eval :: Bool -> ExceptT SymBool Maybe SymBool -> ExceptT SymBool Maybe SymBool eval = flip evaluateSym model in testGroup "ExceptT SymBool Maybe SymBool" [ testGroup "No fill default" [ testCase "ExceptT Nothing" $ eval False (ExceptT Nothing) @?= ExceptT Nothing, testCase "ExceptT (Just (Left v)): v in model" $ eval False (ExceptT $ Just $ Left $ ssym "a") @?= ExceptT (Just $ Left $ con True), testCase "ExceptT (Just (Left v)): v not in model" $ eval False (ExceptT $ Just $ Left $ ssym "b") @?= ExceptT (Just $ Left $ ssym "b"), testCase "ExceptT (Just (Right v)): v in model" $ eval False (ExceptT $ Just $ Right $ ssym "a") @?= ExceptT (Just $ Right $ con True), testCase "ExceptT (Just (Right v)): v not in model" $ eval False (ExceptT $ Just $ Right $ ssym "b") @?= ExceptT (Just $ Right $ ssym "b") ], testGroup "Fill default" [ testCase "ExceptT Nothing" $ eval True (ExceptT Nothing) @?= ExceptT Nothing, testCase "ExceptT (Just (Left v)): v in model" $ eval True (ExceptT $ Just $ Left $ ssym "a") @?= ExceptT (Just $ Left $ con True), testCase "ExceptT (Just (Left v)): v not in model" $ eval True (ExceptT $ Just $ Left $ ssym "b") @?= ExceptT (Just $ Left $ con False), testCase "ExceptT (Just (Right v)): v in model" $ eval True (ExceptT $ Just $ Right $ ssym "a") @?= ExceptT (Just $ Right $ con True), testCase "ExceptT (Just (Right v)): v not in model" $ eval True (ExceptT $ Just $ Right $ ssym "b") @?= ExceptT (Just $ Right $ con False) ] ] ], testProperty "()" (ioProperty . concreteEvaluateSymOkProp @()), testGroup "(,)" [ testProperty "(Integer, Integer)" $ ioProperty . concreteEvaluateSymOkProp @(Integer, Integer), let model = buildModel ("a" ::= True) eval :: Bool -> (SymBool, SymBool) -> (SymBool, SymBool) eval = flip evaluateSym model in testGroup "(SymBool, SymBool)" [ testCase "No fill default" $ eval False (ssym "a", ssym "b") @?= (con True, ssym "b"), testCase "Fill default" $ eval True (ssym "a", ssym "b") @?= (con True, con False) ] ], testGroup "(,,)" [ testProperty "(Integer, Integer, Integer)" $ ioProperty . concreteEvaluateSymOkProp @(Integer, Integer, Integer), let model = buildModel ("a" ::= True) eval :: Bool -> (SymBool, SymBool, SymBool) -> (SymBool, SymBool, SymBool) eval = flip evaluateSym model in testGroup "(SymBool, SymBool, SymBool)" [ testCase "No fill default" $ eval False (ssym "a", ssym "b", ssym "c") @?= (con True, ssym "b", ssym "c"), testCase "Fill default" $ eval True (ssym "a", ssym "b", ssym "c") @?= (con True, con False, con False) ] ], testGroup "(,,,)" [ testProperty "(Integer, Integer, Integer, Integer)" $ ioProperty . concreteEvaluateSymOkProp @(Integer, Integer, Integer, Integer), let model = buildModel ("a" ::= True) eval :: Bool -> (SymBool, SymBool, SymBool, SymBool) -> (SymBool, SymBool, SymBool, SymBool) eval = flip evaluateSym model in testGroup "(SymBool, SymBool, SymBool, SymBool)" [ testCase "No fill default" $ eval False (ssym "a", ssym "b", ssym "c", ssym "d") @?= (con True, ssym "b", ssym "c", ssym "d"), testCase "Fill default" $ eval True (ssym "a", ssym "b", ssym "c", ssym "d") @?= (con True, con False, con False, con False) ] ], testGroup "(,,,,)" [ testProperty "(Integer, Integer, Integer, Integer, Integer)" $ ioProperty . concreteEvaluateSymOkProp @(Integer, Integer, Integer, Integer, Integer), let model = buildModel ("a" ::= True) eval :: Bool -> (SymBool, SymBool, SymBool, SymBool, SymBool) -> (SymBool, SymBool, SymBool, SymBool, SymBool) eval = flip evaluateSym model in testGroup "(SymBool, SymBool, SymBool, SymBool, SymBool)" [ testCase "No fill default" $ eval False (ssym "a", ssym "b", ssym "c", ssym "d", ssym "e") @?= ( con True, ssym "b", ssym "c", ssym "d", ssym "e" ), testCase "Fill default" $ eval True (ssym "a", ssym "b", ssym "c", ssym "d", ssym "e") @?= ( con True, con False, con False, con False, con False ) ] ], testGroup "(,,,,,)" [ testProperty "(Integer, Integer, Integer, Integer, Integer, Integer)" $ ioProperty . concreteEvaluateSymOkProp @(Integer, Integer, Integer, Integer, Integer, Integer), let model = buildModel ("a" ::= True) eval :: Bool -> (SymBool, SymBool, SymBool, SymBool, SymBool, SymBool) -> (SymBool, SymBool, SymBool, SymBool, SymBool, SymBool) eval = flip evaluateSym model in testGroup "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)" [ testCase "No fill default" $ eval False ( ssym "a", ssym "b", ssym "c", ssym "d", ssym "e", ssym "f" ) @?= ( con True, ssym "b", ssym "c", ssym "d", ssym "e", ssym "f" ), testCase "Fill default" $ eval True ( ssym "a", ssym "b", ssym "c", ssym "d", ssym "e", ssym "f" ) @?= ( con True, con False, con False, con False, con False, con False ) ] ], testGroup "(,,,,,,)" [ testProperty "(Integer, Integer, Integer, Integer, Integer, Integer, Integer)" $ ioProperty . concreteEvaluateSymOkProp @( Integer, Integer, Integer, Integer, Integer, Integer, Integer ), let model = buildModel ("a" ::= True) eval :: Bool -> ( SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool ) -> ( SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool ) eval = flip evaluateSym model in testGroup "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)" [ testCase "No fill default" $ eval False ( ssym "a", ssym "b", ssym "c", ssym "d", ssym "e", ssym "f", ssym "g" ) @?= ( con True, ssym "b", ssym "c", ssym "d", ssym "e", ssym "f", ssym "g" ), testCase "Fill default" $ eval True ( ssym "a", ssym "b", ssym "c", ssym "d", ssym "e", ssym "f", ssym "h" ) @?= ( con True, con False, con False, con False, con False, con False, con False ) ] ], testGroup "(,,,,,,,)" [ testProperty "(Integer, Integer, Integer, Integer, Integer, Integer, Integer, Integer)" $ ioProperty . concreteEvaluateSymOkProp @( Integer, Integer, Integer, Integer, Integer, Integer, Integer, Integer ), let model = buildModel ("a" ::= True) eval :: Bool -> ( SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool ) -> ( SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool ) eval = flip evaluateSym model in testGroup "(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)" [ testCase "No fill default" $ eval False ( ssym "a", ssym "b", ssym "c", ssym "d", ssym "e", ssym "f", ssym "g", ssym "h" ) @?= ( con True, ssym "b", ssym "c", ssym "d", ssym "e", ssym "f", ssym "g", ssym "h" ), testCase "Fill default" $ eval True ( ssym "a", ssym "b", ssym "c", ssym "d", ssym "e", ssym "f", ssym "h", ssym "h" ) @?= ( con True, con False, con False, con False, con False, con False, con False, con False ) ] ], let model = buildModel ("a" ::= True) eval :: Bool -> B.ByteString -> B.ByteString eval = flip evaluateSym model in testGroup "ByteString should work" [ testGroup "No fill default" [ testCase "\"\"" $ eval False ("" :: B.ByteString) @?= "", testCase "\"a\"" $ eval False ("a" :: B.ByteString) @?= "a" ], testGroup "Fill default" [ testCase "\"\"" $ eval True ("" :: B.ByteString) @?= "", testCase "\"a\"" $ eval True ("a" :: B.ByteString) @?= "a" ] ], testGroup "Sum" [ testProperty "Sum Maybe Maybe Integer" ( ioProperty . \(x :: Either (Maybe Integer) (Maybe Integer)) -> case x of Left val -> concreteEvaluateSymOkProp @(Sum Maybe Maybe Integer) $ InL val Right val -> concreteEvaluateSymOkProp @(Sum Maybe Maybe Integer) $ InR val ), let model = buildModel ("a" ::= True) eval :: Bool -> Sum Maybe Maybe SymBool -> Sum Maybe Maybe SymBool eval = flip evaluateSym model in testGroup "Sum Maybe Maybe SymBool" [ testGroup "No fill default" [ testCase "InL Nothing" $ eval False (InL Nothing) @?= InL Nothing, testCase "InR Nothing" $ eval False (InR Nothing) @?= InR Nothing, testCase "InL (Just v): v in model" $ eval False (InL (Just $ ssym "a")) @?= InL (Just $ con True), testCase "InL (Just v): v not in model" $ eval False (InL (Just $ ssym "b")) @?= InL (Just $ ssym "b"), testCase "InR (Just v): v in model" $ eval False (InR (Just $ ssym "a")) @?= InR (Just $ con True), testCase "InR (Just v): v not in model" $ eval False (InR (Just $ ssym "b")) @?= InR (Just $ ssym "b") ], testGroup "Fill default" [ testCase "InL Nothing" $ eval True (InL Nothing) @?= InL Nothing, testCase "InR Nothing" $ eval True (InR Nothing) @?= InR Nothing, testCase "InL (Just v): v in model" $ eval True (InL (Just $ ssym "a")) @?= InL (Just $ con True), testCase "InL (Just v): v not in model" $ eval True (InL (Just $ ssym "b")) @?= InL (Just $ con False), testCase "InR (Just v): v in model" $ eval True (InR (Just $ ssym "a")) @?= InR (Just $ con True), testCase "InR (Just v): v not in model" $ eval True (InR (Just $ ssym "b")) @?= InR (Just $ con False) ] ] ], testGroup "WriterT" [ testGroup "Lazy" [ testProperty "WriterT Integer (Either Integer) Integer" $ ioProperty . \(x :: Either Integer (Integer, Integer)) -> concreteEvaluateSymOkProp (WriterLazy.WriterT x), let model = buildModel ("a" ::= True) eval :: Bool -> WriterLazy.WriterT SymBool (Either SymBool) SymBool -> WriterLazy.WriterT SymBool (Either SymBool) SymBool eval = flip evaluateSym model in testGroup "WriterT SymBool (Either SymBool) SymBool" [ testGroup "No fill default" [ testCase "WriterT (Left v): v in model" $ eval False (WriterLazy.WriterT $ Left $ ssym "a") @?= WriterLazy.WriterT (Left $ con True), testCase "WriterT (Left v): v not in model" $ eval False (WriterLazy.WriterT $ Left $ ssym "b") @?= WriterLazy.WriterT (Left $ ssym "b"), testCase "WriterT (Right (v1, v2))" $ eval False ( WriterLazy.WriterT $ Right (ssym "a", ssym "b") ) @?= WriterLazy.WriterT (Right (con True, ssym "b")) ], testGroup "Fill default" [ testCase "WriterT (Left v): v in model" $ eval True (WriterLazy.WriterT $ Left $ ssym "a") @?= WriterLazy.WriterT (Left $ con True), testCase "WriterT (Left v): v not in model" $ eval True (WriterLazy.WriterT $ Left $ ssym "b") @?= WriterLazy.WriterT (Left $ con False), testCase "WriterT (Right (v1, v2))" $ eval True ( WriterLazy.WriterT $ Right (ssym "a", ssym "b") ) @?= WriterLazy.WriterT (Right (con True, con False)) ] ] ], testGroup "Strict" [ testProperty "WriterT Integer (Either Integer) Integer" $ ioProperty . \(x :: Either Integer (Integer, Integer)) -> concreteEvaluateSymOkProp (WriterStrict.WriterT x), let model = buildModel ("a" ::= True) eval :: Bool -> WriterStrict.WriterT SymBool (Either SymBool) SymBool -> WriterStrict.WriterT SymBool (Either SymBool) SymBool eval = flip evaluateSym model in testGroup "WriterT SymBool (Either SymBool) SymBool" [ testGroup "No fill default" [ testCase "WriterT (Left v): v in model" $ eval False (WriterStrict.WriterT $ Left $ ssym "a") @?= WriterStrict.WriterT (Left $ con True), testCase "WriterT (Left v): v not in model" $ eval False (WriterStrict.WriterT $ Left $ ssym "b") @?= WriterStrict.WriterT (Left $ ssym "b"), testCase "WriterT (Right (v1, v2))" $ eval False ( WriterStrict.WriterT $ Right (ssym "a", ssym "b") ) @?= WriterStrict.WriterT (Right (con True, ssym "b")) ], testGroup "Fill default" [ testCase "WriterT (Left v): v in model" $ eval True (WriterStrict.WriterT $ Left $ ssym "a") @?= WriterStrict.WriterT (Left $ con True), testCase "WriterT (Left v): v not in model" $ eval True (WriterStrict.WriterT $ Left $ ssym "b") @?= WriterStrict.WriterT (Left $ con False), testCase "WriterT (Right (v1, v2))" $ eval True ( WriterStrict.WriterT $ Right (ssym "a", ssym "b") ) @?= WriterStrict.WriterT (Right (con True, con False)) ] ] ] ], testGroup "Identity" [ testProperty "Identity Integer" $ ioProperty . \(x :: Integer) -> concreteEvaluateSymOkProp $ Identity x, let model = buildModel ("a" ::= True) eval :: Bool -> Identity SymBool -> Identity SymBool eval = flip evaluateSym model in testGroup "Identity SymBool" [ testGroup "No fill default" [ testCase "Identity v: v in model" $ eval False (Identity $ ssym "a") @?= Identity (con True), testCase "Identity v: v not in model" $ eval False (Identity $ ssym "b") @?= Identity (ssym "b") ], testGroup "Fill default" [ testCase "Identity v: v in model" $ eval True (Identity $ ssym "a") @?= Identity (con True), testCase "Identity v: v not in model" $ eval True (Identity $ ssym "b") @?= Identity (con False) ] ] ], testGroup "IdentityT" [ testProperty "IdentityT (Either Integer) Integer" $ ioProperty . \(x :: Either Integer Integer) -> concreteEvaluateSymOkProp $ IdentityT x, let model = buildModel ("a" ::= True) eval :: Bool -> IdentityT (Either SymBool) SymBool -> IdentityT (Either SymBool) SymBool eval = flip evaluateSym model in testGroup "IdentityT (Either SymBool) SymBool" [ testGroup "No fill default" [ testCase "IdentityT (Left v): v in model" $ eval False (IdentityT $ Left $ ssym "a") @?= IdentityT (Left $ con True), testCase "IdentityT (Left v): v not in model" $ eval False (IdentityT $ Left $ ssym "b") @?= IdentityT (Left $ ssym "b"), testCase "IdentityT (Right v): v in model" $ eval False (IdentityT $ Right $ ssym "a") @?= IdentityT (Right $ con True), testCase "IdentityT (Right v): v not in model" $ eval False (IdentityT $ Right $ ssym "b") @?= IdentityT (Right $ ssym "b") ], testGroup "Fill default" [ testCase "IdentityT (Left v): v in model" $ eval True (IdentityT $ Left $ ssym "a") @?= IdentityT (Left $ con True), testCase "IdentityT (Left v): v not in model" $ eval True (IdentityT $ Left $ ssym "b") @?= IdentityT (Left $ con False), testCase "IdentityT (Right v): v in model" $ eval True (IdentityT $ Right $ ssym "a") @?= IdentityT (Right $ con True), testCase "IdentityT (Right v): v not in model" $ eval True (IdentityT $ Right $ ssym "b") @?= IdentityT (Right $ con False) ] ] ] ] ]