diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md
index fca9d206d..e15744daa 100644
--- a/prover/lang/kore-lang.md
+++ b/prover/lang/kore-lang.md
@@ -141,12 +141,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)]
@@ -326,8 +329,8 @@ module KORE-HELPERS
rule getReturnSort(\exists{Vs} P) => getReturnSort(P)
- syntax Sort ::= "TopSort" [token]
- | "BottomSort" [token]
+ syntax UpperName ::= "TopSort" [token]
+ | "BottomSort" [token]
syntax Sort ::= unionSort(Sort, Sort) [function]
rule unionSort(TopSort, S) => TopSort
@@ -771,10 +774,10 @@ Simplifications
// TODO: This should use an axiom, similar to `functional` instead: `axiom predicate(P)`
rule isPredicatePattern(S:Symbol(ARGS)) => true
- requires getReturnSort(S(ARGS)) =/=K Heap
+ requires getReturnSort(S(ARGS)) ==K Bool
rule isPredicatePattern(S:Symbol(ARGS)) => false
- requires getReturnSort(S(ARGS)) ==K Heap
+ requires getReturnSort(S(ARGS)) =/=K Bool
rule isPredicatePattern(emp(.Patterns)) => false
rule isPredicatePattern(\exists{Vs} P) => isPredicatePattern(P)
rule isPredicatePattern(\forall{Vs} P) => isPredicatePattern(P)
@@ -795,6 +798,8 @@ Simplifications
rule isSpatialPattern(\or(_)) => false
rule isSpatialPattern(S:Symbol(ARGS)) => true
requires S =/=K sep andBool getReturnSort(S(ARGS)) ==K Heap
+ rule isSpatialPattern(S:Symbol(ARGS)) => false
+ requires getReturnSort(S(ARGS)) =/=K Heap
rule isSpatialPattern(#hole { Bool }) => false
rule isSpatialPattern(#hole { Heap }) => true
rule isSpatialPattern(V:VariableName { Heap }) => true
@@ -856,6 +861,7 @@ Simplifications
rule hasImplicationContext(\functionalPattern(P)) => hasImplicationContext(P)
rule hasImplicationContext(\exists{ _ } P ) => hasImplicationContext(P)
rule hasImplicationContext(\forall{ _ } P ) => hasImplicationContext(P)
+ rule hasImplicationContext(\mu X . P) => hasImplicationContext(P)
rule hasImplicationContext(implicationContext(_, _)) => true
rule hasImplicationContextPs(.Patterns) => false
rule hasImplicationContextPs(P, Ps)
diff --git a/prover/strategies/knaster-tarski.md b/prover/strategies/knaster-tarski.md
index 54908449d..c97f1f0de 100644
--- a/prover/strategies/knaster-tarski.md
+++ b/prover/strategies/knaster-tarski.md
@@ -384,7 +384,9 @@ Move #holes to the front
```
```k
- rule \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { SORT }, _) , _ ) , _ ) , _ )
+ rule \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { Bool }, _) , _ ) , _ ) , _ )
+ normalize-implication-context => noop ...
+ rule \implies(\and( S:Symbol(\forall { UNIVs } implicationContext( \and(#hole { TopSort }, _) , _ )) , _ ) , _ )
normalize-implication-context => noop ...
rule \implies(\and( sep(\forall { UNIVs } implicationContext( \and(sep(#hole { Heap }, _), _) , _ ) , _ ), _ ), _ )
normalize-implication-context => noop ...
@@ -496,6 +498,50 @@ of heaps.
```
+```k
+ syntax UpperName ::= "#rest" [token]
+ rule \implies( \and( S:Symbol ( \forall { UNIVs }
+ implicationContext(\and(CTXLHS), CTXRHS)
+ )
+ , LHS:Patterns
+ )
+ , RHS:Pattern
+ )
+
+ kt-collapse
+ => with-each-match( #matchAssoc( terms: S( #hole { TopSort } )
+ , pattern: #rest[CTXLHS]
+ , variables: #rest { TopSort }
+ , subst: .Map
+ , rest: .Patterns
+ )
+ , kt-collapse
+ , kt-collapse-no-match
+ )
+ ...
+
+```
+
+```k
+ rule \implies( \and( S:Symbol ( \forall { .Patterns }
+ implicationContext( \and(_), CTXRHS )
+ )
+ , LHS:Patterns
+ )
+ , RHS:Pattern
+ )
+ => \implies( \and( subst({SUBST[#rest { TopSort }]}:>Pattern, #hole { TopSort }, CTXRHS)
+ , LHS
+ )
+ , RHS
+ )
+
+ ( #matchResult(subst: SUBST, rest: .Patterns) ~> kt-collapse )
+ => noop
+ ...
+
+```
+
In the context of the heuristics we implement, this becomes the following, where
REST is obtained via matching:
diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md
index d774fe096..d25fd0a9b 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/strategies/simplification.md b/prover/strategies/simplification.md
index ea4d4116c..72e9fdcba 100644
--- a/prover/strategies/simplification.md
+++ b/prover/strategies/simplification.md
@@ -341,6 +341,8 @@ Bring predicate constraints to the top of a term.
syntax Pattern ::= #liftConstraints(Pattern) [function]
syntax Patterns ::= #liftConstraintsPs(Patterns) [function]
+ // rule #liftConstraints(S:Symbol(\and(P1, P2, Ps), ARGs)) => #liftConstraints(\and(S(P1, ARGs), S(\and(P2, Ps), ARGs)))
+ // rule #liftConstraints(S:Symbol(\and(P, .Patterns), ARGs)) => #liftConstraints(\and(S(P, ARGs)))
rule #liftConstraints(\and(Ps)) => \and(#liftConstraintsPs(Ps))
rule #liftConstraintsPs(.Patterns) => .Patterns
rule #liftConstraintsPs(sep(\and(.Patterns), .Patterns), REST) => #liftConstraintsPs(REST)
diff --git a/prover/t/ltl/until-implies-eventually.kore b/prover/t/ltl/until-implies-eventually.kore
index 9dd34b605..d1cc74b68 100644
--- a/prover/t/ltl/until-implies-eventually.kore
+++ b/prover/t/ltl/until-implies-eventually.kore
@@ -37,4 +37,6 @@ right-unfold-Nth(0, 1)
phi-implies-phi
*/
-strategy normalize . kt . right-unfold-Nth(0, 0) . normalize . patterns-equal . rhs-top
+strategy normalize . kt . ( ( right-unfold-Nth(0, 0) . normalize . patterns-equal . rhs-top )
+ | ( right-unfold-Nth(0, 1) . normalize . lift-constraints . wait . patterns-equal . rhs-top )
+ )
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