grisette-0.2.0.0: test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Grisette.IR.SymPrim.Data.Prim.BoolTests where
import Grisette.Core.Data.BV
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
import Test.Tasty
import Test.Tasty.HUnit
boolTests :: TestTree
boolTests =
testGroup
"BoolTests"
[ 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
pevalEqvTerm (conTerm True) (conTerm True) @=? conTerm True
pevalEqvTerm (conTerm True) (conTerm False) @=? conTerm False
pevalEqvTerm (conTerm False) (conTerm True) @=? conTerm False
pevalEqvTerm (conTerm False) (conTerm False) @=? conTerm True
pevalEqvTerm (conTerm (1 :: Integer)) (conTerm 1) @=? conTerm True
pevalEqvTerm (conTerm (1 :: Integer)) (conTerm 2) @=? conTerm False
pevalEqvTerm (conTerm (1 :: IntN 4)) (conTerm 1) @=? conTerm True
pevalEqvTerm (conTerm (1 :: IntN 4)) (conTerm 2) @=? conTerm False
pevalEqvTerm (conTerm (1 :: WordN 4)) (conTerm 1) @=? conTerm True
pevalEqvTerm (conTerm (1 :: WordN 4)) (conTerm 2) @=? conTerm False,
testCase "Eqv on single concrete always put concrete ones in the right" $ do
pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
@=? eqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1 :: Term Integer)
pevalEqvTerm (conTerm 1) (ssymTerm "a" :: Term Integer)
@=? eqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1 :: Term Integer),
testCase "Eqv on general symbolic" $ do
pevalEqvTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
@=? eqvTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b" :: Term Integer),
testCase "Eqv on Bool with single concrete" $ do
pevalEqvTerm (conTerm True) (ssymTerm "a") @=? ssymTerm "a"
pevalEqvTerm (ssymTerm "a") (conTerm True) @=? ssymTerm "a"
pevalEqvTerm (conTerm False) (ssymTerm "a") @=? pevalNotTerm (ssymTerm "a")
pevalEqvTerm (ssymTerm "a") (conTerm False) @=? pevalNotTerm (ssymTerm "a"),
testCase "NEqv on general symbolic" $ do
pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
@=? pevalNotTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")),
testCase "Eqv(Not(x), x) / Eqv(x, Not(x))" $ do
pevalEqvTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "a") @=? conTerm False
pevalEqvTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "a")) @=? conTerm False,
testCase "Eqv(n1+x, n2)" $ do
pevalEqvTerm (pevalAddNumTerm (conTerm 1 :: Term Integer) (ssymTerm "a")) (conTerm 3)
@=? pevalEqvTerm (ssymTerm "a") (conTerm 2 :: Term Integer)
pevalEqvTerm (pevalAddNumTerm (conTerm 1 :: Term (IntN 4)) (ssymTerm "a")) (conTerm 3)
@=? pevalEqvTerm (ssymTerm "a") (conTerm 2 :: Term (IntN 4))
pevalEqvTerm (pevalAddNumTerm (conTerm 1 :: Term (WordN 4)) (ssymTerm "a")) (conTerm 3)
@=? pevalEqvTerm (ssymTerm "a") (conTerm 2 :: Term (WordN 4)),
testCase "Eqv(n1, n2+x)" $ do
pevalEqvTerm (conTerm 3) (pevalAddNumTerm (conTerm 1 :: Term Integer) (ssymTerm "a"))
@=? pevalEqvTerm (ssymTerm "a") (conTerm 2 :: Term Integer)
pevalEqvTerm (conTerm 3) (pevalAddNumTerm (conTerm 1 :: Term (IntN 4)) (ssymTerm "a"))
@=? pevalEqvTerm (ssymTerm "a") (conTerm 2 :: Term (IntN 4))
pevalEqvTerm (conTerm 3) (pevalAddNumTerm (conTerm 1 :: Term (WordN 4)) (ssymTerm "a"))
@=? pevalEqvTerm (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
pevalEqvTerm (ssymTerm "a" :: Term Integer) (pevalITETerm (ssymTerm "b") (ssymTerm "a") (ssymTerm "c"))
@=? pevalOrTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a") (ssymTerm "c" :: Term Integer))
pevalEqvTerm (ssymTerm "a" :: Term Integer) (pevalITETerm (ssymTerm "b") (ssymTerm "c") (ssymTerm "a"))
@=? pevalOrTerm (pevalNotTerm $ ssymTerm "b") (pevalEqvTerm (ssymTerm "a") (ssymTerm "c" :: Term Integer))
pevalEqvTerm (pevalITETerm (ssymTerm "b") (ssymTerm "a") (ssymTerm "c")) (ssymTerm "a" :: Term Integer)
@=? pevalOrTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "c") (ssymTerm "a" :: Term Integer))
pevalEqvTerm (pevalITETerm (ssymTerm "b") (ssymTerm "c") (ssymTerm "a")) (ssymTerm "a" :: Term Integer)
@=? pevalOrTerm (pevalNotTerm $ ssymTerm "b") (pevalEqvTerm (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
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNotEqvTerm (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
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@=? pevalNotEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@=? pevalNotEqvTerm (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
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalNotEqvTerm (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
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@=? conTerm True,
testCase "Or(x, Or(y1, y2)) -> Or(x, y2)" $ do
pevalOrTerm
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@=? pevalOrTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "Or(x, Or(y1, y2)) -> Or(x, y1)" $ do
pevalOrTerm
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@=? pevalOrTerm (pevalNotEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalOrTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
@=? pevalOrTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b")
pevalOrTerm (ssymTerm "a") (pevalOrTerm (ssymTerm "b") (ssymTerm "a"))
@=? pevalOrTerm (ssymTerm "b") (ssymTerm "a")
pevalOrTerm
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalOrTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
@=? pevalOrTerm (ssymTerm "b") (pevalNotEqvTerm (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 (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalNotEqvTerm (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") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalNotEqvTerm (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 (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@=? pevalOrTerm (pevalNotEqvTerm (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") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@=? pevalOrTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "Or(Or(x1, x2), y) -> Or(x2, y)" $ do
pevalOrTerm
(pevalOrTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@=? pevalOrTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "Or(Or(x1, x2), y) -> Or(x1, y)" $ do
pevalOrTerm
(pevalOrTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@=? pevalOrTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "Or(x, And(y1, y2)) -> x" $ do
pevalOrTerm
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@=? pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
pevalOrTerm
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@=? pevalNotEqvTerm (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
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@=? pevalOrTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "Or(And(x1, x2), y) -> y" $ do
pevalOrTerm
(pevalAndTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@=? pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
pevalOrTerm
(pevalAndTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@=? pevalNotEqvTerm (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
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@=? pevalOrTerm (pevalNotEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@=? pevalEqvTerm (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
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@=? pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@=? conTerm False,
testCase "And(x, And(y1, y2)) -> And(x, y2)" $ do
pevalAndTerm
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@=? pevalAndTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "And(x, And(y1, y2)) -> And(x, y1)" $ do
pevalAndTerm
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@=? pevalAndTerm (pevalEqvTerm (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
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalAndTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
@=? pevalAndTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b")
pevalAndTerm (ssymTerm "a") (pevalAndTerm (ssymTerm "b") (ssymTerm "a"))
@=? pevalAndTerm (ssymTerm "b") (ssymTerm "a")
pevalAndTerm
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
(pevalAndTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
@=? pevalAndTerm (ssymTerm "b") (pevalEqvTerm (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 (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalEqvTerm (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") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalEqvTerm (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 (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@=? pevalAndTerm (pevalEqvTerm (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") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
(pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
@=? pevalAndTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "And(And(x1, x2), y) -> And(x2, y)" $ do
pevalAndTerm
(pevalAndTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@=? pevalAndTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "And(And(x1, x2), y) -> And(x1, y)" $ do
pevalAndTerm
(pevalAndTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@=? pevalAndTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
testCase "And(x, Or(y1, y2)) -> x" $ do
pevalAndTerm
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@=? pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
pevalAndTerm
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@=? pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
@=? pevalAndTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
testCase "And(Or(x1, x2), y) -> y" $ do
pevalAndTerm
(pevalOrTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@=? pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
pevalAndTerm
(pevalOrTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
@=? pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
@=? pevalAndTerm (pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(ssymTerm "c")
@=? pevalAndTerm (pevalNotEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(ssymTerm "c")
@=? pevalAndTerm (pevalNotEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(ssymTerm "c")
@=? pevalITETerm (pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalAndTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(ssymTerm "c")
@=? pevalITETerm (pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(ssymTerm "c")
@=? pevalITETerm (pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(ssymTerm "c")
@=? pevalITETerm (pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
(ssymTerm "c")
@=? pevalOrTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
pevalITETerm
(ssymTerm "a")
(pevalOrTerm (ssymTerm "a") (ssymTerm "b"))
(ssymTerm "c")
@=? pevalOrTerm (ssymTerm "a") (ssymTerm "c")
pevalITETerm
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalOrTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
(ssymTerm "c")
@=? pevalOrTerm (pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNotTerm (pevalAndTerm (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b")))
(ssymTerm "c")
@=? pevalOrTerm (pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNotTerm (pevalAndTerm (ssymTerm "b") (pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))))
(ssymTerm "c")
@=? pevalOrTerm (pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNotTerm (pevalAndTerm (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b")))
(ssymTerm "c")
@=? pevalITETerm (pevalEqvTerm (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
(pevalEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
(pevalNotTerm (pevalAndTerm (ssymTerm "b") (pevalNotEqvTerm (ssymTerm "a" :: Term Integer) (conTerm 2))))
(ssymTerm "c")
@=? pevalITETerm (pevalEqvTerm (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"))
]
]