grisette-0.9.0.0: test/Grisette/SymPrim/Prim/BoolTests.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Grisette.SymPrim.Prim.BoolTests (boolTests) where
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Term
( PEvalNumTerm (pevalAddNumTerm),
SupportedPrim (pevalITETerm),
Term,
andTerm,
conTerm,
eqTerm,
notTerm,
orTerm,
pevalAndTerm,
pevalEqTerm,
pevalImplyTerm,
pevalNEqTerm,
pevalNotTerm,
pevalOrTerm,
pevalXorTerm,
ssymTerm,
)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.HUnit ((@?=))
boolTests :: Test
boolTests =
testGroup
"Bool"
[ testGroup
"Not"
[ testCase "On concrete" $ do
pevalNotTerm (conTerm True) @?= conTerm False
pevalNotTerm (conTerm True) @?= conTerm False,
testCase "On general symbolic" $ do
pevalNotTerm (ssymTerm "a") @?= notTerm (ssymTerm "a" :: Term Bool),
testCase "On Not" $ do
pevalNotTerm (pevalNotTerm (ssymTerm "a")) @?= ssymTerm "a",
testCase "On Or Not" $ do
pevalNotTerm (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"))
@?= pevalAndTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "b"))
pevalNotTerm (pevalOrTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "b")))
@?= pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"),
testCase "On And Not" $ do
pevalNotTerm (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"))
@?= pevalOrTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "b"))
pevalNotTerm (pevalAndTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "b")))
@?= pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
],
testGroup
"Eqv & NEqv"
[ testCase "Eqv on both concrete" $ do
pevalEqTerm (conTerm True) (conTerm True) @?= conTerm True
pevalEqTerm (conTerm True) (conTerm False) @?= conTerm False
pevalEqTerm (conTerm False) (conTerm True) @?= conTerm False
pevalEqTerm (conTerm False) (conTerm False) @?= conTerm True
pevalEqTerm (conTerm (1 :: Integer)) (conTerm 1) @?= conTerm True
pevalEqTerm (conTerm (1 :: Integer)) (conTerm 2) @?= conTerm False
pevalEqTerm (conTerm (1 :: IntN 4)) (conTerm 1) @?= conTerm True
pevalEqTerm (conTerm (1 :: IntN 4)) (conTerm 2) @?= conTerm False
pevalEqTerm (conTerm (1 :: WordN 4)) (conTerm 1) @?= conTerm True
pevalEqTerm (conTerm (1 :: WordN 4)) (conTerm 2) @?= conTerm False,
testCase "Eqv on single concrete always put concrete ones in the right" $ do
pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
@?= eqTerm (ssymTerm "a" :: Term Integer) (conTerm 1 :: Term Integer)
pevalEqTerm (conTerm 1) (ssymTerm "a" :: Term Integer)
@?= eqTerm (ssymTerm "a" :: Term Integer) (conTerm 1 :: Term Integer),
testCase "Eqv on general symbolic" $ do
pevalEqTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
@?= eqTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b" :: Term Integer),
testCase "Eqv on Bool with single concrete" $ do
pevalEqTerm (conTerm True) (ssymTerm "a") @?= ssymTerm "a"
pevalEqTerm (ssymTerm "a") (conTerm True) @?= ssymTerm "a"
pevalEqTerm (conTerm False) (ssymTerm "a") @?= pevalNotTerm (ssymTerm "a")
pevalEqTerm (ssymTerm "a") (conTerm False) @?= pevalNotTerm (ssymTerm "a"),
testCase "NEqv on general symbolic" $ do
pevalNEqTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
@?= pevalNotTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")),
testCase "Eqv(Not(x), x) / Eqv(x, Not(x))" $ do
pevalEqTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "a") @?= conTerm False
pevalEqTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "a")) @?= conTerm False,
testCase "Eqv(n1+x, n2)" $ do
pevalEqTerm (pevalAddNumTerm (conTerm 1 :: Term Integer) (ssymTerm "a")) (conTerm 3)
@?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term Integer)
pevalEqTerm (pevalAddNumTerm (conTerm 1 :: Term (IntN 4)) (ssymTerm "a")) (conTerm 3)
@?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term (IntN 4))
pevalEqTerm (pevalAddNumTerm (conTerm 1 :: Term (WordN 4)) (ssymTerm "a")) (conTerm 3)
@?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term (WordN 4)),
testCase "Eqv(n1, n2+x)" $ do
pevalEqTerm (conTerm 3) (pevalAddNumTerm (conTerm 1 :: Term Integer) (ssymTerm "a"))
@?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term Integer)
pevalEqTerm (conTerm 3) (pevalAddNumTerm (conTerm 1 :: Term (IntN 4)) (ssymTerm "a"))
@?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term (IntN 4))
pevalEqTerm (conTerm 3) (pevalAddNumTerm (conTerm 1 :: Term (WordN 4)) (ssymTerm "a"))
@?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term (WordN 4)),
testCase "Eqv(l, ITE(c, l, f)) / Eqv(l, ITE(c, t, l) / Eqv(ITE(c, r, f), r) / Eqv(ITE(c, t, r), r)" $ do
pevalEqTerm (ssymTerm "a" :: Term Integer) (pevalITETerm (ssymTerm "b") (ssymTerm "a") (ssymTerm "c"))
@?= pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a") (ssymTerm "c" :: Term Integer))
pevalEqTerm (ssymTerm "a" :: Term Integer) (pevalITETerm (ssymTerm "b") (ssymTerm "c") (ssymTerm "a"))
@?= pevalOrTerm (pevalNotTerm $ ssymTerm "b") (pevalEqTerm (ssymTerm "a") (ssymTerm "c" :: Term Integer))
pevalEqTerm (pevalITETerm (ssymTerm "b") (ssymTerm "a") (ssymTerm "c")) (ssymTerm "a" :: Term Integer)
@?= pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "c") (ssymTerm "a" :: Term Integer))
pevalEqTerm (pevalITETerm (ssymTerm "b") (ssymTerm "c") (ssymTerm "a")) (ssymTerm "a" :: Term Integer)
@?= pevalOrTerm (pevalNotTerm $ ssymTerm "b") (pevalEqTerm (ssymTerm "c") (ssymTerm "a" :: Term Integer))
],
testGroup
"Or"
[ testCase "On both concrete" $ do
pevalOrTerm (conTerm True) (conTerm True) @?= conTerm True
pevalOrTerm (conTerm True) (conTerm False) @?= conTerm True
pevalOrTerm (conTerm False) (conTerm True) @?= conTerm True
pevalOrTerm (conTerm False) (conTerm False) @?= conTerm False,
testCase "On general symbolic" $ do
pevalOrTerm (ssymTerm "a") (ssymTerm "b")
@?= orTerm (ssymTerm "a" :: Term Bool) (ssymTerm "b" :: Term Bool),
testCase "Or(x, y) -> True" $ do
pevalOrTerm (conTerm True) (ssymTerm "b") @?= conTerm True
pevalOrTerm (ssymTerm "a") (conTerm True) @?= conTerm True
pevalOrTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@?= conTerm True
pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "a") @?= conTerm True
pevalOrTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "a")) @?= conTerm True,
testCase "Or(x, y) -> x" $ do
pevalOrTerm (ssymTerm "a") (conTerm False) @?= ssymTerm "a"
pevalOrTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
pevalOrTerm (ssymTerm "a") (ssymTerm "a") @?= ssymTerm "a",
testCase "Or(x, y) -> y" $ do
pevalOrTerm (conTerm False) (ssymTerm "a") @?= ssymTerm "a"
pevalOrTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
testCase "Or(x, Or(y1, y2)) -> True" $ do
pevalOrTerm (pevalNotTerm (ssymTerm "a")) (pevalOrTerm (ssymTerm "a") (ssymTerm "b")) @?= conTerm True
pevalOrTerm (ssymTerm "a") (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")) @?= conTerm True
pevalOrTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@?= conTerm True
pevalOrTerm (pevalNotTerm (ssymTerm "a")) (pevalOrTerm (ssymTerm "b") (ssymTerm "a")) @?= conTerm True
pevalOrTerm (ssymTerm "a") (pevalOrTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a"))) @?= conTerm True
pevalOrTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@?= conTerm True,
testCase "Or(x, Or(y1, y2)) -> Or(x, y2)" $ do
pevalOrTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "Or(x, Or(y1, y2)) -> Or(x, y1)" $ do
pevalOrTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "Or(x, y@Or(y1, y2)) -> y" $ do
pevalOrTerm (ssymTerm "a") (pevalOrTerm (ssymTerm "a") (ssymTerm "b"))
@?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
pevalOrTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
@?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b")
pevalOrTerm (ssymTerm "a") (pevalOrTerm (ssymTerm "b") (ssymTerm "a"))
@?= pevalOrTerm (ssymTerm "b") (ssymTerm "a")
pevalOrTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
@?= pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "Or(Or(x1, x2), y) -> True" $ do
pevalOrTerm (pevalOrTerm (ssymTerm "a") (ssymTerm "b")) (pevalNotTerm (ssymTerm "a")) @?= conTerm True
pevalOrTerm (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")) (ssymTerm "a") @?= conTerm True
pevalOrTerm
(pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= conTerm True
pevalOrTerm (pevalOrTerm (ssymTerm "b") (ssymTerm "a")) (pevalNotTerm (ssymTerm "a")) @?= conTerm True
pevalOrTerm (pevalOrTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a"))) (ssymTerm "a") @?= conTerm True
pevalOrTerm
(pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= conTerm True,
testCase "Or(x@Or(x1, x2), y) -> x" $ do
pevalOrTerm (pevalOrTerm (ssymTerm "a") (ssymTerm "b")) (ssymTerm "a")
@?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
pevalOrTerm
(pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b")
pevalOrTerm (pevalOrTerm (ssymTerm "b") (ssymTerm "a")) (ssymTerm "a")
@?= pevalOrTerm (ssymTerm "b") (ssymTerm "a")
pevalOrTerm
(pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@?= pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "Or(Or(x1, x2), y) -> Or(x2, y)" $ do
pevalOrTerm
(pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "Or(Or(x1, x2), y) -> Or(x1, y)" $ do
pevalOrTerm
(pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "Or(x, And(y1, y2)) -> x" $ do
pevalOrTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
pevalOrTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
testCase "Or(x, And(y1, y2)) -> Or(x, y2)" $ do
pevalOrTerm (ssymTerm "a") (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"))
@?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
pevalOrTerm (pevalNotTerm (ssymTerm "a")) (pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
@?= pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
pevalOrTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "Or(And(x1, x2), y) -> y" $ do
pevalOrTerm
(pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
pevalOrTerm
(pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
testCase "Or(x, And(y1, y2)) -> Or(x, y1)" $ do
pevalOrTerm (ssymTerm "a") (pevalAndTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a")))
@?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
pevalOrTerm (pevalNotTerm (ssymTerm "a")) (pevalAndTerm (ssymTerm "b") (ssymTerm "a"))
@?= pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
pevalOrTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "Or(Not(x), Not(y)) -> Not(And(x, y))" $ do
pevalOrTerm (pevalNotTerm (ssymTerm "a")) (pevalNotTerm (ssymTerm "b"))
@?= pevalNotTerm (pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
],
testGroup
"And"
[ testCase "Oith both concrete" $ do
pevalAndTerm (conTerm True) (conTerm True) @?= conTerm True
pevalAndTerm (conTerm True) (conTerm False) @?= conTerm False
pevalAndTerm (conTerm False) (conTerm True) @?= conTerm False
pevalAndTerm (conTerm False) (conTerm False) @?= conTerm False,
testCase "On general symbolic" $ do
pevalAndTerm (ssymTerm "a") (ssymTerm "b")
@?= andTerm (ssymTerm "a" :: Term Bool) (ssymTerm "b" :: Term Bool),
testCase "And(x, y) -> False" $ do
pevalAndTerm (conTerm False) (ssymTerm "b") @?= conTerm False
pevalAndTerm (ssymTerm "a") (conTerm False) @?= conTerm False
pevalAndTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@?= conTerm False
pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "a") @?= conTerm False
pevalAndTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "a")) @?= conTerm False,
testCase "And(x, y) -> x" $ do
pevalAndTerm (ssymTerm "a") (conTerm True) @?= ssymTerm "a"
pevalAndTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
pevalAndTerm (ssymTerm "a") (ssymTerm "a") @?= ssymTerm "a",
testCase "And(x, y) -> y" $ do
pevalAndTerm (conTerm True) (ssymTerm "a") @?= ssymTerm "a"
pevalAndTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
testCase "And(x, And(y1, y2)) -> False" $ do
pevalAndTerm (pevalNotTerm (ssymTerm "a")) (pevalAndTerm (ssymTerm "a") (ssymTerm "b")) @?= conTerm False
pevalAndTerm (ssymTerm "a") (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")) @?= conTerm False
pevalAndTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@?= conTerm False
pevalAndTerm (pevalNotTerm (ssymTerm "a")) (pevalAndTerm (ssymTerm "b") (ssymTerm "a")) @?= conTerm False
pevalAndTerm (ssymTerm "a") (pevalAndTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a"))) @?= conTerm False
pevalAndTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@?= conTerm False,
testCase "And(x, And(y1, y2)) -> And(x, y2)" $ do
pevalAndTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "And(x, And(y1, y2)) -> And(x, y1)" $ do
pevalAndTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "And(x, y@And(y1, y2)) -> y" $ do
pevalAndTerm (ssymTerm "a") (pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
@?= pevalAndTerm (ssymTerm "a") (ssymTerm "b")
pevalAndTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
@?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b")
pevalAndTerm (ssymTerm "a") (pevalAndTerm (ssymTerm "b") (ssymTerm "a"))
@?= pevalAndTerm (ssymTerm "b") (ssymTerm "a")
pevalAndTerm
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
@?= pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "And(And(x1, x2), y) -> False" $ do
pevalAndTerm (pevalAndTerm (ssymTerm "a") (ssymTerm "b")) (pevalNotTerm (ssymTerm "a")) @?= conTerm False
pevalAndTerm (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")) (ssymTerm "a") @?= conTerm False
pevalAndTerm
(pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= conTerm False
pevalAndTerm (pevalAndTerm (ssymTerm "b") (ssymTerm "a")) (pevalNotTerm (ssymTerm "a")) @?= conTerm False
pevalAndTerm (pevalAndTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a"))) (ssymTerm "a") @?= conTerm False
pevalAndTerm
(pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= conTerm False,
testCase "And(x@And(x1, x2), y) -> x" $ do
pevalAndTerm (pevalAndTerm (ssymTerm "a") (ssymTerm "b")) (ssymTerm "a")
@?= pevalAndTerm (ssymTerm "a") (ssymTerm "b")
pevalAndTerm
(pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b")
pevalAndTerm (pevalAndTerm (ssymTerm "b") (ssymTerm "a")) (ssymTerm "a")
@?= pevalAndTerm (ssymTerm "b") (ssymTerm "a")
pevalAndTerm
(pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
(pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@?= pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "And(And(x1, x2), y) -> And(x2, y)" $ do
pevalAndTerm
(pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "And(And(x1, x2), y) -> And(x1, y)" $ do
pevalAndTerm
(pevalAndTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "And(x, Or(y1, y2)) -> x" $ do
pevalAndTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
pevalAndTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
testCase "And(x, Or(y1, y2)) -> And(x, y2)" $ do
pevalAndTerm (ssymTerm "a") (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"))
@?= pevalAndTerm (ssymTerm "a") (ssymTerm "b")
pevalAndTerm (pevalNotTerm (ssymTerm "a")) (pevalOrTerm (ssymTerm "a") (ssymTerm "b"))
@?= pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
pevalAndTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "And(Or(x1, x2), y) -> y" $ do
pevalAndTerm
(pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
pevalAndTerm
(pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
testCase "And(x, Or(y1, y2)) -> And(x, y1)" $ do
pevalAndTerm (ssymTerm "a") (pevalOrTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a")))
@?= pevalAndTerm (ssymTerm "a") (ssymTerm "b")
pevalAndTerm (pevalNotTerm (ssymTerm "a")) (pevalOrTerm (ssymTerm "b") (ssymTerm "a"))
@?= pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
pevalAndTerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "And(Not(x), Not(y)) -> Not(Or(x, y))" $ do
pevalAndTerm (pevalNotTerm (ssymTerm "a")) (pevalNotTerm (ssymTerm "b"))
@?= pevalNotTerm (pevalOrTerm (ssymTerm "a") (ssymTerm "b"))
],
testGroup
"ITE"
[ testCase "On concrete condition" $ do
pevalITETerm (conTerm True) (ssymTerm "a" :: Term Integer) (ssymTerm "b")
@?= ssymTerm "a"
pevalITETerm (conTerm False) (ssymTerm "a" :: Term Integer) (ssymTerm "b")
@?= ssymTerm "b",
testCase "On same branches" $ do
pevalITETerm (ssymTerm "c") (ssymTerm "a" :: Term Integer) (ssymTerm "a")
@?= ssymTerm "a",
testCase "On both not" $ do
pevalITETerm (ssymTerm "c") (pevalNotTerm $ ssymTerm "a") (pevalNotTerm $ ssymTerm "b")
@?= pevalNotTerm (pevalITETerm (ssymTerm "c") (ssymTerm "a") (ssymTerm "b")),
testCase "On not in condition" $ do
pevalITETerm (pevalNotTerm $ ssymTerm "c") (ssymTerm "a" :: Term Integer) (ssymTerm "b")
@?= pevalITETerm (ssymTerm "c") (ssymTerm "b") (ssymTerm "a"),
testCase "On all arguments as ITE with same conditions" $ do
pevalITETerm
(pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "c"))
(pevalITETerm (ssymTerm "a") (ssymTerm "d" :: Term Integer) (ssymTerm "e"))
(pevalITETerm (ssymTerm "a") (ssymTerm "f" :: Term Integer) (ssymTerm "g"))
@?= pevalITETerm
(ssymTerm "a")
(pevalITETerm (ssymTerm "b") (ssymTerm "d") (ssymTerm "f"))
(pevalITETerm (ssymTerm "c") (ssymTerm "e") (ssymTerm "g")),
testCase "On with true branch as ITE" $ do
pevalITETerm
(ssymTerm "a")
(pevalITETerm (ssymTerm "a") (ssymTerm "b" :: Term Integer) (ssymTerm "c"))
(ssymTerm "d")
@?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "d")
pevalITETerm
(ssymTerm "a")
(pevalITETerm (ssymTerm "b") (ssymTerm "c" :: Term Integer) (ssymTerm "d"))
(ssymTerm "c")
@?= pevalITETerm
(pevalOrTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"))
(ssymTerm "c")
(ssymTerm "d")
pevalITETerm
(ssymTerm "a")
(pevalITETerm (ssymTerm "b") (ssymTerm "c" :: Term Integer) (ssymTerm "d"))
(ssymTerm "d")
@?= pevalITETerm
(pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
(ssymTerm "c")
(ssymTerm "d"),
testCase "On false branch as ITE" $ do
pevalITETerm
(ssymTerm "a")
(ssymTerm "b")
(pevalITETerm (ssymTerm "a") (ssymTerm "c" :: Term Integer) (ssymTerm "d"))
@?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "d")
pevalITETerm
(ssymTerm "a")
(ssymTerm "b")
(pevalITETerm (ssymTerm "c") (ssymTerm "b" :: Term Integer) (ssymTerm "d"))
@?= pevalITETerm
(pevalOrTerm (ssymTerm "a") (ssymTerm "c"))
(ssymTerm "b")
(ssymTerm "d")
pevalITETerm
(ssymTerm "a")
(ssymTerm "b")
(pevalITETerm (ssymTerm "c") (ssymTerm "d" :: Term Integer) (ssymTerm "b"))
@?= pevalITETerm
(pevalOrTerm (ssymTerm "a") (pevalNotTerm $ ssymTerm "c"))
(ssymTerm "b")
(ssymTerm "d"),
testCase "On both And" $ do
pevalITETerm
(ssymTerm "a")
(pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
(pevalAndTerm (ssymTerm "b") (ssymTerm "d"))
@?= pevalAndTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
pevalITETerm
(ssymTerm "a")
(pevalAndTerm (ssymTerm "c") (ssymTerm "b"))
(pevalAndTerm (ssymTerm "b") (ssymTerm "d"))
@?= pevalAndTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
pevalITETerm
(ssymTerm "a")
(pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
(pevalAndTerm (ssymTerm "d") (ssymTerm "b"))
@?= pevalAndTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
pevalITETerm
(ssymTerm "a")
(pevalAndTerm (ssymTerm "c") (ssymTerm "b"))
(pevalAndTerm (ssymTerm "d") (ssymTerm "b"))
@?= pevalAndTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d")),
testCase "On left And" $ do
pevalITETerm
(ssymTerm "a")
(pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
(ssymTerm "b")
@?= pevalAndTerm (ssymTerm "b") (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "c"))
pevalITETerm
(ssymTerm "a")
(pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
(ssymTerm "c")
@?= pevalAndTerm (ssymTerm "c") (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"))
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(ssymTerm "c")
@?= pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"))
(ssymTerm "c")
@?= pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "c")
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(ssymTerm "c")
@?= pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalAndTerm (ssymTerm "b") (pevalNotTerm $ ssymTerm "a"))
(ssymTerm "c")
@?= pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "c")
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(ssymTerm "c")
@?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b") (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
(ssymTerm "c")
@?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "c")
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(ssymTerm "c")
@?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b") (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalAndTerm (ssymTerm "b") (ssymTerm "a"))
(ssymTerm "c")
@?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "c"),
testCase "On right And" $ do
pevalITETerm
(ssymTerm "a")
(ssymTerm "b")
(pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
@?= pevalAndTerm (ssymTerm "b") (pevalOrTerm (ssymTerm "a") (ssymTerm "c"))
pevalITETerm
(ssymTerm "a")
(ssymTerm "c")
(pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
@?= pevalAndTerm (ssymTerm "c") (pevalOrTerm (ssymTerm "a") (ssymTerm "b")),
testCase "On both Or" $ do
pevalITETerm
(ssymTerm "a")
(pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
(pevalOrTerm (ssymTerm "b") (ssymTerm "d"))
@?= pevalOrTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
pevalITETerm
(ssymTerm "a")
(pevalOrTerm (ssymTerm "c") (ssymTerm "b"))
(pevalOrTerm (ssymTerm "b") (ssymTerm "d"))
@?= pevalOrTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
pevalITETerm
(ssymTerm "a")
(pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
(pevalOrTerm (ssymTerm "d") (ssymTerm "b"))
@?= pevalOrTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
pevalITETerm
(ssymTerm "a")
(pevalOrTerm (ssymTerm "c") (ssymTerm "b"))
(pevalOrTerm (ssymTerm "d") (ssymTerm "b"))
@?= pevalOrTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d")),
testCase "On left Or" $ do
pevalITETerm
(ssymTerm "a")
(pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
(ssymTerm "b")
@?= pevalOrTerm (ssymTerm "b") (pevalAndTerm (ssymTerm "a") (ssymTerm "c"))
pevalITETerm
(ssymTerm "a")
(pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
(ssymTerm "c")
@?= pevalOrTerm (ssymTerm "c") (pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(ssymTerm "c")
@?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b") (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalOrTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"))
(ssymTerm "c")
@?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "c")
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(ssymTerm "c")
@?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b") (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalOrTerm (ssymTerm "b") (pevalNotTerm $ ssymTerm "a"))
(ssymTerm "c")
@?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "c")
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(ssymTerm "c")
@?= pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalOrTerm (ssymTerm "a") (ssymTerm "b"))
(ssymTerm "c")
@?= pevalOrTerm (ssymTerm "a") (ssymTerm "c")
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(ssymTerm "c")
@?= pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalOrTerm (ssymTerm "b") (ssymTerm "a"))
(ssymTerm "c")
@?= pevalOrTerm (ssymTerm "a") (ssymTerm "c"),
testCase "On right Or" $ do
pevalITETerm
(ssymTerm "a")
(ssymTerm "b")
(pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
@?= pevalOrTerm (ssymTerm "b") (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "c"))
pevalITETerm
(ssymTerm "a")
(ssymTerm "c")
(pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
@?= pevalOrTerm (ssymTerm "c") (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")),
testCase "On const boolean in branches" $ do
pevalITETerm
(ssymTerm "a")
(conTerm True)
(ssymTerm "b")
@?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
pevalITETerm
(ssymTerm "a")
(conTerm False)
(ssymTerm "b")
@?= pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b")
pevalITETerm
(ssymTerm "a")
(ssymTerm "b")
(conTerm True)
@?= pevalOrTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b")
pevalITETerm
(ssymTerm "a")
(ssymTerm "b")
(conTerm False)
@?= pevalAndTerm (ssymTerm "a") (ssymTerm "b"),
testCase "On condition equal to some branch" $ do
pevalITETerm
(ssymTerm "a")
(ssymTerm "a")
(ssymTerm "b")
@?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
pevalITETerm
(ssymTerm "a")
(ssymTerm "b")
(ssymTerm "a")
@?= pevalAndTerm (ssymTerm "a") (ssymTerm "b"),
testCase "On left Not" $ do
pevalITETerm (ssymTerm "a") (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
@?= pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"),
testCase "On right Not" $ do
pevalITETerm (ssymTerm "a") (ssymTerm "b") (pevalNotTerm (ssymTerm "a"))
@?= pevalOrTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"),
testCase "On left Not And" $ do
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNotTerm (pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b")))
(ssymTerm "c")
@?= pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalNotTerm (pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b")))
(ssymTerm "c")
@?= pevalOrTerm (ssymTerm "a") (ssymTerm "c")
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNotTerm (pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))))
(ssymTerm "c")
@?= pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalNotTerm (pevalAndTerm (ssymTerm "b") (pevalNotTerm $ ssymTerm "a")))
(ssymTerm "c")
@?= pevalOrTerm (ssymTerm "a") (ssymTerm "c")
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNotTerm (pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b")))
(ssymTerm "c")
@?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (pevalNotTerm $ ssymTerm "b") (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalNotTerm (pevalAndTerm (ssymTerm "a") (ssymTerm "b")))
(ssymTerm "c")
@?= pevalITETerm (ssymTerm "a") (pevalNotTerm $ ssymTerm "b") (ssymTerm "c")
pevalITETerm
(pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNotTerm (pevalAndTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))))
(ssymTerm "c")
@?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (pevalNotTerm $ ssymTerm "b") (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalNotTerm (pevalAndTerm (ssymTerm "b") (ssymTerm "a")))
(ssymTerm "c")
@?= pevalITETerm (ssymTerm "a") (pevalNotTerm $ ssymTerm "b") (ssymTerm "c")
],
testGroup
"Imply"
[ testCase "pevalImplyTerm" $ do
ssymTerm "a"
`pevalImplyTerm` ssymTerm "b"
@?= pevalOrTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b")
],
testGroup
"Xor"
[ testCase "pevalXorTerm" $ do
ssymTerm "a"
`pevalXorTerm` ssymTerm "b"
@?= pevalOrTerm
(pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"))
(pevalAndTerm (ssymTerm "a") (pevalNotTerm $ ssymTerm "b"))
]
]