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.

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
Changes from 1 commit
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
Prev Previous commit
match: fix test cases
lucaspena committed Jun 17, 2020
commit e2385f25991c280cdb937972cdde8229170268a0
14 changes: 9 additions & 5 deletions prover/t/unit/match-assoc-comm.k
Original file line number Diff line number Diff line change
@@ -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)
2 changes: 1 addition & 1 deletion prover/t/unit/match-assoc.k
Original file line number Diff line number Diff line change
@@ -124,7 +124,7 @@ module TEST-MATCH-ASSOC
// Match multiple occurances of a variable
rule test("match-assoc", 10)
=> symbol c ( Data ) : Data
Copy link
Collaborator

Choose a reason for hiding this comment

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

How does this work? I thought that #matchAssoc, which is a function, is evaluated before the symbol declaration.

assert( #matchResult( subst: X0 |-> c( #hole )
assert( #matchResult( subst: X0 { Data } |-> c( #hole )
, rest: .Patterns
)
, .MatchResults