From ce98bfa6cbaf901f8dba81fbbabdb339b1f310da Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 10 Jun 2020 11:53:46 -0500 Subject: [PATCH 01/33] 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/33] 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/33] 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/33] 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/33] 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/33] 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/33] 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/33] 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/33] 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/33] 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/33] 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/33] 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 } ) From cf5ff710673334398289de4cbdccd6b30e020f89 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 11:28:16 -0500 Subject: [PATCH 13/33] match: terms can be and(.Patterns) --- prover/strategies/matching.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 5c89c5b0f..80380bf4f 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -44,6 +44,9 @@ module MATCHING-FUNCTIONAL rule #match( terms: \and(sep(H), .Patterns), pattern: P, variables: Vs ) => #match( terms: H, pattern: P, variables: Vs ) + rule #match( terms: \and(.Patterns), pattern: P, variables: Vs ) + => .MatchResults + rule #match( terms: T, pattern: P, variables: Vs ) => #filterErrors( #matchAssocComm( terms: T , pattern: P From 73153f1af3db8b1cc6f15a0a45d6bff91bf7c2f7 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 11:32:14 -0500 Subject: [PATCH 14/33] match-debug --- prover/prover.md | 2 +- prover/strategies/matching.md | 11 +++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/prover/prover.md b/prover/prover.md index b4a241310..eab7a9149 100644 --- a/prover/prover.md +++ b/prover/prover.md @@ -58,7 +58,7 @@ module STRATEGIES-EXPORTED-SYNTAX | "instantiate-universals-with-ground-terms" | "instantiate-separation-logic-axioms" | "spatial-patterns-equal" - | "match" | "match-pto" + | "match" | "match-debug" | "match-pto" | "frame" | "unfold-mut-recs" | "apply-equation" diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 80380bf4f..2e7e52486 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -431,6 +431,17 @@ 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(sep(RSPATIAL), RHS)) + match-debug => wait ... + _ + => #match( terms: \and(getSpatialPatterns(LHS)) + , pattern: RSPATIAL + , variables: Vs + ) + + requires isSpatialPattern(sep(RSPATIAL)) + rule \implies(\and(LHS) , \exists { Vs } \and(RHS)) match => noop ... requires getFreeVariables(getSpatialPatterns(RHS)) intersect Vs ==K .Patterns From 6c196f31fdb01945387c62d2b5957eba31923ff7 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 11:32:53 -0500 Subject: [PATCH 15/33] matching: match: Everything matches \top --- prover/strategies/matching.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 2e7e52486..9a0419986 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -463,8 +463,9 @@ Instantiate existentials using matching on the spatial part of goals: match => fail ... requires isPredicatePattern(LHS) andBool isSpatialPattern(RSPATIAL) + rule \implies(\and(LSPATIAL, LHS), \exists { Vs } RHS) - match => fail ... + match => noop ... requires isPredicatePattern(RHS) andBool isSpatialPattern(LSPATIAL) From 2fb6c9fc56105236f3f3026e2af12b22a8077585 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 11:39:58 -0500 Subject: [PATCH 16/33] matching: allow set variables --- prover/strategies/matching.md | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 9a0419986..6e53e0707 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -143,7 +143,15 @@ Recurse over assoc-only constructors (including `pto`): // ground variable: identical rule #matchAssoc( terms: P:Variable, Ts => Ts - , pattern: P:Variable, Ps => Ps + , pattern: P, Ps => Ps + , variables: Vs + , subst: _ + , rest: REST + ) + requires notBool P in Vs + + rule #matchAssoc( terms: P:SetVariable, Ts => Ts + , pattern: P, Ps => Ps , variables: Vs , subst: _ , rest: REST @@ -160,7 +168,18 @@ Recurse over assoc-only constructors (including `pto`): => #error( "No valid substitution" ), .MatchResults requires T =/=K P andBool notBool P in Vs - + + // ground variable: non-identical + rule #matchAssoc( terms: T, Ts + , pattern: P:SetVariable, Ps + , variables: Vs + , subst: _ + , rest: REST + ) + => #error( "No valid substitution" ), .MatchResults + requires T =/=K P + andBool notBool P in Vs + // free variable: different sorts rule #matchAssoc( terms: T , Ts , pattern: P:Variable, Ps From 9dcda07764f33346a918b30f8b6065b17789b99a Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 11:47:46 -0500 Subject: [PATCH 17/33] matching: begin matching over context patterns --- prover/strategies/matching.md | 13 +++++++++++++ prover/t/unit/match-assoc.k | 16 ++++++++++++++++ 2 files changed, 29 insertions(+) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 6e53e0707..9010f229f 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -91,6 +91,19 @@ Work around OCaml not producing reasonable error messages: Recurse over assoc-only constructors (including `pto`): ```k + // TODO: matching over context patterns + rule #matchAssoc( terms: S:Symbol(T), .Patterns + , pattern: V[T], .Patterns + , variables: Vs + , subst: SUBST + , rest: REST + ) + => #matchResult( subst: SUBST V { getReturnSort(S(T)) } |-> S( #hole { getReturnSort(T) }) + , rest: .Patterns + ) + , .MatchResults + requires V { getReturnSort(S(T)) } in Vs + // Base case rule #matchAssoc( terms: .Patterns , pattern: .Patterns diff --git a/prover/t/unit/match-assoc.k b/prover/t/unit/match-assoc.k index 6696afbb9..1d52f5dd4 100644 --- a/prover/t/unit/match-assoc.k +++ b/prover/t/unit/match-assoc.k @@ -110,6 +110,7 @@ module TEST-MATCH-ASSOC // Match constructor against variable rule test("match-assoc", 9) => symbol pto ( Loc, Data ) : Heap + symbol c ( Data ) : Data assert( #error("Constructors do not match") , .MatchResults == #matchAssoc( terms: X0 { Loc }, Y0 { Data } @@ -120,4 +121,19 @@ module TEST-MATCH-ASSOC ) ) .Declarations + // Match multiple occurances of a variable + rule test("match-assoc", 10) + => symbol c ( Data ) : Data + assert( #matchResult( subst: X0 |-> c( #hole { Data } ) + , rest: .Patterns + ) + , .MatchResults + == #matchAssoc( terms: c( W { Data } ) + , pattern: X0[W { Data }] + , variables: X0 { Data } + , subst: .Map + , rest: .Patterns + ) + ) + .Declarations endmodule From 4801d968ef8fb17bfd53f612bb484d5533e66c22 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:01:15 -0500 Subject: [PATCH 18/33] kore-lang: add Context sort --- prover/lang/kore-lang.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md index 6c1d89d6d..8c6632f36 100644 --- a/prover/lang/kore-lang.md +++ b/prover/lang/kore-lang.md @@ -140,12 +140,15 @@ only in this scenario*. ```k syntax Variable ::= VariableName "{" Sort "}" [klabel(sortedVariable)] syntax SetVariable ::= SharpName [klabel(setVariable)] + syntax Context ::= VariableName "[" Pattern "]" [klabel(context)] syntax Pattern ::= Int | Variable | SetVariable | Symbol | Symbol "(" Patterns ")" [klabel(apply)] + | Context + | "\\top" "(" ")" [klabel(top)] | "\\bottom" "(" ")" [klabel(bottom)] | "\\equals" "(" Pattern "," Pattern ")" [klabel(equals)] From 0efa47ec05d2a27d11126c853a19e335d4464b0d Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:01:29 -0500 Subject: [PATCH 19/33] matching: hole not parameterized --- prover/strategies/matching.md | 2 +- prover/t/unit/match-assoc.k | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 9010f229f..a89067973 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -98,7 +98,7 @@ Recurse over assoc-only constructors (including `pto`): , subst: SUBST , rest: REST ) - => #matchResult( subst: SUBST V { getReturnSort(S(T)) } |-> S( #hole { getReturnSort(T) }) + => #matchResult( subst: SUBST V { getReturnSort(S(T)) } |-> S( #hole ) , rest: .Patterns ) , .MatchResults diff --git a/prover/t/unit/match-assoc.k b/prover/t/unit/match-assoc.k index 1d52f5dd4..f4139ed83 100644 --- a/prover/t/unit/match-assoc.k +++ b/prover/t/unit/match-assoc.k @@ -124,7 +124,7 @@ module TEST-MATCH-ASSOC // Match multiple occurances of a variable rule test("match-assoc", 10) => symbol c ( Data ) : Data - assert( #matchResult( subst: X0 |-> c( #hole { Data } ) + assert( #matchResult( subst: X0 |-> c( #hole ) , rest: .Patterns ) , .MatchResults From 20ad3676d496dbef86bec9656fc762379409eaf3 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:02:49 -0500 Subject: [PATCH 20/33] matching: #match: Fix missing side condition --- prover/strategies/matching.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index a89067973..6ddbcac30 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -56,7 +56,7 @@ module MATCHING-FUNCTIONAL , rest: .Patterns ) ) - + requires isSpatialPattern(sep(T)) syntax MatchResults ::= #filterErrors(MatchResults) [function] rule #filterErrors(MR:Error , MRs) => #filterErrors(MRs) rule #filterErrors(MR , MRs) => MR , #filterErrors(MRs) From ef208facfdfc76d0cb8696c2dc5a2e970a8677ee Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:17:20 -0500 Subject: [PATCH 21/33] kore-lang: add syntax for mu --- prover/lang/kore-lang.md | 1 + 1 file changed, 1 insertion(+) diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md index 8c6632f36..6e9a7a301 100644 --- a/prover/lang/kore-lang.md +++ b/prover/lang/kore-lang.md @@ -161,6 +161,7 @@ only in this scenario*. | "\\exists" "{" Patterns "}" Pattern [klabel(exists)] | "\\forall" "{" Patterns "}" Pattern [klabel(forall)] + | "\\mu" SetVariable "." Pattern [klabel(mu)] /* Sugar for \iff, \mu and application */ | "\\iff-lfp" "(" Pattern "," Pattern ")" [klabel(ifflfp)] From 9e6d79cdd6193e6da71b4714b0ce574d40f21531 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:21:07 -0500 Subject: [PATCH 22/33] matching: recurse over and/or/mu (incorrect for and/or) --- prover/strategies/matching.md | 32 +++++++++++++++++++++++++++++++- 1 file changed, 31 insertions(+), 1 deletion(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 6ddbcac30..1e7e4637e 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -152,7 +152,37 @@ Recurse over assoc-only constructors (including `pto`): , subst: SUBST , rest: REST ) - requires S =/=K sep + + // Recursive over conjunction + rule #matchAssoc( terms: \and(T_ARGs), Ts + => T_ARGs ++Patterns Ts + , pattern: \and(P_ARGs), Ps + => P_ARGs ++Patterns Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + + // Recursive over disjunction + rule #matchAssoc( terms: \or(T_ARGs), Ts + => T_ARGs ++Patterns Ts + , pattern: \or(P_ARGs), Ps + => P_ARGs ++Patterns Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + + // Both term and pattern are a mu: + // Recurse over pattern with same fresh variable for each mu term + rule #matchAssoc( terms: (\mu X . T), Ts + => subst(T, X, !F:SetVariable), Ts + , pattern: (\mu Y . P), Ps + => subst(P, Y, !F), Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) // ground variable: identical rule #matchAssoc( terms: P:Variable, Ts => Ts From 119ad56a987442b5c34d83c3149b8f833eaf23e3 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:22:03 -0500 Subject: [PATCH 23/33] match-assoc-comm: mu test --- prover/t/unit/match-assoc-comm.k | 34 +++++++++++++++++++++++--------- 1 file changed, 25 insertions(+), 9 deletions(-) diff --git a/prover/t/unit/match-assoc-comm.k b/prover/t/unit/match-assoc-comm.k index 03d580b1f..6d85ce910 100644 --- a/prover/t/unit/match-assoc-comm.k +++ b/prover/t/unit/match-assoc-comm.k @@ -1,15 +1,17 @@ module TEST-MATCH-ASSOC-COMM imports UNIT-TEST - syntax LowerName ::= "c" [token] - | "d" [token] - syntax UpperName ::= "Data" [token] - | "Loc" [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] - | "H0" [token] | "H1" [token] + syntax LowerName ::= "c" [token] + | "d" [token] + syntax UpperName ::= "Data" [token] + | "Loc" [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] + | "H0" [token] | "H1" [token] + syntax SharpName ::= "#X0" [token] | "#X1" [token] + | "#PHI1" [token] rule test("match-assoc-comm", 1) => assert( #matchResult( subst: .Map , rest: pto( Z { Loc }, W { Data })) @@ -226,4 +228,18 @@ module TEST-MATCH-ASSOC-COMM ) ) .Declarations + + // matching on mu terms with different binders + rule test("match-assoc-comm", 13) + => assert( #matchResult( subst: .Map , rest: .Patterns ) + , .MatchResults + == #matchAssocComm( terms: \mu #X0 . \and(#X0, #PHI1) + , pattern: \mu #X1 . \and(#X1, #PHI1) + , variables: .Patterns + , results: .MatchResults + , subst: .Map + , rest: .Patterns + ) + ) + .Declarations endmodule From 7e3860b5662eb14a9b83c1530d9199cd377019ac Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:31:13 -0500 Subject: [PATCH 24/33] matching: owise case instead of requiring spatial pattern for more general matching --- prover/strategies/matching.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 1e7e4637e..0dcfc27af 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -56,7 +56,8 @@ module MATCHING-FUNCTIONAL , rest: .Patterns ) ) - requires isSpatialPattern(sep(T)) + [owise] + // requires isSpatialPattern(sep(T)) syntax MatchResults ::= #filterErrors(MatchResults) [function] rule #filterErrors(MR:Error , MRs) => #filterErrors(MRs) rule #filterErrors(MR , MRs) => MR , #filterErrors(MRs) From 582f3066ebbcbd8e2e02c2ab065f63a3588a776f Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:34:29 -0500 Subject: [PATCH 25/33] match: recurse over exists --- prover/strategies/matching.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 0dcfc27af..8eb4b3a47 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -174,6 +174,16 @@ Recurse over assoc-only constructors (including `pto`): , rest: REST ) + // Recursive over exists + rule #matchAssoc( terms: \exists { .Patterns } T, Ts + => T, Ts + , pattern: \exists { .Patterns } P, Ps + => P, Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + // Both term and pattern are a mu: // Recurse over pattern with same fresh variable for each mu term rule #matchAssoc( terms: (\mu X . T), Ts From 4a7605a4e551155604415671c3b5863b1d494c7c Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:36:14 -0500 Subject: [PATCH 26/33] unit/match-assoc-comm: change test name --- 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 6d85ce910..7ce3ce84a 100644 --- a/prover/t/unit/match-assoc-comm.k +++ b/prover/t/unit/match-assoc-comm.k @@ -230,7 +230,7 @@ module TEST-MATCH-ASSOC-COMM .Declarations // matching on mu terms with different binders - rule test("match-assoc-comm", 13) + rule test("match-assoc-comm", 14) => assert( #matchResult( subst: .Map , rest: .Patterns ) , .MatchResults == #matchAssocComm( terms: \mu #X0 . \and(#X0, #PHI1) From d1b03590af5a6725aaf2042f2a5cd5fb01d79c97 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:42:14 -0500 Subject: [PATCH 27/33] unit/match-assoc-comm: add test 13 --- prover/t/unit/match-assoc-comm.k | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/prover/t/unit/match-assoc-comm.k b/prover/t/unit/match-assoc-comm.k index 7ce3ce84a..013766871 100644 --- a/prover/t/unit/match-assoc-comm.k +++ b/prover/t/unit/match-assoc-comm.k @@ -229,6 +229,18 @@ module TEST-MATCH-ASSOC-COMM ) .Declarations + rule test("match-assoc-comm", 13) + => assert( #error( "???" ), .MatchResults + == #match( terms: \and(sep( pto ( Y0 { Loc } , c ( Z { Loc })) + , pto ( X0 { Loc } , c ( Y0 { Loc })) + ) ) + , pattern: pto ( X0 { Loc } , c ( W0 { Loc })) + , pto ( W0 { Loc } , c ( Z { Loc })) + , variables: W0 { Loc } + ) + ) + .Declarations + // matching on mu terms with different binders rule test("match-assoc-comm", 14) => assert( #matchResult( subst: .Map , rest: .Patterns ) @@ -240,6 +252,6 @@ module TEST-MATCH-ASSOC-COMM , subst: .Map , rest: .Patterns ) - ) + ) .Declarations endmodule From bcf3e055d33bceaa46e4f62e8ab611c77fc0397d Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:45:53 -0500 Subject: [PATCH 28/33] matching: fix preprocessing --- prover/strategies/matching.md | 37 +++++++++++++++++++++++------------ 1 file changed, 24 insertions(+), 13 deletions(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 8eb4b3a47..4106b9b54 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -36,28 +36,37 @@ 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: \and(.Patterns), pattern: P, variables: Vs ) + rule #match( terms: \and(T, Ts), pattern: P, variables: Vs ) + => #match( terms: T, pattern: P, variables: Vs ) + ++MatchResults #match( terms: \and(Ts), pattern: P, variables: Vs ) + requires \and(_) :/=K P + rule #match( terms: \and(T, .Patterns), pattern: P, variables: Vs ) + => #match( terms: T, pattern: P, variables: Vs ) + requires \and(_) :/=K P + rule #match( terms: \and(.Patterns), pattern: P, variables: Vs ) => .MatchResults + requires \and(_) :/=K P - rule #match( terms: T, pattern: P, variables: Vs ) - => #filterErrors( #matchAssocComm( terms: T - , pattern: P + rule #match( terms: sep(Ts), pattern: sep(Ps), variables: Vs ) + => #filterErrors( #matchAssocComm( terms: Ts + , pattern: Ps , variables: Vs , results: .MatchResults , subst: .Map , rest: .Patterns ) ) + + rule #match( terms: Ts, pattern: Ps, variables: Vs ) + => #filterErrors( #matchAssoc( terms: Ts + , pattern: Ps + , variables: Vs + , subst: .Map + , rest: .Patterns + ) + ) [owise] - // requires isSpatialPattern(sep(T)) + syntax MatchResults ::= #filterErrors(MatchResults) [function] rule #filterErrors(MR:Error , MRs) => #filterErrors(MRs) rule #filterErrors(MR , MRs) => MR , #filterErrors(MRs) @@ -153,7 +162,9 @@ Recurse over assoc-only constructors (including `pto`): , subst: SUBST , rest: REST ) + requires S =/=K sep + // TODO: the conjunction/disjunction matching rules should be more general, i.e. aware of commutativity // Recursive over conjunction rule #matchAssoc( terms: \and(T_ARGs), Ts => T_ARGs ++Patterns Ts From 5aa40f77ce73fd6503163253764313d29b41e53a Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:48:30 -0500 Subject: [PATCH 29/33] kore-lang: add syntax for nu --- prover/lang/kore-lang.md | 1 + 1 file changed, 1 insertion(+) diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md index 6e9a7a301..035b72a11 100644 --- a/prover/lang/kore-lang.md +++ b/prover/lang/kore-lang.md @@ -162,6 +162,7 @@ only in this scenario*. | "\\forall" "{" Patterns "}" Pattern [klabel(forall)] | "\\mu" SetVariable "." Pattern [klabel(mu)] + | "\\nu" SetVariable "." Pattern [klabel(mu)] /* Sugar for \iff, \mu and application */ | "\\iff-lfp" "(" Pattern "," Pattern ")" [klabel(ifflfp)] From 3795bd880cca8da5aca3a2a6e004cd40f505a451 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:50:51 -0500 Subject: [PATCH 30/33] matching: both term and pattern are nu --- prover/strategies/matching.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 4106b9b54..04c726f50 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -206,6 +206,17 @@ Recurse over assoc-only constructors (including `pto`): , rest: REST ) + // Both term and pattern are a nu: + // Recurse over pattern with same fresh variable for each nu term + rule #matchAssoc( terms: (\nu X . T), Ts + => subst(T, X, !F:SetVariable), Ts + , pattern: (\nu Y . P), Ps + => subst(P, Y, !F), Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + // ground variable: identical rule #matchAssoc( terms: P:Variable, Ts => Ts , pattern: P, Ps => Ps From 618dedc4ca41e93d14dd3ea92c5327272a10c7ba Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:52:38 -0500 Subject: [PATCH 31/33] matching: #matchAssoc: Syntactically match on `\not` --- prover/strategies/matching.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 04c726f50..5bc4f2f80 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -164,6 +164,15 @@ Recurse over assoc-only constructors (including `pto`): ) requires S =/=K sep + rule #matchAssoc( terms: \not(T), Ts + => T, Ts + , pattern: \not(P), Ps + => P, Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + // TODO: the conjunction/disjunction matching rules should be more general, i.e. aware of commutativity // Recursive over conjunction rule #matchAssoc( terms: \and(T_ARGs), Ts From 9d1f267e41859b815127454adc1df2026eaf3b0b Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 3 Jun 2020 12:54:07 -0500 Subject: [PATCH 32/33] matching: #matchAssoc: Patterns may use set variables too --- prover/strategies/matching.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 5bc4f2f80..34a723869 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -243,26 +243,27 @@ Recurse over assoc-only constructors (including `pto`): ) requires notBool P in Vs - // ground variable: non-identical rule #matchAssoc( terms: T, Ts - , pattern: P:Variable, Ps + , pattern: P, Ps , variables: Vs , subst: _ , rest: REST ) - => #error( "No valid substitution" ), .MatchResults + => #error("Ground term does not match") requires T =/=K P + andBool (isSetVariable(T) orBool isVariable(T)) andBool notBool P in Vs // ground variable: non-identical rule #matchAssoc( terms: T, Ts - , pattern: P:SetVariable, Ps + , pattern: P, Ps , variables: Vs , subst: _ , rest: REST ) => #error( "No valid substitution" ), .MatchResults requires T =/=K P + andBool (isSetVariable(P) orBool isVariable(P)) andBool notBool P in Vs // free variable: different sorts @@ -799,4 +800,3 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil ```k endmodule ``` - From e2385f25991c280cdb937972cdde8229170268a0 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Tue, 9 Jun 2020 14:02:32 -0500 Subject: [PATCH 33/33] match: fix test cases --- prover/t/unit/match-assoc-comm.k | 14 +++++++++----- prover/t/unit/match-assoc.k | 2 +- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/prover/t/unit/match-assoc-comm.k b/prover/t/unit/match-assoc-comm.k index 013766871..440fc360d 100644 --- a/prover/t/unit/match-assoc-comm.k +++ b/prover/t/unit/match-assoc-comm.k @@ -229,20 +229,24 @@ module TEST-MATCH-ASSOC-COMM ) .Declarations - rule test("match-assoc-comm", 13) - => assert( #error( "???" ), .MatchResults + rule test("match-assoc-comm", 12) + => assert( #matchResult( subst: W0 { Loc } |-> Y0 { Loc } + , rest: .Patterns + ) + , .MatchResults == #match( terms: \and(sep( pto ( Y0 { Loc } , c ( Z { Loc })) , pto ( X0 { Loc } , c ( Y0 { Loc })) ) ) - , pattern: pto ( X0 { Loc } , c ( W0 { Loc })) - , pto ( W0 { Loc } , c ( Z { Loc })) + , pattern: sep ( pto ( X0 { Loc } , c ( W0 { Loc })) + , pto ( W0 { Loc } , c ( Z { Loc })) + ) , variables: W0 { Loc } ) ) .Declarations // matching on mu terms with different binders - rule test("match-assoc-comm", 14) + rule test("match-assoc-comm", 13) => assert( #matchResult( subst: .Map , rest: .Patterns ) , .MatchResults == #matchAssocComm( terms: \mu #X0 . \and(#X0, #PHI1) diff --git a/prover/t/unit/match-assoc.k b/prover/t/unit/match-assoc.k index f4139ed83..bbd358345 100644 --- a/prover/t/unit/match-assoc.k +++ b/prover/t/unit/match-assoc.k @@ -124,7 +124,7 @@ module TEST-MATCH-ASSOC // Match multiple occurances of a variable rule test("match-assoc", 10) => symbol c ( Data ) : Data - assert( #matchResult( subst: X0 |-> c( #hole ) + assert( #matchResult( subst: X0 { Data } |-> c( #hole ) , rest: .Patterns ) , .MatchResults