grisette-0.5.0.0: test/Grisette/SymPrim/Prim/BVTests.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.SymPrim.Prim.BVTests (bvTests) where
import Data.Proxy (Proxy (Proxy))
import GHC.TypeNats (KnownNat, type (+), type (<=))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Term
( PEvalBVSignConversionTerm
( pevalBVToSignedTerm,
pevalBVToUnsignedTerm
),
PEvalBVTerm
( pevalBVConcatTerm,
pevalBVExtendTerm,
pevalBVSelectTerm
),
Term,
bvconcatTerm,
bvextendTerm,
bvselectTerm,
conTerm,
ssymTerm,
toSignedTerm,
toUnsignedTerm,
)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.HUnit ((@?=))
data ToSignedTest = ToSignedTest
{ toSignedTestName :: String,
toSignedTestTerm :: Term (WordN 4),
toSignedTestExpected :: Term (IntN 4)
}
data ToUnsignedTest = ToUnsignedTest
{ toUnsignedTestName :: String,
toUnsignedTestTerm :: Term (IntN 4),
toUnsignedTestExpected :: Term (WordN 4)
}
data BVSelectTest where
BVSelectTest ::
forall ix w n bv.
( PEvalBVTerm bv,
KnownNat ix,
1 <= n,
KnownNat w,
1 <= w,
KnownNat n,
ix + w <= n
) =>
{ bvSelectTestName :: String,
bvSelectIx :: Proxy ix,
bvSelectW :: Proxy w,
bvSelectTestTerm :: Term (bv n),
bvSelectTestExpected :: Term (bv w)
} ->
BVSelectTest
data BVExtendTest where
BVExtendTest ::
forall l r bv.
( PEvalBVTerm bv,
KnownNat l,
1 <= l,
KnownNat r,
1 <= r,
l <= r
) =>
{ bvExtendTestName :: String,
bvExtendSigned :: Bool,
bvExtendR :: Proxy r,
bvExtendTestTerm :: Term (bv l),
bvExtendExpected :: Term (bv r)
} ->
BVExtendTest
data BVConcatTest where
BVConcatTest ::
forall l r bv.
( PEvalBVTerm bv,
KnownNat l,
KnownNat r,
KnownNat (l + r),
1 <= l,
1 <= r,
1 <= l + r
) =>
{ bvConcatTestName :: String,
bvConcatTestLhs :: Term (bv l),
bvConcatTestRhs :: Term (bv r),
bvConcatTestExpected :: Term (bv (l + r))
} ->
BVConcatTest
bvTests :: Test
bvTests =
testGroup
"BV"
[ testGroup "pevalBVToSignedTerm" $ do
ToSignedTest name term expected <-
[ ToSignedTest
{ toSignedTestName = "concrete",
toSignedTestTerm = conTerm 6,
toSignedTestExpected = conTerm 6
},
ToSignedTest
{ toSignedTestName = "symbolic",
toSignedTestTerm = ssymTerm "a",
toSignedTestExpected = toSignedTerm $ ssymTerm "a"
},
ToSignedTest
{ toSignedTestName = "toUnsigned",
toSignedTestTerm = toUnsignedTerm $ ssymTerm "a",
toSignedTestExpected = ssymTerm "a"
},
ToSignedTest
{ toSignedTestName = "bvConcat",
toSignedTestTerm =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 2))
(ssymTerm "b" :: Term (WordN 2)),
toSignedTestExpected =
bvconcatTerm
(toSignedTerm (ssymTerm "a" :: Term (WordN 2)))
(toSignedTerm (ssymTerm "b" :: Term (WordN 2)))
},
ToSignedTest
{ toSignedTestName = "bvExtend",
toSignedTestTerm =
bvextendTerm True (Proxy @4) (ssymTerm "a" :: Term (WordN 2)),
toSignedTestExpected =
bvextendTerm
True
(Proxy @4)
(toSignedTerm (ssymTerm "a" :: Term (WordN 2)))
}
]
return $ testCase name $ do
let actual = pevalBVToSignedTerm term
actual @?= expected,
testGroup "pevalBVToUnsignedTerm" $ do
ToUnsignedTest name term expected <-
[ ToUnsignedTest
{ toUnsignedTestName = "concrete",
toUnsignedTestTerm = conTerm 6,
toUnsignedTestExpected = conTerm 6
},
ToUnsignedTest
{ toUnsignedTestName = "symbolic",
toUnsignedTestTerm = ssymTerm "a",
toUnsignedTestExpected = toUnsignedTerm $ ssymTerm "a"
},
ToUnsignedTest
{ toUnsignedTestName = "toSigned",
toUnsignedTestTerm = toSignedTerm $ ssymTerm "a",
toUnsignedTestExpected = ssymTerm "a"
},
ToUnsignedTest
{ toUnsignedTestName = "bvConcat",
toUnsignedTestTerm =
bvconcatTerm
(ssymTerm "a" :: Term (IntN 2))
(ssymTerm "b" :: Term (IntN 2)),
toUnsignedTestExpected =
bvconcatTerm
(toUnsignedTerm (ssymTerm "a" :: Term (IntN 2)))
(toUnsignedTerm (ssymTerm "b" :: Term (IntN 2)))
},
ToUnsignedTest
{ toUnsignedTestName = "bvExtend",
toUnsignedTestTerm =
bvextendTerm True (Proxy @4) (ssymTerm "a" :: Term (IntN 2)),
toUnsignedTestExpected =
bvextendTerm
True
(Proxy @4)
(toUnsignedTerm (ssymTerm "a" :: Term (IntN 2)))
}
]
return $ testCase name $ do
let actual = pevalBVToUnsignedTerm term
actual @?= expected,
testGroup "pevalBVSelectTerm" $ do
BVSelectTest name ix w term expected <-
[ BVSelectTest
{ bvSelectTestName = "concrete 0 1",
bvSelectIx = Proxy @0,
bvSelectW = Proxy @1,
bvSelectTestTerm = conTerm 6 :: Term (WordN 4),
bvSelectTestExpected = conTerm 0
},
BVSelectTest
{ bvSelectTestName = "concrete 1 1",
bvSelectIx = Proxy @1,
bvSelectW = Proxy @1,
bvSelectTestTerm = conTerm 6 :: Term (WordN 4),
bvSelectTestExpected = conTerm 1
},
BVSelectTest
{ bvSelectTestName = "concrete 2 1",
bvSelectIx = Proxy @2,
bvSelectW = Proxy @1,
bvSelectTestTerm = conTerm 6 :: Term (WordN 4),
bvSelectTestExpected = conTerm 1
},
BVSelectTest
{ bvSelectTestName = "concrete 3 1",
bvSelectIx = Proxy @3,
bvSelectW = Proxy @1,
bvSelectTestTerm = conTerm 6 :: Term (WordN 4),
bvSelectTestExpected = conTerm 0
},
BVSelectTest
{ bvSelectTestName = "concrete 0 2",
bvSelectIx = Proxy @0,
bvSelectW = Proxy @2,
bvSelectTestTerm = conTerm 6 :: Term (WordN 4),
bvSelectTestExpected = conTerm 2
},
BVSelectTest
{ bvSelectTestName = "concrete 1 2",
bvSelectIx = Proxy @1,
bvSelectW = Proxy @2,
bvSelectTestTerm = conTerm 6 :: Term (WordN 4),
bvSelectTestExpected = conTerm 3
},
BVSelectTest
{ bvSelectTestName = "concrete 0 4",
bvSelectIx = Proxy @0,
bvSelectW = Proxy @4,
bvSelectTestTerm = conTerm 6 :: Term (WordN 4),
bvSelectTestExpected = conTerm 6
},
BVSelectTest
{ bvSelectTestName = "symbolic",
bvSelectIx = Proxy @2,
bvSelectW = Proxy @1,
bvSelectTestTerm = ssymTerm "a" :: Term (WordN 4),
bvSelectTestExpected =
bvselectTerm
(Proxy @2)
(Proxy @1)
(ssymTerm "a" :: Term (WordN 4))
},
BVSelectTest
{ bvSelectTestName = "On ToSigned",
bvSelectIx = Proxy @2,
bvSelectW = Proxy @1,
bvSelectTestTerm =
toSignedTerm (ssymTerm "a" :: Term (WordN 4)),
bvSelectTestExpected =
toSignedTerm
( bvselectTerm
(Proxy @2)
(Proxy @1)
(ssymTerm "a" :: Term (WordN 4))
)
},
BVSelectTest
{ bvSelectTestName = "On ToUnsigned",
bvSelectIx = Proxy @2,
bvSelectW = Proxy @1,
bvSelectTestTerm =
toUnsignedTerm (ssymTerm "a" :: Term (IntN 4)),
bvSelectTestExpected =
toUnsignedTerm
( bvselectTerm
(Proxy @2)
(Proxy @1)
(ssymTerm "a" :: Term (IntN 4))
)
},
BVSelectTest
{ bvSelectTestName = "On BVSelect",
bvSelectIx = Proxy @3,
bvSelectW = Proxy @2,
bvSelectTestTerm =
bvselectTerm
(Proxy @2)
(Proxy @6)
(ssymTerm "a" :: Term (WordN 16)),
bvSelectTestExpected =
bvselectTerm
(Proxy @5)
(Proxy @2)
(ssymTerm "a" :: Term (WordN 16))
},
BVSelectTest
{ bvSelectTestName = "Whole vector",
bvSelectIx = Proxy @0,
bvSelectW = Proxy @4,
bvSelectTestTerm = ssymTerm "a" :: Term (WordN 4),
bvSelectTestExpected = ssymTerm "a"
},
BVSelectTest
{ bvSelectTestName = "bvConcat only lower part",
bvSelectIx = Proxy @1,
bvSelectW = Proxy @2,
bvSelectTestTerm =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4)),
bvSelectTestExpected =
bvselectTerm
(Proxy @1)
(Proxy @2)
(ssymTerm "b" :: Term (WordN 4))
},
BVSelectTest
{ bvSelectTestName = "bvConcat whole lower part",
bvSelectIx = Proxy @0,
bvSelectW = Proxy @4,
bvSelectTestTerm =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4)),
bvSelectTestExpected = ssymTerm "b" :: Term (WordN 4)
},
BVSelectTest
{ bvSelectTestName = "bvConcat only higher part",
bvSelectIx = Proxy @5,
bvSelectW = Proxy @2,
bvSelectTestTerm =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4)),
bvSelectTestExpected =
bvselectTerm
(Proxy @1)
(Proxy @2)
(ssymTerm "a" :: Term (WordN 4))
},
BVSelectTest
{ bvSelectTestName = "bvConcat whole higher part",
bvSelectIx = Proxy @4,
bvSelectW = Proxy @4,
bvSelectTestTerm =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4)),
bvSelectTestExpected = ssymTerm "a" :: Term (WordN 4)
},
BVSelectTest
{ bvSelectTestName = "bvConcat cross border",
bvSelectIx = Proxy @3,
bvSelectW = Proxy @4,
bvSelectTestTerm =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4)),
bvSelectTestExpected =
bvconcatTerm
( bvselectTerm
(Proxy @0)
(Proxy @3)
(ssymTerm "a" :: Term (WordN 4))
)
( bvselectTerm
(Proxy @3)
(Proxy @1)
(ssymTerm "b" :: Term (WordN 4))
)
},
BVSelectTest
{ bvSelectTestName = "bvExtend only lower part",
bvSelectIx = Proxy @1,
bvSelectW = Proxy @2,
bvSelectTestTerm =
bvextendTerm True (Proxy @8) (ssymTerm "a" :: Term (WordN 4)),
bvSelectTestExpected =
bvselectTerm
(Proxy @1)
(Proxy @2)
(ssymTerm "a" :: Term (WordN 4))
},
BVSelectTest
{ bvSelectTestName = "bvExtend whole lower part",
bvSelectIx = Proxy @0,
bvSelectW = Proxy @4,
bvSelectTestTerm =
bvextendTerm True (Proxy @8) (ssymTerm "a" :: Term (WordN 4)),
bvSelectTestExpected = ssymTerm "a" :: Term (WordN 4)
},
BVSelectTest
{ bvSelectTestName = "bvExtend cross boarder",
bvSelectIx = Proxy @3,
bvSelectW = Proxy @4,
bvSelectTestTerm =
bvextendTerm True (Proxy @8) (ssymTerm "a" :: Term (WordN 4)),
bvSelectTestExpected =
bvextendTerm True (Proxy @4) $
bvselectTerm
(Proxy @3)
(Proxy @1)
(ssymTerm "a" :: Term (WordN 4))
}
]
return . testCase name $
pevalBVSelectTerm ix w term @?= expected,
testGroup "pevalBVExtendTerm" $ do
BVExtendTest name signed pr term expected <-
[ BVExtendTest
{ bvExtendTestName = "Concrete zext on negative",
bvExtendSigned = False,
bvExtendR = Proxy @6,
bvExtendTestTerm = conTerm 15 :: Term (WordN 4),
bvExtendExpected = conTerm 15 :: Term (WordN 6)
},
BVExtendTest
{ bvExtendTestName = "Concrete sext on negative",
bvExtendSigned = True,
bvExtendR = Proxy @6,
bvExtendTestTerm = conTerm 15 :: Term (WordN 4),
bvExtendExpected = conTerm 63 :: Term (WordN 6)
},
BVExtendTest
{ bvExtendTestName = "Concrete zext on positive",
bvExtendSigned = False,
bvExtendR = Proxy @6,
bvExtendTestTerm = conTerm 7 :: Term (WordN 4),
bvExtendExpected = conTerm 7 :: Term (WordN 6)
},
BVExtendTest
{ bvExtendTestName = "Concrete sext on positive",
bvExtendSigned = True,
bvExtendR = Proxy @6,
bvExtendTestTerm = conTerm 7 :: Term (WordN 4),
bvExtendExpected = conTerm 7 :: Term (WordN 6)
},
BVExtendTest
{ bvExtendTestName = "Same width",
bvExtendSigned = False,
bvExtendR = Proxy @4,
bvExtendTestTerm = ssymTerm "a" :: Term (WordN 4),
bvExtendExpected = ssymTerm "a" :: Term (WordN 4)
},
BVExtendTest
{ bvExtendTestName = "Symbolic zext",
bvExtendSigned = False,
bvExtendR = Proxy @6,
bvExtendTestTerm = ssymTerm "a" :: Term (WordN 4),
bvExtendExpected =
bvconcatTerm
(conTerm 0 :: Term (WordN 2))
(ssymTerm "a" :: Term (WordN 4))
},
BVExtendTest
{ bvExtendTestName = "Symbolic sext on sext",
bvExtendSigned = True,
bvExtendR = Proxy @6,
bvExtendTestTerm =
pevalBVExtendTerm
True
(Proxy @4)
(ssymTerm "a" :: Term (WordN 2)),
bvExtendExpected =
bvextendTerm True (Proxy @6) (ssymTerm "a" :: Term (WordN 2))
}
]
return . testCase name $
pevalBVExtendTerm signed pr term @?= expected,
testGroup "pevalBVConcatTerm" $ do
BVConcatTest name lhs rhs expected <-
[ BVConcatTest
{ bvConcatTestName = "[c1 c2] -> c1c2",
bvConcatTestLhs = conTerm 3 :: Term (WordN 4),
bvConcatTestRhs = conTerm 5 :: Term (WordN 3),
bvConcatTestExpected = conTerm 29
},
BVConcatTest
{ bvConcatTestName = "[c1 (c2 s)] -> (c1c2 s)",
bvConcatTestLhs = conTerm 3 :: Term (WordN 4),
bvConcatTestRhs =
bvconcatTerm
(conTerm 5 :: Term (WordN 3))
(ssymTerm "b" :: Term (WordN 3)),
bvConcatTestExpected =
bvconcatTerm
(conTerm 29 :: Term (WordN 7))
( ssymTerm "b" :: Term (WordN 3)
)
},
BVConcatTest
{ bvConcatTestName = "[c1 (s c2)] -> (c1 (s c2))",
bvConcatTestLhs = conTerm 3 :: Term (WordN 4),
bvConcatTestRhs =
bvconcatTerm
(ssymTerm "b" :: Term (WordN 3))
(conTerm 5 :: Term (WordN 3)),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "b" :: Term (WordN 3))
(conTerm 5 :: Term (WordN 3))
)
},
BVConcatTest
{ bvConcatTestName = "[c1 (c2 (s c3))] -> (c1c2 (s c3))",
bvConcatTestLhs = conTerm 3 :: Term (WordN 4),
bvConcatTestRhs =
bvconcatTerm (conTerm 5 :: Term (WordN 5)) $
bvconcatTerm
(ssymTerm "b" :: Term (WordN 6))
(conTerm 7 :: Term (WordN 7)),
bvConcatTestExpected =
bvconcatTerm
(conTerm 101 :: Term (WordN 9))
( bvconcatTerm
(ssymTerm "b" :: Term (WordN 6))
(conTerm 7 :: Term (WordN 7))
)
},
BVConcatTest
{ bvConcatTestName = "[c s] -> (c s)",
bvConcatTestLhs = conTerm 3 :: Term (WordN 4),
bvConcatTestRhs = ssymTerm "b" :: Term (WordN 3),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 3))
},
BVConcatTest
{ bvConcatTestName = "[(c1 s) c2] -> (c1 (s c2))",
bvConcatTestLhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
(ssymTerm "a" :: Term (WordN 4)),
bvConcatTestRhs = conTerm 5 :: Term (WordN 3),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
( conTerm 5 :: Term (WordN 3)
)
)
},
BVConcatTest
{ bvConcatTestName = "[(c1 s1) (c2 s2)] -> (c1 (s1 (c2 s2)))",
bvConcatTestLhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
(ssymTerm "a" :: Term (WordN 4)),
bvConcatTestRhs =
bvconcatTerm
(conTerm 5 :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4)),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
( bvconcatTerm
(conTerm 5 :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4))
)
)
},
BVConcatTest
{ bvConcatTestName = "[(c1 s1) (s2 c2)] -> (c1 ((s1 s2) c2))",
bvConcatTestLhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
(ssymTerm "a" :: Term (WordN 4)),
bvConcatTestRhs =
bvconcatTerm
(ssymTerm "b" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4)),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4))
)
(conTerm 5 :: Term (WordN 4))
)
},
BVConcatTest
{ bvConcatTestName =
"[(c1 s1) (c2 (s2 c3))] -> (c1 (((s1 c2) s2)) c3))",
bvConcatTestLhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
(ssymTerm "a" :: Term (WordN 4)),
bvConcatTestRhs =
bvconcatTerm
(conTerm 5 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "b" :: Term (WordN 4))
(conTerm 7 :: Term (WordN 4))
),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
( bvconcatTerm
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
)
(ssymTerm "b" :: Term (WordN 4))
)
(conTerm 7 :: Term (WordN 4))
)
},
BVConcatTest
{ bvConcatTestName = "[(c s1) s2] -> (c (s1 s2))",
bvConcatTestLhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
(ssymTerm "a" :: Term (WordN 4)),
bvConcatTestRhs = ssymTerm "b" :: Term (WordN 3),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 3))
)
},
BVConcatTest
{ bvConcatTestName = "[(s c1) c2] -> (s c1c2)",
bvConcatTestLhs =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 3)),
bvConcatTestRhs = conTerm 3 :: Term (WordN 4),
bvConcatTestExpected =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 83 :: Term (WordN 7))
},
BVConcatTest
{ bvConcatTestName = "[(s1 c1) (c2 s2)] -> (s1 (c1c2 s2))",
bvConcatTestLhs =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4)),
bvConcatTestRhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4)),
bvConcatTestExpected =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
( bvconcatTerm
(conTerm 83 :: Term (WordN 8))
(ssymTerm "b" :: Term (WordN 4))
)
},
BVConcatTest
{ bvConcatTestName = "[(s1 c1) (s2 c2)] -> (((s1 c1) s2) c2)",
bvConcatTestLhs =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4)),
bvConcatTestRhs =
bvconcatTerm
(ssymTerm "b" :: Term (WordN 4))
(conTerm 3 :: Term (WordN 4)),
bvConcatTestExpected =
bvconcatTerm
( bvconcatTerm
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
)
(ssymTerm "b" :: Term (WordN 4))
)
(conTerm 3 :: Term (WordN 4))
},
BVConcatTest
{ bvConcatTestName =
"[(s1 c1) (c2 (s2 c3))] -> (((s1 c1c2) s2) c3)",
bvConcatTestLhs =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4)),
bvConcatTestRhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "b" :: Term (WordN 4))
(conTerm 7 :: Term (WordN 4))
),
bvConcatTestExpected =
bvconcatTerm
( bvconcatTerm
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 83 :: Term (WordN 8))
)
( ssymTerm "b" :: Term (WordN 4)
)
)
(conTerm 7 :: Term (WordN 4))
},
BVConcatTest
{ bvConcatTestName = "[(s1 c1) s2] -> ((s1 c1) s2)",
bvConcatTestLhs =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4)),
bvConcatTestRhs = ssymTerm "b" :: Term (WordN 3),
bvConcatTestExpected =
bvconcatTerm
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
)
(ssymTerm "b" :: Term (WordN 3))
},
BVConcatTest
{ bvConcatTestName = "[(c1 (s1 c2)) c3] -> (c1 (s1 c2c3))",
bvConcatTestLhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
),
bvConcatTestRhs = conTerm 7 :: Term (WordN 4),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 87 :: Term (WordN 8))
)
},
BVConcatTest
{ bvConcatTestName =
"[(c1 (s1 c2)) (c3 s3)] -> (c1 (s1 (c2c3 s3)))",
bvConcatTestLhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
),
bvConcatTestRhs =
bvconcatTerm
(conTerm 7 :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4)),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
( bvconcatTerm
(conTerm 87 :: Term (WordN 8))
( ssymTerm "b" :: Term (WordN 4)
)
)
)
},
BVConcatTest
{ bvConcatTestName =
"[(c1 (s1 c2)) (s2 c3)] -> (c1 (((s1 c2) s2) c3))",
bvConcatTestLhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
),
bvConcatTestRhs =
bvconcatTerm
(ssymTerm "b" :: Term (WordN 4))
(conTerm 7 :: Term (WordN 4)),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
( bvconcatTerm
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
)
(ssymTerm "b" :: Term (WordN 4))
)
(conTerm 7 :: Term (WordN 4))
)
},
BVConcatTest
{ bvConcatTestName =
"[(c1 (s1 c2)) (c3 (s2 c4))] -> (c1 (((s1 c2c3) s2) c4))",
bvConcatTestLhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
),
bvConcatTestRhs =
bvconcatTerm
(conTerm 7 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "b" :: Term (WordN 4))
(conTerm 9 :: Term (WordN 4))
),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
( bvconcatTerm
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 87 :: Term (WordN 8))
)
(ssymTerm "b" :: Term (WordN 4))
)
(conTerm 9 :: Term (WordN 4))
)
},
BVConcatTest
{ bvConcatTestName = "[(c1 (s1 c2)) s2] -> (c1 ((s1 c2) s2))",
bvConcatTestLhs =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
),
bvConcatTestRhs = ssymTerm "b" :: Term (WordN 3),
bvConcatTestExpected =
bvconcatTerm
(conTerm 3 :: Term (WordN 4))
( bvconcatTerm
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
)
( ssymTerm "b" :: Term (WordN 3)
)
)
},
BVConcatTest
{ bvConcatTestName = "[s c] -> (s c)",
bvConcatTestLhs = ssymTerm "a" :: Term (WordN 4),
bvConcatTestRhs = conTerm 5 :: Term (WordN 4),
bvConcatTestExpected =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
},
BVConcatTest
{ bvConcatTestName = "[s (c s)] -> (s (c s))",
bvConcatTestLhs = ssymTerm "a" :: Term (WordN 4),
bvConcatTestRhs =
bvconcatTerm
(conTerm 5 :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4)),
bvConcatTestExpected =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
( bvconcatTerm
(conTerm 5 :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4))
)
},
BVConcatTest
{ bvConcatTestName = "[s (s c)] -> ((s s) c))",
bvConcatTestLhs = ssymTerm "a" :: Term (WordN 4),
bvConcatTestRhs =
bvconcatTerm
(ssymTerm "b" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4)),
bvConcatTestExpected =
bvconcatTerm
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4))
)
(conTerm 5 :: Term (WordN 4))
},
BVConcatTest
{ bvConcatTestName = "[s (c (s c))] -> (((s c) s)) c)",
bvConcatTestLhs = ssymTerm "a" :: Term (WordN 4),
bvConcatTestRhs =
bvconcatTerm
(conTerm 5 :: Term (WordN 4))
( bvconcatTerm
(ssymTerm "b" :: Term (WordN 4))
(conTerm 7 :: Term (WordN 4))
),
bvConcatTestExpected =
bvconcatTerm
( bvconcatTerm
( bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(conTerm 5 :: Term (WordN 4))
)
(ssymTerm "b" :: Term (WordN 4))
)
(conTerm 7 :: Term (WordN 4))
},
BVConcatTest
{ bvConcatTestName = "[s1 s2] -> (s1 s2)",
bvConcatTestLhs = ssymTerm "a" :: Term (WordN 4),
bvConcatTestRhs = ssymTerm "b" :: Term (WordN 3),
bvConcatTestExpected =
bvconcatTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 3))
}
]
return . testCase name $
pevalBVConcatTerm lhs rhs @?= expected
]