Skip to content

Commit d85aa38

Browse files
lucaspenanishantjr
lucaspena
authored and
nishantjr
committed
t/unit: Use token names that aren't used as variables in the semantics to avoid parsing issues
1 parent 882d567 commit d85aa38

2 files changed

Lines changed: 40 additions & 38 deletions

File tree

‎prover/t/unit/match-assoc-comm.k‎

Lines changed: 17 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,10 @@ module TEST-MATCH-ASSOC-COMM
66
syntax UpperName ::= "Data" [token]
77
| "Loc" [token]
88
| "W" [token] | "W1" [token] | "W2" [token]
9-
| "X" [token] | "X1" [token] | "X2" [token]
10-
| "Y" [token] | "Y1" [token] | "Y2" [token]
9+
| "X0" [token] | "X1" [token] | "X2" [token]
10+
| "Y0" [token] | "Y1" [token] | "Y2" [token]
1111
| "Z" [token] | "Z1" [token] | "Z2" [token]
12+
| "H0" [token]
1213

1314
rule test("match-assoc-comm", 1)
1415
=> assert( #matchResult( subst: .Map , rest: pto( Z { Loc }, W { Data }))
@@ -24,12 +25,12 @@ module TEST-MATCH-ASSOC-COMM
2425
.Declarations
2526

2627
rule test("match-assoc-comm", 2)
27-
=> assert( #matchResult( subst: Z { Loc } |-> X { Loc }
28-
W { Data } |-> Y { Data }
28+
=> assert( #matchResult( subst: Z { Loc } |-> X0 { Loc }
29+
W { Data } |-> Y0 { Data }
2930
, rest: .Patterns
3031
)
3132
, .MatchResults
32-
== #matchAssocComm( terms: pto( X { Loc }, Y { Data })
33+
== #matchAssocComm( terms: pto( X0 { Loc }, Y0 { Data })
3334
, pattern: pto( Z { Loc }, W { Data })
3435
, variables: Z { Loc }, W { Data }
3536
, results: .MatchResults
@@ -91,9 +92,9 @@ module TEST-MATCH-ASSOC-COMM
9192
, .MatchResults
9293
== #matchAssocComm( terms: pto( X1 { Loc }, Y1 { Loc })
9394
, pto( X2 { Loc }, Y2 { Loc })
94-
, pattern: pto( X { Loc }, Y { Loc })
95-
, pto( Y { Loc }, Z { Loc })
96-
, variables: X { Loc }, Y { Loc }, Z { Loc }
95+
, pattern: pto( X0 { Loc }, Y0 { Loc })
96+
, pto( Y0 { Loc }, Z { Loc })
97+
, variables: X0 { Loc }, Y0 { Loc }, Z { Loc }
9798
, results: .MatchResults
9899
, subst: .Map
99100
, rest: .Patterns
@@ -103,14 +104,14 @@ module TEST-MATCH-ASSOC-COMM
103104

104105
rule test("match-assoc-comm", 7)
105106
=> assert( #error( "No valid substitution" )
106-
, #matchResult( subst: W { Loc } |-> Y { Loc }
107+
, #matchResult( subst: W { Loc } |-> Y0 { Loc }
107108
, rest: .Patterns
108109
)
109110
, .MatchResults
110-
== #matchAssocComm( terms: pto ( Y { Loc } , c(Z { Loc }) )
111-
, pto ( X { Loc } , c(Y { Loc }) )
112-
, pattern: pto ( X { Loc } , c(W { Loc }) )
113-
, pto ( W { Loc } , c(Z { Loc }) )
111+
== #matchAssocComm( terms: pto ( Y0 { Loc } , c(Z { Loc }) )
112+
, pto ( X0 { Loc } , c(Y0 { Loc }) )
113+
, pattern: pto ( X0 { Loc } , c(W { Loc }) )
114+
, pto ( W { Loc } , c(Z { Loc }) )
114115
, variables: W { Loc }
115116
, results: .MatchResults
116117
, subst: .Map
@@ -123,9 +124,9 @@ module TEST-MATCH-ASSOC-COMM
123124
rule test("match-assoc-comm", 8)
124125
=> assert( #error("Variable sort does not match term")
125126
, .MatchResults
126-
== #matchAssocComm( terms: pto ( W { X1 } , c(X { X1 }) )
127-
, pattern: pto ( Y { X2 } , c(Z { X2 }) )
128-
, variables: Y { X2 }, Z { X2 }
127+
== #matchAssocComm( terms: pto ( W { X1 } , c(X0 { X1 }) )
128+
, pattern: pto ( Y0 { X2 } , c(Z { X2 }) )
129+
, variables: Y0 { X2 }, Z { X2 }
129130
, results: .MatchResults
130131
, subst: .Map
131132
, rest: .Patterns

‎prover/t/unit/match-assoc.k‎

Lines changed: 23 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,14 @@ module TEST-MATCH-ASSOC
66
syntax UpperName ::= "Data" [token]
77
| "Loc" [token]
88
| "W" [token]
9-
| "X" [token]
10-
| "Y" [token]
9+
| "X0" [token]
10+
| "Y0" [token]
1111
| "Z" [token]
1212

1313
rule test("match-assoc", 1)
1414
=> assert( #error("No valid substitution"), .MatchResults
15-
== #matchAssoc( terms: pto( X { Loc }, Y { Data })
16-
, pattern: pto( Z { Loc }, W { Data })
15+
== #matchAssoc( terms: pto( X0 { Loc }, Y0 { Data })
16+
, pattern: pto( Z { Loc }, W { Data })
1717
, variables: W { Data }
1818
, subst: .Map
1919
, rest: .Patterns
@@ -22,8 +22,8 @@ module TEST-MATCH-ASSOC
2222
.Declarations
2323
rule test("match-assoc", 2)
2424
=> assert( #error("Constructors do not match"), .MatchResults
25-
== #matchAssoc( terms: c( X { Loc }, Y { Data })
26-
, pattern: d( Z { Loc }, W { Data })
25+
== #matchAssoc( terms: c( X0 { Loc }, Y0 { Data })
26+
, pattern: d( Z { Loc }, W { Data })
2727
, variables: Z { Loc }, W { Data }
2828
, subst: .Map
2929
, rest: .Patterns
@@ -32,7 +32,7 @@ module TEST-MATCH-ASSOC
3232
.Declarations
3333
rule test("match-assoc", 3)
3434
=> assert( #error( "Mismatch in length of arguments" ), .MatchResults
35-
== #matchAssoc( terms: pto( X { Loc }, Y { Data })
35+
== #matchAssoc( terms: pto( X0 { Loc }, Y0 { Data })
3636
, pattern: .Patterns
3737
, variables: .Patterns
3838
, subst: .Map
@@ -42,8 +42,8 @@ module TEST-MATCH-ASSOC
4242
.Declarations
4343
rule test("match-assoc", 4)
4444
=> assert( #error( "Mismatch in length of arguments" ), .MatchResults
45-
== #matchAssoc( terms: c(X { Loc }, Y { Data })
46-
, pattern: c(X { Loc }, Y { Data }, Y { Data })
45+
== #matchAssoc( terms: c(X0 { Loc }, Y0 { Data })
46+
, pattern: c(X0 { Loc }, Y0 { Data }, Y0 { Data })
4747
, variables: .Patterns
4848
, subst: .Map
4949
, rest: .Patterns
@@ -66,13 +66,13 @@ module TEST-MATCH-ASSOC
6666
.Declarations
6767
// Basic Matching
6868
rule test("match-assoc", 6)
69-
=> assert( #matchResult( subst: Z { Loc } |-> X { Loc }
70-
W { Data } |-> Y { Data }
69+
=> assert( #matchResult( subst: Z { Loc } |-> X0 { Loc }
70+
W { Data } |-> Y0 { Data }
7171
, rest: .Patterns
7272
)
7373
, .MatchResults
74-
== #matchAssoc( terms: pto( X { Loc }, Y { Data })
75-
, pattern: pto( Z { Loc }, W { Data })
74+
== #matchAssoc( terms: pto( X0 { Loc }, Y0 { Data })
75+
, pattern: pto( Z { Loc }, W { Data })
7676
, variables: Z { Loc }, W { Data }
7777
, subst: .Map
7878
, rest: .Patterns
@@ -81,13 +81,13 @@ module TEST-MATCH-ASSOC
8181
.Declarations
8282
// Match multiple occurances of a variable
8383
rule test("match-assoc", 7)
84-
=> assert( #matchResult( subst: Z { Loc } |-> X { Loc }
85-
W { Data } |-> Y { Data }
84+
=> assert( #matchResult( subst: Z { Loc } |-> X0 { Loc }
85+
W { Data } |-> Y0 { Data }
8686
, rest: .Patterns
8787
)
8888
, .MatchResults
89-
== #matchAssoc( terms: c( X { Loc }, Y { Data }), d( X { Loc }, Y { Data })
90-
, pattern: c( Z { Loc }, W { Data }), d( Z { Loc }, W { Data })
89+
== #matchAssoc( terms: c( X0 { Loc }, Y0 { Data }), d( X0 { Loc }, Y0 { Data })
90+
, pattern: c( Z { Loc }, W { Data }), d( Z { Loc }, W { Data })
9191
, variables: Z { Loc }, W { Data }
9292
, subst: .Map
9393
, rest: .Patterns
@@ -98,8 +98,8 @@ module TEST-MATCH-ASSOC
9898
rule test("match-assoc", 8)
9999
=> assert( #error( "No valid substitution" )
100100
, .MatchResults
101-
== #matchAssoc( terms: c( X { Loc }, Y { Data }), c( X { Loc }, Y { Data })
102-
, pattern: c( Z { Loc }, W { Data }), c( Y { Loc }, W { Data })
101+
== #matchAssoc( terms: c( X0 { Loc }, Y0 { Data }), c( X0 { Loc }, Y0 { Data })
102+
, pattern: c( Z { Loc }, W { Data }), c( Y0 { Loc }, W { Data })
103103
, variables: Z { Loc }, W { Data }
104104
, subst: .Map
105105
, rest: .Patterns
@@ -109,10 +109,11 @@ module TEST-MATCH-ASSOC
109109

110110
// Match constructor against variable
111111
rule test("match-assoc", 9)
112-
=> assert( #error("Constructors do not match")
112+
=> symbol pto ( Loc, Data ) : Heap
113+
assert( #error("Constructors do not match")
113114
, .MatchResults
114-
== #matchAssoc( terms: X { Loc }, Y { Data }
115-
, pattern: c( Z { Loc }, W { Data }), c( Y { Loc }, W { Data })
115+
== #matchAssoc( terms: X0 { Loc }, Y0 { Data }
116+
, pattern: c( Z { Loc }, W { Data }), c( Y0 { Loc }, W { Data })
116117
, variables: Z { Loc }, W { Data }
117118
, subst: .Map
118119
, rest: .Patterns

0 commit comments

Comments
 (0)