grisette-0.4.0.0: test/Grisette/Core/Data/Class/SubstituteSymTests.hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Grisette.Core.Data.Class.SubstituteSymTests (substituteSymTests) 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.Core.Data.Class.LogicalOp (LogicalOp ((.||)))
import Grisette.Core.Data.Class.SubstituteSym (SubstituteSym (substituteSym))
import Grisette.Core.Data.Class.TestValues (ssymBool, ssymbolBool)
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)
concreteSubstituteSymOkProp ::
(HasCallStack, SubstituteSym a, Show a, Eq a) => a -> Assertion
concreteSubstituteSymOkProp x =
substituteSym (ssymbolBool "a") (ssymBool "b") x @?= x
substituteSymTests :: Test
substituteSymTests =
testGroup
"SubstituteSym"
[ testGroup
"SubstituteSym for common types"
[ testCase "SymBool" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
let subst = substituteSym asym b
subst a @?= b
subst c @?= c
subst (a .|| c) @?= b .|| c,
testProperty "Bool" $ ioProperty . concreteSubstituteSymOkProp @Bool,
testProperty "Integer" $
ioProperty . concreteSubstituteSymOkProp @Integer,
testProperty "Char" $ ioProperty . concreteSubstituteSymOkProp @Char,
testProperty "Int" $ ioProperty . concreteSubstituteSymOkProp @Int,
testProperty "Int8" $ ioProperty . concreteSubstituteSymOkProp @Int8,
testProperty "Int16" $
ioProperty . concreteSubstituteSymOkProp @Int16,
testProperty "Int32" $
ioProperty . concreteSubstituteSymOkProp @Int32,
testProperty "Int64" $
ioProperty . concreteSubstituteSymOkProp @Int64,
testProperty "Word" $ ioProperty . concreteSubstituteSymOkProp @Word,
testProperty "Word8" $
ioProperty . concreteSubstituteSymOkProp @Word8,
testProperty "Word16" $
ioProperty . concreteSubstituteSymOkProp @Word16,
testProperty "Word32" $
ioProperty . concreteSubstituteSymOkProp @Word32,
testProperty "Word64" $
ioProperty . concreteSubstituteSymOkProp @Word64,
testGroup
"List"
[ testProperty "[Integer]" $
ioProperty . concreteSubstituteSymOkProp @[Integer],
testCase "[SymBool]" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
let subst = substituteSym asym b
subst [a, c] @?= [b, c]
],
testGroup
"Maybe"
[ testProperty "Maybe Integer" $
ioProperty . concreteSubstituteSymOkProp @(Maybe Integer),
testCase "Maybe SymBool" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
let subst :: Maybe SymBool -> Maybe SymBool
subst = substituteSym asym b
subst (Just a) @?= Just b
subst (Just c) @?= Just c
subst Nothing @?= Nothing
],
testGroup
"Either"
[ testProperty "Either Integer Integer" $
ioProperty
. concreteSubstituteSymOkProp @(Either Integer Integer),
testCase "Either SymBool SymBool" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
let subst :: Either SymBool SymBool -> Either SymBool SymBool
subst = substituteSym asym b
subst (Left a) @?= Left b
subst (Left c) @?= Left c
subst (Right a) @?= Right b
subst (Right c) @?= Right c
],
testGroup
"MaybeT"
[ testProperty "MaybeT Maybe Integer" $
ioProperty
. concreteSubstituteSymOkProp @(MaybeT Maybe Integer)
. MaybeT,
testCase "MaybeT Maybe SymBool" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
let subst :: MaybeT Maybe SymBool -> MaybeT Maybe SymBool
subst = substituteSym asym b
subst (MaybeT Nothing) @?= MaybeT Nothing
subst (MaybeT (Just Nothing)) @?= MaybeT (Just Nothing)
subst (MaybeT (Just (Just a))) @?= MaybeT (Just (Just b))
subst (MaybeT (Just (Just c))) @?= MaybeT (Just (Just c))
],
testGroup
"ExceptT"
[ testProperty "ExceptT Maybe Integer" $
ioProperty
. concreteSubstituteSymOkProp @(ExceptT Integer Maybe Integer)
. ExceptT,
testCase "ExceptT SymBool Maybe SymBool" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
let subst ::
ExceptT SymBool Maybe SymBool ->
ExceptT SymBool Maybe SymBool
subst = substituteSym asym b
subst (ExceptT Nothing) @?= ExceptT Nothing
subst (ExceptT $ Just $ Left a) @?= ExceptT (Just $ Left b)
subst (ExceptT $ Just $ Left c) @?= ExceptT (Just $ Left c)
subst (ExceptT $ Just $ Right a) @?= ExceptT (Just $ Right b)
subst (ExceptT $ Just $ Right c) @?= ExceptT (Just $ Right c)
],
testProperty "()" (ioProperty . concreteSubstituteSymOkProp @()),
testGroup
"(,)"
[ testProperty "(Integer, Integer)" $
ioProperty . concreteSubstituteSymOkProp @(Integer, Integer),
testCase "(SymBool, SymBool)" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
substituteSym asym b (a, c) @?= (b, c)
],
testGroup
"(,,)"
[ testProperty "(Integer, Integer, Integer)" $
ioProperty
. concreteSubstituteSymOkProp @(Integer, Integer, Integer),
testCase "(SymBool, SymBool, SymBool)" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
substituteSym asym b (a, c, a) @?= (b, c, b)
],
testGroup
"(,,,)"
[ testProperty "(Integer, Integer, Integer, Integer)" $
ioProperty
. concreteSubstituteSymOkProp
@(Integer, Integer, Integer, Integer),
testCase "(SymBool, SymBool, SymBool, SymBool)" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
substituteSym asym b (a, c, a, c) @?= (b, c, b, c)
],
testGroup
"(,,,,)"
[ testProperty "(Integer, Integer, Integer, Integer, Integer)" $
ioProperty
. concreteSubstituteSymOkProp
@(Integer, Integer, Integer, Integer, Integer),
testCase "(SymBool, SymBool, SymBool, SymBool, SymBool)" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
substituteSym asym b (a, c, a, c, a) @?= (b, c, b, c, b)
],
testGroup
"(,,,,,)"
[ testProperty
"(Integer, Integer, Integer, Integer, Integer, Integer)"
$ ioProperty
. concreteSubstituteSymOkProp
@(Integer, Integer, Integer, Integer, Integer, Integer),
testCase
"(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
$ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
substituteSym asym b (a, c, a, c, a, c) @?= (b, c, b, c, b, c)
],
testGroup
"(,,,,,,)"
[ testProperty
"(Integer, Integer, Integer, Integer, Integer, Integer, Integer)"
$ ioProperty
. concreteSubstituteSymOkProp
@( Integer,
Integer,
Integer,
Integer,
Integer,
Integer,
Integer
),
testCase
"(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
$ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
substituteSym asym b (a, c, a, c, a, c, a)
@?= (b, c, b, c, b, c, b)
],
testGroup
"(,,,,,,,)"
[ testProperty
"(Integer, Integer, Integer, Integer, Integer, Integer, Integer, Integer)"
$ ioProperty
. concreteSubstituteSymOkProp
@( Integer,
Integer,
Integer,
Integer,
Integer,
Integer,
Integer,
Integer
),
testCase
"(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
$ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
substituteSym asym b (a, c, a, c, a, c, a, c)
@?= (b, c, b, c, b, c, b, c)
],
testProperty "ByteString" $
ioProperty
. concreteSubstituteSymOkProp @B.ByteString
. B.pack,
testGroup
"Sum"
[ testProperty
"Sum Maybe Maybe Integer"
( ioProperty
. concreteSubstituteSymOkProp @(Sum Maybe Maybe Integer)
. ( \case
Left x -> InL x
Right x -> InL x
)
),
testCase
"Sum Maybe Maybe SymBool"
( do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
let subst ::
Sum Maybe Maybe SymBool ->
Sum Maybe Maybe SymBool
subst = substituteSym asym b
subst (InL Nothing) @?= InL Nothing
subst (InL (Just a)) @?= InL (Just b)
subst (InL (Just c)) @?= InL (Just c)
subst (InR Nothing) @?= InR Nothing
subst (InR (Just a)) @?= InR (Just b)
subst (InR (Just c)) @?= InR (Just c)
)
],
testGroup
"WriterT"
[ testGroup
"Lazy"
[ testProperty
"WriterT Integer (Either Integer) Integer"
( ioProperty
. concreteSubstituteSymOkProp
@(WriterLazy.WriterT Integer (Either Integer) Integer)
. WriterLazy.WriterT
),
testCase "WriterT SymBool (Either SymBool) SymBool" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
let subst ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool ->
WriterLazy.WriterT SymBool (Either SymBool) SymBool
subst = substituteSym asym b
subst
(WriterLazy.WriterT (Left a))
@?= WriterLazy.WriterT (Left b)
subst
(WriterLazy.WriterT (Left c))
@?= WriterLazy.WriterT (Left c)
subst
(WriterLazy.WriterT (Right (a, a)))
@?= WriterLazy.WriterT (Right (b, b))
subst
(WriterLazy.WriterT (Right (c, c)))
@?= WriterLazy.WriterT (Right (c, c))
],
testGroup
"Strict"
[ testProperty
"WriterT Integer (Either Integer) Integer"
( ioProperty
. concreteSubstituteSymOkProp
@( WriterStrict.WriterT
Integer
(Either Integer)
Integer
)
. WriterStrict.WriterT
),
testCase "WriterT SymBool (Either SymBool) SymBool" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
let subst ::
WriterStrict.WriterT
SymBool
(Either SymBool)
SymBool ->
WriterStrict.WriterT
SymBool
(Either SymBool)
SymBool
subst = substituteSym asym b
subst
(WriterStrict.WriterT (Left a))
@?= WriterStrict.WriterT (Left b)
subst
(WriterStrict.WriterT (Left c))
@?= WriterStrict.WriterT (Left c)
subst
(WriterStrict.WriterT (Right (a, a)))
@?= WriterStrict.WriterT (Right (b, b))
subst
(WriterStrict.WriterT (Right (c, c)))
@?= WriterStrict.WriterT (Right (c, c))
]
],
testGroup
"Identity"
[ testProperty
"Identity Integer"
(ioProperty . concreteSubstituteSymOkProp @(Identity Integer)),
testCase "Identity SymBool" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
let subst :: Identity SymBool -> Identity SymBool
subst = substituteSym asym b
subst (Identity a) @?= Identity b
subst (Identity c) @?= Identity c
],
testGroup
"IdentityT"
[ testProperty
"IdentityT (Either Integer) Integer"
$ ioProperty
. concreteSubstituteSymOkProp
@(IdentityT (Either Integer) Integer)
. IdentityT,
testCase "IdentityT (Either SymBool) SymBool" $ do
let asym = ssymbolBool "a"
let a = ssymBool "a"
let b = ssymBool "b"
let c = ssymBool "c"
let subst ::
IdentityT (Either SymBool) SymBool ->
IdentityT (Either SymBool) SymBool
subst = substituteSym asym b
subst (IdentityT (Left a)) @?= IdentityT (Left b)
subst (IdentityT (Left c)) @?= IdentityT (Left c)
subst (IdentityT (Right a)) @?= IdentityT (Right b)
subst (IdentityT (Right c)) @?= IdentityT (Right c)
]
]
]