Skip to content

Commit

Permalink
t/unit: Use token names that aren't used as variables in the semantic…
Browse files Browse the repository at this point in the history 
…s to avoid parsing issues
  • Loading branch information
@lucaspena @nishantjr
lucaspena authored and nishantjr committed Apr 14, 2020
1 parent 882d567 commit d85aa38
Show file tree
Hide file tree
Showing 2 changed files with 40 additions and 38 deletions.
33 changes: 17 additions & 16 deletions prover/t/unit/match-assoc-comm.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,10 @@ module TEST-MATCH-ASSOC-COMM
syntax UpperName ::= "Data" [token]
| "Loc" [token]
| "W" [token] | "W1" [token] | "W2" [token]
| "X" [token] | "X1" [token] | "X2" [token]
| "Y" [token] | "Y1" [token] | "Y2" [token]
| "X0" [token] | "X1" [token] | "X2" [token]
| "Y0" [token] | "Y1" [token] | "Y2" [token]
| "Z" [token] | "Z1" [token] | "Z2" [token]
| "H0" [token]

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

rule test("match-assoc-comm", 2)
=> assert( #matchResult( subst: Z { Loc } |-> X { Loc }
W { Data } |-> Y { Data }
=> assert( #matchResult( subst: Z { Loc } |-> X0 { Loc }
W { Data } |-> Y0 { Data }
, rest: .Patterns
)
, .MatchResults
== #matchAssocComm( terms: pto( X { Loc }, Y { Data })
== #matchAssocComm( terms: pto( X0 { Loc }, Y0 { Data })
, pattern: pto( Z { Loc }, W { Data })
, variables: Z { Loc }, W { Data }
, results: .MatchResults
Expand Down Expand Up @@ -91,9 +92,9 @@ module TEST-MATCH-ASSOC-COMM
, .MatchResults
== #matchAssocComm( terms: pto( X1 { Loc }, Y1 { Loc })
, pto( X2 { Loc }, Y2 { Loc })
, pattern: pto( X { Loc }, Y { Loc })
, pto( Y { Loc }, Z { Loc })
, variables: X { Loc }, Y { Loc }, Z { Loc }
, pattern: pto( X0 { Loc }, Y0 { Loc })
, pto( Y0 { Loc }, Z { Loc })
, variables: X0 { Loc }, Y0 { Loc }, Z { Loc }
, results: .MatchResults
, subst: .Map
, rest: .Patterns
Expand All @@ -103,14 +104,14 @@ module TEST-MATCH-ASSOC-COMM

rule test("match-assoc-comm", 7)
=> assert( #error( "No valid substitution" )
, #matchResult( subst: W { Loc } |-> Y { Loc }
, #matchResult( subst: W { Loc } |-> Y0 { Loc }
, rest: .Patterns
)
, .MatchResults
== #matchAssocComm( terms: pto ( Y { Loc } , c(Z { Loc }) )
, pto ( X { Loc } , c(Y { Loc }) )
, pattern: pto ( X { Loc } , c(W { Loc }) )
, pto ( W { Loc } , c(Z { Loc }) )
== #matchAssocComm( terms: pto ( Y0 { Loc } , c(Z { Loc }) )
, pto ( X0 { Loc } , c(Y0 { Loc }) )
, pattern: pto ( X0 { Loc } , c(W { Loc }) )
, pto ( W { Loc } , c(Z { Loc }) )
, variables: W { Loc }
, results: .MatchResults
, subst: .Map
Expand All @@ -123,9 +124,9 @@ module TEST-MATCH-ASSOC-COMM
rule test("match-assoc-comm", 8)
=> assert( #error("Variable sort does not match term")
, .MatchResults
== #matchAssocComm( terms: pto ( W { X1 } , c(X { X1 }) )
, pattern: pto ( Y { X2 } , c(Z { X2 }) )
, variables: Y { X2 }, Z { X2 }
== #matchAssocComm( terms: pto ( W { X1 } , c(X0 { X1 }) )
, pattern: pto ( Y0 { X2 } , c(Z { X2 }) )
, variables: Y0 { X2 }, Z { X2 }
, results: .MatchResults
, subst: .Map
, rest: .Patterns
Expand Down
45 changes: 23 additions & 22 deletions prover/t/unit/match-assoc.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,14 @@ module TEST-MATCH-ASSOC
syntax UpperName ::= "Data" [token]
| "Loc" [token]
| "W" [token]
| "X" [token]
| "Y" [token]
| "X0" [token]
| "Y0" [token]
| "Z" [token]

rule test("match-assoc", 1)
=> assert( #error("No valid substitution"), .MatchResults
== #matchAssoc( terms: pto( X { Loc }, Y { Data })
, pattern: pto( Z { Loc }, W { Data })
== #matchAssoc( terms: pto( X0 { Loc }, Y0 { Data })
, pattern: pto( Z { Loc }, W { Data })
, variables: W { Data }
, subst: .Map
, rest: .Patterns
Expand All @@ -22,8 +22,8 @@ module TEST-MATCH-ASSOC
.Declarations
rule test("match-assoc", 2)
=> assert( #error("Constructors do not match"), .MatchResults
== #matchAssoc( terms: c( X { Loc }, Y { Data })
, pattern: d( Z { Loc }, W { Data })
== #matchAssoc( terms: c( X0 { Loc }, Y0 { Data })
, pattern: d( Z { Loc }, W { Data })
, variables: Z { Loc }, W { Data }
, subst: .Map
, rest: .Patterns
Expand All @@ -32,7 +32,7 @@ module TEST-MATCH-ASSOC
.Declarations
rule test("match-assoc", 3)
=> assert( #error( "Mismatch in length of arguments" ), .MatchResults
== #matchAssoc( terms: pto( X { Loc }, Y { Data })
== #matchAssoc( terms: pto( X0 { Loc }, Y0 { Data })
, pattern: .Patterns
, variables: .Patterns
, subst: .Map
Expand All @@ -42,8 +42,8 @@ module TEST-MATCH-ASSOC
.Declarations
rule test("match-assoc", 4)
=> assert( #error( "Mismatch in length of arguments" ), .MatchResults
== #matchAssoc( terms: c(X { Loc }, Y { Data })
, pattern: c(X { Loc }, Y { Data }, Y { Data })
== #matchAssoc( terms: c(X0 { Loc }, Y0 { Data })
, pattern: c(X0 { Loc }, Y0 { Data }, Y0 { Data })
, variables: .Patterns
, subst: .Map
, rest: .Patterns
Expand All @@ -66,13 +66,13 @@ module TEST-MATCH-ASSOC
.Declarations
// Basic Matching
rule test("match-assoc", 6)
=> assert( #matchResult( subst: Z { Loc } |-> X { Loc }
W { Data } |-> Y { Data }
=> assert( #matchResult( subst: Z { Loc } |-> X0 { Loc }
W { Data } |-> Y0 { Data }
, rest: .Patterns
)
, .MatchResults
== #matchAssoc( terms: pto( X { Loc }, Y { Data })
, pattern: pto( Z { Loc }, W { Data })
== #matchAssoc( terms: pto( X0 { Loc }, Y0 { Data })
, pattern: pto( Z { Loc }, W { Data })
, variables: Z { Loc }, W { Data }
, subst: .Map
, rest: .Patterns
Expand All @@ -81,13 +81,13 @@ module TEST-MATCH-ASSOC
.Declarations
// Match multiple occurances of a variable
rule test("match-assoc", 7)
=> assert( #matchResult( subst: Z { Loc } |-> X { Loc }
W { Data } |-> Y { Data }
=> assert( #matchResult( subst: Z { Loc } |-> X0 { Loc }
W { Data } |-> Y0 { Data }
, rest: .Patterns
)
, .MatchResults
== #matchAssoc( terms: c( X { Loc }, Y { Data }), d( X { Loc }, Y { Data })
, pattern: c( Z { Loc }, W { Data }), d( Z { Loc }, W { Data })
== #matchAssoc( terms: c( X0 { Loc }, Y0 { Data }), d( X0 { Loc }, Y0 { Data })
, pattern: c( Z { Loc }, W { Data }), d( Z { Loc }, W { Data })
, variables: Z { Loc }, W { Data }
, subst: .Map
, rest: .Patterns
Expand All @@ -98,8 +98,8 @@ module TEST-MATCH-ASSOC
rule test("match-assoc", 8)
=> assert( #error( "No valid substitution" )
, .MatchResults
== #matchAssoc( terms: c( X { Loc }, Y { Data }), c( X { Loc }, Y { Data })
, pattern: c( Z { Loc }, W { Data }), c( Y { Loc }, W { Data })
== #matchAssoc( terms: c( X0 { Loc }, Y0 { Data }), c( X0 { Loc }, Y0 { Data })
, pattern: c( Z { Loc }, W { Data }), c( Y0 { Loc }, W { Data })
, variables: Z { Loc }, W { Data }
, subst: .Map
, rest: .Patterns
Expand All @@ -109,10 +109,11 @@ module TEST-MATCH-ASSOC

// Match constructor against variable
rule test("match-assoc", 9)
=> assert( #error("Constructors do not match")
=> symbol pto ( Loc, Data ) : Heap
assert( #error("Constructors do not match")
, .MatchResults
== #matchAssoc( terms: X { Loc }, Y { Data }
, pattern: c( Z { Loc }, W { Data }), c( Y { Loc }, W { Data })
== #matchAssoc( terms: X0 { Loc }, Y0 { Data }
, pattern: c( Z { Loc }, W { Data }), c( Y0 { Loc }, W { Data })
, variables: Z { Loc }, W { Data }
, subst: .Map
, rest: .Patterns
Expand Down

0 comments on commit d85aa38

Please sign in to comment.