grisette-0.13.0.1: test/Grisette/Core/Data/Class/EvalSymTests.hs
{-# 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)
]
]
]
]
]