Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generalize matching #78

Open
wants to merge 33 commits into
base: master
Choose a base branch
from
Open

Generalize matching #78

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
33 commits
Select commit Hold shift + click to select a range
ce98bfa
matching: match over heap variable
lucaspena Jun 10, 2020
449aa2a
matching: #matchStuck is own sort now, results in stuck configuration…
lucaspena Mar 17, 2020
0425b75
matching: remove spurious side condition in matchAssocComm rule causi…
lucaspena Mar 17, 2020
65a620b
kore-lang: getSpatialPatterns and getPredicatePatterns
lucaspena Jun 3, 2020
3922c7a
matching: allow multiple heaps in terms
lucaspena Jun 3, 2020
b52dad9
matching with heap variable must be at end of pattern list
lucaspena Apr 15, 2020
75911fb
match: rotate heap variable when not at end of pattern list
lucaspena Jun 3, 2020
9f4b7bb
match: lhs can have multiple seps
lucaspena Jun 3, 2020
32177c5
matching: match on multiple heaps on RHS
lucaspena Jun 3, 2020
6557873
match-assoc-comm: H1 is a token
lucaspena Jun 3, 2020
4d2c0a4
matching: remove extraneous side condition
lucaspena Jun 10, 2020
2c3ab94
t/unit/match: fix test cases
lucaspena Jun 10, 2020
cf5ff71
match: terms can be and(.Patterns)
lucaspena Jun 3, 2020
73153f1
match-debug
lucaspena Jun 3, 2020
6c196f3
matching: match: Everything matches \top
lucaspena Jun 3, 2020
2fb6c9f
matching: allow set variables
lucaspena Jun 3, 2020
9dcda07
matching: begin matching over context patterns
lucaspena Jun 3, 2020
4801d96
kore-lang: add Context sort
lucaspena Jun 3, 2020
0efa47e
matching: hole not parameterized
lucaspena Jun 3, 2020
20ad367
matching: #match: Fix missing side condition
lucaspena Jun 3, 2020
ef208fa
kore-lang: add syntax for mu
lucaspena Jun 3, 2020
9e6d79c
matching: recurse over and/or/mu (incorrect for and/or)
lucaspena Jun 3, 2020
119ad56
match-assoc-comm: mu test
lucaspena Jun 3, 2020
7e3860b
matching: owise case instead of requiring spatial pattern for more ge…
lucaspena Jun 3, 2020
582f306
match: recurse over exists
lucaspena Jun 3, 2020
4a7605a
unit/match-assoc-comm: change test name
lucaspena Jun 3, 2020
d1b0359
unit/match-assoc-comm: add test 13
lucaspena Jun 3, 2020
bcf3e05
matching: fix preprocessing
lucaspena Jun 3, 2020
5aa40f7
kore-lang: add syntax for nu
lucaspena Jun 3, 2020
3795bd8
matching: both term and pattern are nu
lucaspena Jun 3, 2020
618dedc
matching: #matchAssoc: Syntactically match on `\not`
lucaspena Jun 3, 2020
9d1f267
matching: #matchAssoc: Patterns may use set variables too
lucaspena Jun 3, 2020
e2385f2
match: fix test cases
lucaspena Jun 9, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions prover/lang/kore-lang.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What does this represent? I thought a context is a pattern with a 'hole', which is a variable. So, does VariableName design the variable which plays the role of hole in the Pattern?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, please explain the meaning of VariableName here.

syntax Pattern ::= Int
| Variable
| SetVariable
| Symbol
| Symbol "(" Patterns ")" [klabel(apply)]

| Context

| "\\top" "(" ")" [klabel(top)]
| "\\bottom" "(" ")" [klabel(bottom)]
| "\\equals" "(" Pattern "," Pattern ")" [klabel(equals)]
Expand All @@ -158,6 +161,8 @@ only in this scenario*.
| "\\exists" "{" Patterns "}" Pattern [klabel(exists)]
| "\\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)]

Expand Down Expand Up @@ -798,6 +803,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
Expand Down
2 changes: 1 addition & 1 deletion prover/prover.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
Loading