From ce98bfa6cbaf901f8dba81fbbabdb339b1f310da Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 10 Jun 2020 11:53:46 -0500 Subject: [PATCH 01/12] matching: match over heap variable --- prover/strategies/matching.md | 53 ++++++++++++++++++++++++++++------- 1 file changed, 43 insertions(+), 10 deletions(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index e9c9a6351..a12a7ee75 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -184,6 +184,7 @@ Recurse over assoc-comm `sep`: , rest: REST ) => #error( "Pattern larger than term" ), .MatchResults + requires notBool P in Vs // Base case: emp matches all heaps rule #matchAssocComm( terms: Ts @@ -195,7 +196,7 @@ Recurse over assoc-comm `sep`: ) => #matchResult(subst: SUBST, rest: REST ++Patterns Ts), .MatchResults -// Base case: If matching a single term, agains an atomic pattern, use Assoc Matching +// Base case: If matching a single term against an atomic pattern, use Assoc Matching rule #matchAssocComm( terms: T, .Patterns , pattern: P, .Patterns , variables: Vs @@ -209,6 +210,7 @@ Recurse over assoc-comm `sep`: , subst: SUBST , rest: REST ) + requires notBool P in Vs ``` Matching an atomic pattern against multiple terms: return a disjunction of the solutions @@ -236,6 +238,7 @@ Matching an atomic pattern against multiple terms: return a disjunction of the s , rest: T, REST ) requires Ts =/=K .Patterns + andBool notBool P in Vs ``` Matching a non-atomic pattern against multiple terms: Match the first @@ -264,6 +267,30 @@ atom in the pattern against any of the terms, and then extend those solutions. ) requires ARGs =/=K .Patterns andBool P_ARGs =/=K .Patterns + andBool notBool P_ARG in Vs +``` + +Base case: If matching a single term against a heap variable, return REST +TODO: if there are multiple heap variables, we need to return all possible partitions. +Currently, the entire REST is constrained to a single heap variable +TODO: other corner cases probably + +```k + rule #matchAssocComm( terms: T, Ts + , pattern: H:Variable, Ps + , variables: Vs + , results: .MatchResults + , subst: SUBST + , rest: REST + ) + => #matchAssocComm( terms: T, Ts + , pattern: Ps + , variables: Vs + , results: .MatchResults + , subst: SUBST H |-> sep(REST) + , rest: .Patterns + ) + requires H in Vs ``` With each returned result, we apply the substitution and continue matching over @@ -271,16 +298,22 @@ the unmatched part of the term: ```k // TODO: don't want to call substUnsafe directly (obviously) - rule #matchAssocComm( terms: Ts => REST - , pattern: P => substPatternsMap(P, SUBST1) - , variables: Vs => Vs -Patterns fst(unzip(SUBST1)) - , results: #matchResult(subst: SUBST1, rest: REST), .MatchResults - => .MatchResults - , subst: SUBST2 - => (SUBST1 SUBST2) - , rest: _ + rule #matchAssocComm( terms: Ts + , pattern: P + , variables: Vs + , results: #matchResult(subst: SUBST_INNER, rest: REST_INNER), .MatchResults + , subst: SUBST + , rest: REST + ) + => #matchAssocComm( terms: REST_INNER + , pattern: substPatternsMap(P, SUBST_INNER) + , variables: Vs -Patterns fst(unzip(SUBST_INNER)) + , results: .MatchResults + , subst: SUBST_INNER SUBST + , rest: REST ) - requires intersectSet(keys(SUBST1), keys(SUBST2)) ==K .Set + requires intersectSet(keys(SUBST_INNER), keys(SUBST)) ==K .Set + andBool notBool P in Vs ``` Failures are propagated: From 449aa2ae58060d2599f9918544a6d1b7ab7630a5 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Tue, 17 Mar 2020 12:24:31 -0500 Subject: [PATCH 02/12] matching: #matchStuck is own sort now, results in stuck configuration if fires --- prover/strategies/matching.md | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index a12a7ee75..df8628fb0 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -56,21 +56,23 @@ module MATCHING-FUNCTIONAL Work around OCaml not producing reasonable error messages: ```k + syntax MatchResult ::= MatchStuck + syntax MatchStuck ::= "#matchStuck" "(" K ")" syntax KItem ::= "\\n" [format(%n)] - rule #matchAssocComm(terms: T - , pattern: P + rule #matchAssocComm( terms: T + , pattern: P , variables: Vs , results: MRs , subst: SUBST , rest: REST ) - => #error( "AC" - ~> "terms:" ~> T - ~> "pattern:" ~> P - ~> "variables:" ~> Vs - ~> "subst:" ~> SUBST - ~> "rest:" ~> REST - ~> "MRs:" ~> MRs ) + => #matchStuck( "AC" + ~> "terms:" ~> T + ~> "pattern:" ~> P + ~> "variables:" ~> Vs + ~> "subst:" ~> SUBST + ~> "rest:" ~> REST + ~> "MRs:" ~> MRs ) , .MatchResults [owise] ``` From 0425b758f40b1669215e1c0aec4c53fd86cd824c Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Tue, 17 Mar 2020 12:25:12 -0500 Subject: [PATCH 03/12] matching: remove spurious side condition in matchAssocComm rule causing rule not to fire --- prover/strategies/matching.md | 1 - 1 file changed, 1 deletion(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index df8628fb0..a3f4ecc8f 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -315,7 +315,6 @@ the unmatched part of the term: , rest: REST ) requires intersectSet(keys(SUBST_INNER), keys(SUBST)) ==K .Set - andBool notBool P in Vs ``` Failures are propagated: From 65a620b6b59a08deaab7345b449cef9cf8d68600 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 11:13:46 -0500 Subject: [PATCH 04/12] kore-lang: getSpatialPatterns and getPredicatePatterns --- prover/lang/kore-lang.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md index 8cb0baba5..6c1d89d6d 100644 --- a/prover/lang/kore-lang.md +++ b/prover/lang/kore-lang.md @@ -798,6 +798,19 @@ Simplifications rule isSpatialPattern(\forall{_} implicationContext(_,_)) => false [owise] + syntax Patterns ::= getSpatialPatterns(Patterns) [function] + rule getSpatialPatterns(.Patterns) => .Patterns + rule getSpatialPatterns(P, Ps) => P, getSpatialPatterns(Ps) + requires isSpatialPattern(P) + rule getSpatialPatterns(P, Ps) => getSpatialPatterns(Ps) + requires notBool isSpatialPattern(P) + + syntax Patterns ::= getPredicatePatterns(Patterns) [function] + rule getPredicatePatterns(.Patterns) => .Patterns + rule getPredicatePatterns(P, Ps) => P, getPredicatePatterns(Ps) + requires isPredicatePattern(P) + rule getPredicatePatterns(P, Ps) => getPredicatePatterns(Ps) + requires notBool isPredicatePattern(P) ``` ```k From 3922c7a6c782395473aa2a2677f8b1dcf6f5a7fd Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 11:16:35 -0500 Subject: [PATCH 05/12] matching: allow multiple heaps in terms --- prover/strategies/matching.md | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index a3f4ecc8f..cdc97851a 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -36,15 +36,24 @@ module MATCHING-FUNCTIONAL rule (MR1, MR1s) ++MatchResults MR2s => MR1, (MR1s ++MatchResults MR2s) rule .MatchResults ++MatchResults MR2s => MR2s + rule #match( terms: \and(sep(H), Hs), pattern: P, variables: Vs ) + => #match( terms: H, pattern: P, variables: Vs ) + ++MatchResults #match( terms: \and(Hs), pattern: P, variables: Vs ) + requires Hs =/=K .Patterns + + rule #match( terms: \and(sep(H), .Patterns), pattern: P, variables: Vs ) + => #match( terms: H, pattern: P, variables: Vs ) + rule #match( terms: T, pattern: P, variables: Vs ) => #filterErrors( #matchAssocComm( terms: T - , pattern: P - , variables: Vs - , results: .MatchResults - , subst: .Map - , rest: .Patterns - ) - ) + , pattern: P + , variables: Vs + , results: .MatchResults + , subst: .Map + , rest: .Patterns + ) + ) + requires isSpatialPattern(sep(T)) syntax MatchResults ::= #filterErrors(MatchResults) [function] rule #filterErrors(MR:Error , MRs) => #filterErrors(MRs) From b52dad9df25d8804622f180d985e58339eaac62b Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 15 Apr 2020 17:05:46 -0500 Subject: [PATCH 06/12] matching with heap variable must be at end of pattern list --- prover/strategies/matching.md | 15 ++--- prover/t/unit/match-assoc-comm.k | 108 +++++++++++++++++++++++++++++++ 2 files changed, 114 insertions(+), 9 deletions(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index cdc97851a..6fbedbc93 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -287,20 +287,17 @@ Currently, the entire REST is constrained to a single heap variable TODO: other corner cases probably ```k - rule #matchAssocComm( terms: T, Ts - , pattern: H:Variable, Ps + rule #matchAssocComm( terms: Ts + , pattern: H:Variable, .Patterns , variables: Vs , results: .MatchResults , subst: SUBST - , rest: REST - ) - => #matchAssocComm( terms: T, Ts - , pattern: Ps - , variables: Vs - , results: .MatchResults - , subst: SUBST H |-> sep(REST) , rest: .Patterns ) + => #matchResult( subst: SUBST H |-> sep(Ts) + , rest: .Patterns + ) + , .MatchResults requires H in Vs ``` diff --git a/prover/t/unit/match-assoc-comm.k b/prover/t/unit/match-assoc-comm.k index 2ecba9bed..1892ec850 100644 --- a/prover/t/unit/match-assoc-comm.k +++ b/prover/t/unit/match-assoc-comm.k @@ -133,4 +133,112 @@ module TEST-MATCH-ASSOC-COMM ) ) .Declarations + + rule test("match-assoc-comm", 9) + => assert( #matchResult( subst: Y2 { Data } |-> Y1 { Data } + H1 { Heap } |-> sep( pto ( X2 { Loc } , c( W1 { Loc } , Z1 { Loc }) ), H0 { Heap } ) + , rest: .Patterns + ) + , .MatchResults + == #filterErrors( #matchAssocComm( terms: H0 { Heap } + , pto ( X1 { Loc } , Y1 { Data } ) + , pto ( X2 { Loc } , c( W1 { Loc } , Z1 { Loc }) ) + , pattern: pto ( X1 { Loc } , Y2 { Data } ) + , H1 { Heap } + , variables: Y2 { Data } + , H1 { Heap } + , results: .MatchResults + , subst: .Map + , rest: .Patterns + ) + ) + ) + .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 } ) + 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 } ) + ) + , .MatchResults + == #matchAssocComm( terms: pto ( X1 { Loc } , Y1 { Data } ) + , pto ( X2 { Loc } , Y2 { Data } ) + , pattern: H0 { Heap } + , pto ( W { Loc } , Z { Data } ) + , variables: H0 { Heap }, W { Loc }, Z { Data } + , results: .MatchResults + , subst: .Map + , rest: .Patterns + ) + ) + .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 } ) + 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 } ) + ) + , .MatchResults + == #matchAssocComm( terms: pto ( X1 { Loc } , Y1 { Data } ) + , pto ( X2 { Loc } , Y2 { Data } ) + , pattern: H0 { Heap } + , pto ( W { Loc } , Z { Data } ) + , variables: H0 { Heap }, W { Loc }, Z { Data } + , results: .MatchResults + , subst: .Map + , rest: .Patterns + ) + ) + .Declarations endmodule From 75911fb41498ee5e8130afc2a8db36e6098cb277 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 11:25:32 -0500 Subject: [PATCH 07/12] match: rotate heap variable when not at end of pattern list --- prover/strategies/matching.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 6fbedbc93..1772e77c8 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -287,6 +287,16 @@ Currently, the entire REST is constrained to a single heap variable TODO: other corner cases probably ```k + rule #matchAssocComm( terms: Ts + , pattern: (H:Variable, P, Ps) + => ((P, Ps) ++Patterns H) + , variables: Vs + , results: .MatchResults + , subst: SUBST + , rest: .Patterns + ) + requires notBool isVariable(P) + rule #matchAssocComm( terms: Ts , pattern: H:Variable, .Patterns , variables: Vs From 9f4b7bb15624636a3027d593ea5049e6b8fab4c7 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 11:26:28 -0500 Subject: [PATCH 08/12] match: lhs can have multiple seps --- prover/strategies/matching.md | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 1772e77c8..bfd18d704 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -417,18 +417,17 @@ The `with-each-match` strategy Instantiate existentials using matching on the spatial part of goals: ```k - rule \implies(\and(sep(LSPATIAL), LHS) , \exists { Vs } \and(sep(RSPATIAL), RHS)) + rule \implies(\and(LHS) , \exists { Vs } \and(sep(RSPATIAL), RHS)) match - => with-each-match(#match( terms: LSPATIAL + => with-each-match(#match( terms: \and(getSpatialPatterns(LHS)) , pattern: RSPATIAL , variables: Vs - ) - , match ) - ... + , match + ) + ... - requires isSpatialPattern(sep(LSPATIAL)) - andBool isSpatialPattern(sep(RSPATIAL)) + requires isSpatialPattern(sep(RSPATIAL)) rule \implies( \and( LSPATIAL, LHS) , \exists { Vs } \and( RHS ) => \exists { Vs -Patterns fst(unzip(SUBST)) } substMap(\and(RHS), SUBST) From 32177c56b1ec6484e8c017822a5fa479622bb798 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 11:27:28 -0500 Subject: [PATCH 09/12] matching: match on multiple heaps on RHS --- prover/strategies/matching.md | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index bfd18d704..914ace2b1 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -428,14 +428,22 @@ Instantiate existentials using matching on the spatial part of goals: ... requires isSpatialPattern(sep(RSPATIAL)) + andBool getFreeVariables(getSpatialPatterns(sep(RSPATIAL), RHS)) intersect Vs =/=K .Patterns + rule \implies(\and(LHS) , \exists { Vs } \and(RHS)) + match => noop ... + requires getFreeVariables(getSpatialPatterns(RHS)) intersect Vs ==K .Patterns rule \implies( \and( LSPATIAL, LHS) - , \exists { Vs } \and( RHS ) - => \exists { Vs -Patterns fst(unzip(SUBST)) } substMap(\and(RHS), SUBST) + , \exists { Vs } \and(sep(RSPATIAL), RHS) + => \exists { Vs -Patterns fst(unzip(SUBST)) } + #flattenAnd(substMap( \and(getSpatialPatterns(RHS) ++Patterns (sep(RSPATIAL), (RHS -Patterns getSpatialPatterns(RHS)))) + , SUBST + ) + ) ) ( #matchResult(subst: SUBST, rest: .Patterns) ~> match ) - => noop - ... + => match + ... rule \implies(LHS, \exists { Vs } \and(RSPATIAL, RHS)) From 65578737b42613e777e2f2394d4c62895de7422e Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:01:41 -0500 Subject: [PATCH 10/12] match-assoc-comm: H1 is a token --- prover/t/unit/match-assoc-comm.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prover/t/unit/match-assoc-comm.k b/prover/t/unit/match-assoc-comm.k index 1892ec850..5ff77d2db 100644 --- a/prover/t/unit/match-assoc-comm.k +++ b/prover/t/unit/match-assoc-comm.k @@ -9,7 +9,7 @@ module TEST-MATCH-ASSOC-COMM | "X0" [token] | "X1" [token] | "X2" [token] | "Y0" [token] | "Y1" [token] | "Y2" [token] | "Z" [token] | "Z1" [token] | "Z2" [token] - | "H0" [token] + | "H0" [token] | "H1" [token] rule test("match-assoc-comm", 1) => assert( #matchResult( subst: .Map , rest: pto( Z { Loc }, W { Data })) From 4d2c0a4373533bf3e44b48d699dc2d3583866905 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 10 Jun 2020 13:32:00 -0500 Subject: [PATCH 11/12] matching: remove extraneous side condition --- prover/strategies/matching.md | 1 - 1 file changed, 1 deletion(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 914ace2b1..5c89c5b0f 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -53,7 +53,6 @@ module MATCHING-FUNCTIONAL , rest: .Patterns ) ) - requires isSpatialPattern(sep(T)) syntax MatchResults ::= #filterErrors(MatchResults) [function] rule #filterErrors(MR:Error , MRs) => #filterErrors(MRs) From 2c3ab94eb4377957e100536e12743812ecb304b2 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 10 Jun 2020 13:32:17 -0500 Subject: [PATCH 12/12] t/unit/match: fix test cases --- prover/t/unit/match-assoc-comm.k | 85 +++++++++++++------------------- 1 file changed, 35 insertions(+), 50 deletions(-) diff --git a/prover/t/unit/match-assoc-comm.k b/prover/t/unit/match-assoc-comm.k index 5ff77d2db..03d580b1f 100644 --- a/prover/t/unit/match-assoc-comm.k +++ b/prover/t/unit/match-assoc-comm.k @@ -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] @@ -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 } ) @@ -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 } )