diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md
index 90168d3f8..5b62b1e9e 100644
--- a/prover/lang/kore-lang.md
+++ b/prover/lang/kore-lang.md
@@ -799,6 +799,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
diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md
index e9c9a6351..5c89c5b0f 100644
--- a/prover/strategies/matching.md
+++ b/prover/strategies/matching.md
@@ -36,15 +36,23 @@ 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
+ )
+ )
syntax MatchResults ::= #filterErrors(MatchResults) [function]
rule #filterErrors(MR:Error , MRs) => #filterErrors(MRs)
@@ -56,21 +64,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]
```
@@ -184,6 +194,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 +206,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 +220,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 +248,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 +277,37 @@ 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: 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
+ , results: .MatchResults
+ , subst: SUBST
+ , rest: .Patterns
+ )
+ => #matchResult( subst: SUBST H |-> sep(Ts)
+ , rest: .Patterns
+ )
+ , .MatchResults
+ requires H in Vs
```
With each returned result, we apply the substitution and continue matching over
@@ -271,16 +315,21 @@ 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
)
- requires intersectSet(keys(SUBST1), keys(SUBST2)) ==K .Set
+ => #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(SUBST_INNER), keys(SUBST)) ==K .Set
```
Failures are propagated:
@@ -367,26 +416,33 @@ 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))
+ 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))
diff --git a/prover/t/unit/match-assoc-comm.k b/prover/t/unit/match-assoc-comm.k
index 2ecba9bed..03d580b1f 100644
--- a/prover/t/unit/match-assoc-comm.k
+++ b/prover/t/unit/match-assoc-comm.k
@@ -5,11 +5,11 @@ 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]
- | "H0" [token]
+ | "H0" [token] | "H1" [token]
rule test("match-assoc-comm", 1)
=> assert( #matchResult( subst: .Map , rest: pto( Z { Loc }, W { Data }))
@@ -133,4 +133,97 @@ 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
+
+ // Matching on a symbolic heap
+ 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 ( 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 } )
+ , 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", 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 ( 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 } )
+ , pattern: H0 { Heap }
+ , pto ( W { Loc } , Z { Data } )
+ , variables: H0 { Heap }, W { Loc }, Z { Data }
+ , results: .MatchResults
+ , subst: .Map
+ , rest: .Patterns
+ )
+ )
+ .Declarations
endmodule