{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Grisette.Core.Data.Class.EvalSymTests (evalSymTests) 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 ( AsKey (AsKey), EvalSym (evalSym), ITEOp (symIte), LogicalOp (symNot, (.&&), (.||)), ModelOps (emptyModel), ModelRep (buildModel), ModelValuePair ((::=)), Solvable (con, isym, ssym), SymBool, SymEq ((.==)), SymInteger, Symbol (IndexedSymbol), solve, typedAnySymbol, z3, ) import Test.Framework (Test, TestOptions' (topt_timeout), plusTestOptions, testGroup) import Test.Framework.Providers.HUnit (testCase) import Test.Framework.Providers.QuickCheck2 (testProperty) import Test.HUnit (Assertion, (@?=)) import Test.QuickCheck (ioProperty) concreteEvalSymOkProp :: (HasCallStack, EvalSym a, Show a, Eq a) => a -> Assertion concreteEvalSymOkProp x = evalSym True emptyModel x @?= x evalSymTests :: Test evalSymTests = testGroup "EvalSym" [ plusTestOptions (mempty {topt_timeout = Just (Just 1000000)}) $ testCase "proper memo" $ do let pair = ("a" :: AsKey SymInteger, "b" :: AsKey SymInteger) let iter (x, y) = (y, x + y) let r = iterate iter pair !! 100 Right m <- solve z3 $ snd r .== 0 evalSym True m (snd r) @?= 0, testGroup "EvalSym for common types" [ testGroup "SymBool" [ let model = emptyModel eval :: AsKey SymBool -> AsKey SymBool eval = evalSym 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 (AsKey $ (ssym "a" :: SymBool) .== ssym "b") @?= AsKey ((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 :: AsKey SymBool -> AsKey SymBool eval = evalSym 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 (AsKey $ (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, typedAnySymbol (IndexedSymbol "a" 1) ::= False, "b" ::= False, "c" ::= True ) eval :: AsKey SymBool -> AsKey SymBool eval = evalSym 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 (AsKey $ (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 . concreteEvalSymOkProp @Bool, testProperty "Integer" $ ioProperty . concreteEvalSymOkProp @Integer, testProperty "Char" $ ioProperty . concreteEvalSymOkProp @Char, testProperty "Int" $ ioProperty . concreteEvalSymOkProp @Int, testProperty "Int8" $ ioProperty . concreteEvalSymOkProp @Int8, testProperty "Int16" $ ioProperty . concreteEvalSymOkProp @Int16, testProperty "Int32" $ ioProperty . concreteEvalSymOkProp @Int32, testProperty "Int64" $ ioProperty . concreteEvalSymOkProp @Int64, testProperty "Word" $ ioProperty . concreteEvalSymOkProp @Word, testProperty "Word8" $ ioProperty . concreteEvalSymOkProp @Word8, testProperty "Word16" $ ioProperty . concreteEvalSymOkProp @Word16, testProperty "Word32" $ ioProperty . concreteEvalSymOkProp @Word32, testProperty "Word64" $ ioProperty . concreteEvalSymOkProp @Word64, testGroup "List" [ testProperty "[Integer]" $ ioProperty . concreteEvalSymOkProp @[Integer], let model = buildModel ("a" ::= True, "b" ::= False) eval :: Bool -> [AsKey SymBool] -> [AsKey SymBool] eval = flip evalSym 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 . concreteEvalSymOkProp @(Maybe Integer), let model = buildModel ("a" ::= True) eval :: Bool -> Maybe (AsKey SymBool) -> Maybe (AsKey SymBool) eval = flip evalSym 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 . concreteEvalSymOkProp @(Either Integer Integer), let model = buildModel ("a" ::= True) eval :: Bool -> Either (AsKey SymBool) (AsKey SymBool) -> Either (AsKey SymBool) (AsKey SymBool) eval = flip evalSym 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 . concreteEvalSymOkProp @(MaybeT Maybe Integer) . MaybeT, let model = buildModel ("a" ::= True) eval :: Bool -> MaybeT Maybe (AsKey SymBool) -> MaybeT Maybe (AsKey SymBool) eval = flip evalSym 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 . concreteEvalSymOkProp @(ExceptT Integer Maybe Integer) . ExceptT, let model = buildModel ("a" ::= True) eval :: Bool -> ExceptT (AsKey SymBool) Maybe (AsKey SymBool) -> ExceptT (AsKey SymBool) Maybe (AsKey SymBool) eval = flip evalSym 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 . concreteEvalSymOkProp @()), testGroup "(,)" [ testProperty "(Integer, Integer)" $ ioProperty . concreteEvalSymOkProp @(Integer, Integer), let model = buildModel ("a" ::= True) eval :: Bool -> (AsKey SymBool, AsKey SymBool) -> (AsKey SymBool, AsKey SymBool) eval = flip evalSym 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 . concreteEvalSymOkProp @(Integer, Integer, Integer), let model = buildModel ("a" ::= True) eval :: Bool -> (AsKey SymBool, AsKey SymBool, AsKey SymBool) -> (AsKey SymBool, AsKey SymBool, AsKey SymBool) eval = flip evalSym 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 . concreteEvalSymOkProp @(Integer, Integer, Integer, Integer), let model = buildModel ("a" ::= True) eval :: Bool -> (AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool) -> (AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool) eval = flip evalSym 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 . concreteEvalSymOkProp @(Integer, Integer, Integer, Integer, Integer), let model = buildModel ("a" ::= True) eval :: Bool -> ( AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool ) -> ( AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool ) eval = flip evalSym 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 . concreteEvalSymOkProp @(Integer, Integer, Integer, Integer, Integer, Integer), let model = buildModel ("a" ::= True) eval :: Bool -> ( AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool ) -> ( AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool ) eval = flip evalSym 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 . concreteEvalSymOkProp @( Integer, Integer, Integer, Integer, Integer, Integer, Integer ), let model = buildModel ("a" ::= True) eval :: Bool -> ( AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool ) -> ( AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool ) eval = flip evalSym 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 . concreteEvalSymOkProp @( Integer, Integer, Integer, Integer, Integer, Integer, Integer, Integer ), let model = buildModel ("a" ::= True) eval :: Bool -> ( AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool ) -> ( AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool, AsKey SymBool ) eval = flip evalSym 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 evalSym 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 -> concreteEvalSymOkProp @(Sum Maybe Maybe Integer) $ InL val Right val -> concreteEvalSymOkProp @(Sum Maybe Maybe Integer) $ InR val ), let model = buildModel ("a" ::= True) eval :: Bool -> Sum Maybe Maybe (AsKey SymBool) -> Sum Maybe Maybe (AsKey SymBool) eval = flip evalSym 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)) -> concreteEvalSymOkProp (WriterLazy.WriterT x), let model = buildModel ("a" ::= True) eval :: Bool -> WriterLazy.WriterT (AsKey SymBool) (Either (AsKey SymBool)) (AsKey SymBool) -> WriterLazy.WriterT (AsKey SymBool) (Either (AsKey SymBool)) (AsKey SymBool) eval = flip evalSym 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)) -> concreteEvalSymOkProp (WriterStrict.WriterT x), let model = buildModel ("a" ::= True) eval :: Bool -> WriterStrict.WriterT (AsKey SymBool) (Either (AsKey SymBool)) (AsKey SymBool) -> WriterStrict.WriterT (AsKey SymBool) (Either (AsKey SymBool)) (AsKey SymBool) eval = flip evalSym 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) -> concreteEvalSymOkProp $ Identity x, let model = buildModel ("a" ::= True) eval :: Bool -> Identity (AsKey SymBool) -> Identity (AsKey SymBool) eval = flip evalSym 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) -> concreteEvalSymOkProp $ IdentityT x, let model = buildModel ("a" ::= True) eval :: Bool -> IdentityT (Either (AsKey SymBool)) (AsKey SymBool) -> IdentityT (Either (AsKey SymBool)) (AsKey SymBool) eval = flip evalSym 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) ] ] ] ] ]