Skip to content

Commit

Permalink
t/unit/match: fix test cases
Browse files Browse the repository at this point in the history
  • Loading branch information
@lucaspena
lucaspena committed Jun 10, 2020
1 parent 4d2c0a4 commit 2c3ab94
Showing 1 changed file with 35 additions and 50 deletions.
85 changes: 35 additions & 50 deletions prover/t/unit/match-assoc-comm.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module TEST-MATCH-ASSOC-COMM
| "d" [token]
syntax UpperName ::= "Data" [token]
| "Loc" [token]
| "W" [token] | "W1" [token] | "W2" [token]
| "W" [token] | "W0" [token] | "W1" [token] | "W2" [token]
| "X0" [token] | "X1" [token] | "X2" [token]
| "Y0" [token] | "Y1" [token] | "Y2" [token]
| "Z" [token] | "Z1" [token] | "Z2" [token]
Expand Down Expand Up @@ -155,45 +155,29 @@ module TEST-MATCH-ASSOC-COMM
)
.Declarations

rule test("match-assoc-comm", 10)
=> assert( #error( "Heap variable must be at end of pattern" )
, .MatchResults
== #matchAssocComm( terms: H0 { Heap }
, pto ( X1 { Loc } , Y1 { Data } )
, pto ( X2 { Loc } , c( W1 { Loc } , Z1 { Loc }) )
, pattern: H1 { Heap }
, pto ( X1 { Loc } , Y2 { Data } )
, variables: Y2 { Data }
, H1 { Heap }
, results: .MatchResults
, subst: .Map
, rest: .Patterns
)
)
.Declarations

// Matching on a symbolic heap
rule test("match-assoc-comm", 11)
=> assert( #matchResult( subst: H0 { Heap } |-> pto ( X1 { Loc } , Y1 { Data } )
W { Loc } |-> X2 { Loc }
Z { Data } |-> Y2 { Data }
, rest: .Patterns
)
, #matchResult( subst: H0 { Heap } |-> pto ( X2 { Loc } , Y2 { Data } )
rule test("match-assoc-comm", 10)
=> assert( #matchResult( subst: H0 { Heap } |-> sep ( pto ( X2 { Loc } , Y2 { Data } ) )
W { Loc } |-> X1 { Loc }
Z { Data } |-> Y1 { Data }
, rest: .Patterns
)
, #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
W { Loc } |-> X1 { Loc }
Z { Data } |-> Y1 { Data }
, rest: pto ( X2 { Loc } , Y2 { Data } )
)
, #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
W { Loc } |-> X1 { Loc }
Z { Data } |-> Y1 { Data }
, rest: pto ( X1 { Loc } , Y1 { Data } )
, #matchResult( subst: H0 { Heap } |-> sep ( pto ( X1 { Loc } , Y1 { Data } ) )
W { Loc } |-> X2 { Loc }
Z { Data } |-> Y2 { Data }
, rest: .Patterns
)
// TODO: we need to be getting these results as well
// , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
// W { Loc } |-> X1 { Loc }
// Z { Data } |-> Y1 { Data }
// , rest: pto ( X2 { Loc } , Y2 { Data } )
// )
// , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
// W { Loc } |-> X1 { Loc }
// Z { Data } |-> Y1 { Data }
// , rest: pto ( X1 { Loc } , Y1 { Data } )
// )
, .MatchResults
== #matchAssocComm( terms: pto ( X1 { Loc } , Y1 { Data } )
, pto ( X2 { Loc } , Y2 { Data } )
Expand All @@ -208,27 +192,28 @@ module TEST-MATCH-ASSOC-COMM
.Declarations

// Matching on a symbolic heap
rule test("match-assoc-comm", 12)
=> assert( #matchResult( subst: H0 { Heap } |-> pto ( X1 { Loc } , Y1 { Data } )
W { Loc } |-> X2 { Loc }
Z { Data } |-> Y2 { Data }
, rest: .Patterns
)
, #matchResult( subst: H0 { Heap } |-> pto ( X2 { Loc } , Y2 { Data } )
rule test("match-assoc-comm", 11)
=> assert( #matchResult( subst: H0 { Heap } |-> sep ( pto ( X2 { Loc } , Y2 { Data } ) )
W { Loc } |-> X1 { Loc }
Z { Data } |-> Y1 { Data }
, rest: .Patterns
)
, #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
W { Loc } |-> X1 { Loc }
Z { Data } |-> Y1 { Data }
, rest: pto ( X2 { Loc } , Y2 { Data } )
)
, #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
W { Loc } |-> X1 { Loc }
Z { Data } |-> Y1 { Data }
, rest: pto ( X1 { Loc } , Y1 { Data } )
, #matchResult( subst: H0 { Heap } |-> sep ( pto ( X1 { Loc } , Y1 { Data } ) )
W { Loc } |-> X2 { Loc }
Z { Data } |-> Y2 { Data }
, rest: .Patterns
)
// TODO : we need to be getting these results as well
// , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
// W { Loc } |-> X1 { Loc }
// Z { Data } |-> Y1 { Data }
// , rest: pto ( X2 { Loc } , Y2 { Data } )
// )
// , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
// W { Loc } |-> X1 { Loc }
// Z { Data } |-> Y1 { Data }
// , rest: pto ( X1 { Loc } , Y1 { Data } )
// )
, .MatchResults
== #matchAssocComm( terms: pto ( X1 { Loc } , Y1 { Data } )
, pto ( X2 { Loc } , Y2 { Data } )
Expand Down

0 comments on commit 2c3ab94

Please sign in to comment.