1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
module Unit
( unitTests
)
where
import Control.Lens
import Parser (parseUnitTests)
import Reduce (reduceUnitTests)
import Test.Tasty
import Test.Tasty.HUnit
import VeriFuzz
unitTests :: TestTree
unitTests = testGroup
"Unit tests"
[ testCase "Transformation of AST" $ assertEqual
"Successful transformation"
transformExpectedResult
(transform trans transformTestData)
, parseUnitTests
, reduceUnitTests
]
transformTestData :: Expr
transformTestData = BinOp
(BinOp (BinOp (Id "id1") BinAnd (Id "id2"))
BinAnd
(BinOp (Id "id1") BinAnd (Id "id2"))
)
BinAnd
(BinOp
(BinOp
(BinOp (Id "id1") BinAnd (Id "id2"))
BinAnd
(BinOp
(Id "id1")
BinAnd
(BinOp (BinOp (Id "id1") BinAnd (Id "id2"))
BinAnd
(BinOp (Id "id1") BinAnd (Id "id2"))
)
)
)
BinOr
(Concat
[ Concat
[ Concat [Id "id1", Id "id2", Id "id2"]
, Id "id2"
, Id "id2"
, Concat [Id "id2", Id "id2", Concat [Id "id1", Id "id2"]]
, Id "id2"
]
, Id "id1"
, Id "id2"
]
)
)
transformExpectedResult :: Expr
transformExpectedResult = BinOp
(BinOp (BinOp (Id "id1") BinAnd (Id "Replaced"))
BinAnd
(BinOp (Id "id1") BinAnd (Id "Replaced"))
)
BinAnd
(BinOp
(BinOp
(BinOp (Id "id1") BinAnd (Id "Replaced"))
BinAnd
(BinOp
(Id "id1")
BinAnd
(BinOp (BinOp (Id "id1") BinAnd (Id "Replaced"))
BinAnd
(BinOp (Id "id1") BinAnd (Id "Replaced"))
)
)
)
BinOr
(Concat
[ Concat
[ Concat [Id "id1", Id "Replaced", Id "Replaced"]
, Id "Replaced"
, Id "Replaced"
, Concat
[ Id "Replaced"
, Id "Replaced"
, Concat [Id "id1", Id "Replaced"]
]
, Id "Replaced"
]
, Id "id1"
, Id "Replaced"
]
)
)
trans :: Expr -> Expr
trans e = case e of
Id i -> if i == Identifier "id2" then Id $ Identifier "Replaced" else Id i
_ -> e
|
