grisette-0.12.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
( PEvalBVTerm
( pevalBVConcatTerm,
pevalBVExtendTerm,
pevalBVSelectTerm
),
PEvalBitCastTerm (pevalBitCastTerm),
SupportedPrim,
Term,
bitCastTerm,
bvConcatTerm,
bvExtendTerm,
bvSelectTerm,
conTerm,
ssymTerm,
)
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,
SupportedPrim (bv w)
) =>
{ 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,
SupportedPrim (bv 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,
SupportedPrim (bv (l + r))
) =>
{ bvConcatTestName :: String,
bvConcatTestLhs :: Term (bv l),
bvConcatTestRhs :: Term (bv r),
bvConcatTestExpected :: Term (bv (l + r))
} ->
BVConcatTest
bvTests :: Test
bvTests =
testGroup
"BV"
[ testGroup "pevalBitCastTerm to signed" $ do
ToSignedTest name term expected <-
[ ToSignedTest
{ toSignedTestName = "concrete",
toSignedTestTerm = conTerm 6,
toSignedTestExpected = conTerm 6
},
ToSignedTest
{ toSignedTestName = "symbolic",
toSignedTestTerm = ssymTerm "a",
toSignedTestExpected =
bitCastTerm @(WordN 4) @(IntN 4) $ ssymTerm "a"
},
ToSignedTest
{ toSignedTestName = "toUnsigned",
toSignedTestTerm =
bitCastTerm @(IntN 4) @(WordN 4) $ ssymTerm "a",
toSignedTestExpected = ssymTerm "a"
},
ToSignedTest
{ toSignedTestName = "bvConcat",
toSignedTestTerm =
bvConcatTerm
(ssymTerm "a" :: Term (WordN 2))
(ssymTerm "b" :: Term (WordN 2)),
toSignedTestExpected =
bvConcatTerm
( bitCastTerm (ssymTerm "a" :: Term (WordN 2)) ::
Term (IntN 2)
)
(bitCastTerm (ssymTerm "b" :: Term (WordN 2)))
},
ToSignedTest
{ toSignedTestName = "bvExtend",
toSignedTestTerm =
bvExtendTerm True (Proxy @4) (ssymTerm "a" :: Term (WordN 2)),
toSignedTestExpected =
bvExtendTerm
True
(Proxy @4)
(bitCastTerm @(WordN 2) @(IntN 2) (ssymTerm "a"))
}
]
return $ testCase name $ do
let actual = pevalBitCastTerm term
actual @?= expected,
testGroup "pevalBitCastTerm to unsigned" $ do
ToUnsignedTest name term expected <-
[ ToUnsignedTest
{ toUnsignedTestName = "concrete",
toUnsignedTestTerm = conTerm 6,
toUnsignedTestExpected = conTerm 6
},
ToUnsignedTest
{ toUnsignedTestName = "symbolic",
toUnsignedTestTerm = ssymTerm "a",
toUnsignedTestExpected =
bitCastTerm @(IntN 4) @(WordN 4) $ ssymTerm "a"
},
ToUnsignedTest
{ toUnsignedTestName = "toSigned",
toUnsignedTestTerm =
bitCastTerm @(WordN 4) @(IntN 4) $ ssymTerm "a",
toUnsignedTestExpected = ssymTerm "a"
},
ToUnsignedTest
{ toUnsignedTestName = "bvConcat",
toUnsignedTestTerm =
bvConcatTerm
(ssymTerm "a" :: Term (IntN 2))
(ssymTerm "b" :: Term (IntN 2)),
toUnsignedTestExpected =
bvConcatTerm
(bitCastTerm @(IntN 2) @(WordN 2) (ssymTerm "a"))
(bitCastTerm (ssymTerm "b" :: Term (IntN 2)))
},
ToUnsignedTest
{ toUnsignedTestName = "bvExtend",
toUnsignedTestTerm =
bvExtendTerm True (Proxy @4) (ssymTerm "a" :: Term (IntN 2)),
toUnsignedTestExpected =
bvExtendTerm
True
(Proxy @4)
(bitCastTerm @(IntN 2) @(WordN 2) (ssymTerm "a"))
}
]
return $ testCase name $ do
let actual = pevalBitCastTerm 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 =
bitCastTerm @(WordN 4) @(IntN 4) (ssymTerm "a"),
bvSelectTestExpected =
bitCastTerm
( bvSelectTerm
(Proxy @2)
(Proxy @1)
(ssymTerm "a" :: Term (WordN 4))
)
},
BVSelectTest
{ bvSelectTestName = "On ToUnsigned",
bvSelectIx = Proxy @2,
bvSelectW = Proxy @1,
bvSelectTestTerm =
bitCastTerm @(IntN 4) @(WordN 4) (ssymTerm "a"),
bvSelectTestExpected =
bitCastTerm
( 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
]