Skip to content

Commit 8939328

Browse files
lucaspenanishantjr
lucaspena
authored and
nishantjr
committed
more wip on until implies eventually
1 parent b40b25e commit 8939328

File tree

7 files changed

+107
-22
lines changed

7 files changed

+107
-22
lines changed

‎prover/lang/kore-lang.md‎

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -141,12 +141,15 @@ only in this scenario*.
141141
```k
142142
syntax Variable ::= VariableName "{" Sort "}" [klabel(sortedVariable)]
143143
syntax SetVariable ::= SharpName [klabel(setVariable)]
144+
syntax Context ::= VariableName "[" Pattern "]" [klabel(context)]
144145
syntax Pattern ::= Int
145146
| Variable
146147
| SetVariable
147148
| Symbol
148149
| Symbol "(" Patterns ")" [klabel(apply)]
149150
151+
| Context
152+
150153
| "\\top" "(" ")" [klabel(top)]
151154
| "\\bottom" "(" ")" [klabel(bottom)]
152155
| "\\equals" "(" Pattern "," Pattern ")" [klabel(equals)]
@@ -359,8 +362,8 @@ module KORE-HELPERS
359362
360363
rule getReturnSort(\exists{Vs} P) => getReturnSort(P)
361364
362-
syntax Sort ::= "TopSort" [token]
363-
| "BottomSort" [token]
365+
syntax UpperName ::= "TopSort" [token]
366+
| "BottomSort" [token]
364367
365368
syntax Sort ::= unionSort(Sort, Sort) [function]
366369
rule unionSort(TopSort, S) => TopSort
@@ -833,10 +836,10 @@ Simplifications
833836
834837
// TODO: This should use an axiom, similar to `functional` instead: `axiom predicate(P)`
835838
rule isPredicatePattern(S:Symbol(ARGS)) => true
836-
requires getReturnSort(S(ARGS)) =/=K Heap
839+
requires getReturnSort(S(ARGS)) ==K Bool
837840
838841
rule isPredicatePattern(S:Symbol(ARGS)) => false
839-
requires getReturnSort(S(ARGS)) ==K Heap
842+
requires getReturnSort(S(ARGS)) =/=K Bool
840843
rule isPredicatePattern(emp(.Patterns)) => false
841844
rule isPredicatePattern(\exists{Vs} P) => isPredicatePattern(P)
842845
rule isPredicatePattern(\forall{Vs} P) => isPredicatePattern(P)
@@ -857,6 +860,8 @@ Simplifications
857860
rule isSpatialPattern(\or(_)) => false
858861
rule isSpatialPattern(S:Symbol(ARGS)) => true
859862
requires S =/=K sep andBool getReturnSort(S(ARGS)) ==K Heap
863+
rule isSpatialPattern(S:Symbol(ARGS)) => false
864+
requires getReturnSort(S(ARGS)) =/=K Heap
860865
rule isSpatialPattern(#hole { Bool }) => false
861866
rule isSpatialPattern(#hole { Heap }) => true
862867
rule isSpatialPattern(V:VariableName { Heap }) => true
@@ -918,6 +923,7 @@ Simplifications
918923
rule hasImplicationContext(\functionalPattern(P)) => hasImplicationContext(P)
919924
rule hasImplicationContext(\exists{ _ } P ) => hasImplicationContext(P)
920925
rule hasImplicationContext(\forall{ _ } P ) => hasImplicationContext(P)
926+
rule hasImplicationContext(\mu X . P) => hasImplicationContext(P)
921927
rule hasImplicationContext(implicationContext(_, _)) => true
922928
rule hasImplicationContextPs(.Patterns) => false
923929
rule hasImplicationContextPs(P, Ps)

‎prover/strategies/core.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -290,8 +290,8 @@ Internal strategy used to implement `or-split` and `and-split`.
290290
`rhs-top` evaluates to success if the right hand side is top
291291

292292
```k
293-
rule <k> \implies(LHS, \exists{.Patterns} \and(.Patterns)) </k>
294-
<strategy> rhs-top => success ... </strategy>
293+
rule <claim> \implies(LHS, \exists{.Patterns} \and(.Patterns)) </claim>
294+
<k> rhs-top => success ... </k>
295295
```
296296

297297
If-then-else-fi strategy is useful for implementing other strategies:

‎prover/strategies/knaster-tarski.md‎

Lines changed: 47 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -384,7 +384,9 @@ Move #holes to the front
384384
```
385385

386386
```k
387-
rule <claim> \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { SORT }, _) , _ ) , _ ) , _ ) </claim>
387+
rule <claim> \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { Bool }, _) , _ ) , _ ) , _ ) </claim>
388+
<k> normalize-implication-context => noop ... </k>
389+
rule <claim> \implies(\and( S:Symbol(\forall { UNIVs } implicationContext( \and(#hole { TopSort }, _) , _ )) , _ ) , _ ) </claim>
388390
<k> normalize-implication-context => noop ... </k>
389391
rule <claim> \implies(\and( sep(\forall { UNIVs } implicationContext( \and(sep(#hole { Heap }, _), _) , _ ) , _ ), _ ), _ ) </claim>
390392
<k> normalize-implication-context => noop ... </k>
@@ -496,6 +498,50 @@ of heaps.
496498
</k>
497499
```
498500

501+
```k
502+
syntax UpperName ::= "#rest" [token]
503+
rule <claim> \implies( \and( S:Symbol ( \forall { UNIVs }
504+
implicationContext(\and(CTXLHS), CTXRHS)
505+
)
506+
, LHS:Patterns
507+
)
508+
, RHS:Pattern
509+
)
510+
</claim>
511+
<k> kt-collapse
512+
=> with-each-match( #matchAssoc( terms: S( #hole { TopSort } )
513+
, pattern: #rest[CTXLHS]
514+
, variables: #rest { TopSort }
515+
, subst: .Map
516+
, rest: .Patterns
517+
)
518+
, kt-collapse
519+
, kt-collapse-no-match
520+
)
521+
...
522+
</k>
523+
```
524+
525+
```k
526+
rule <claim> \implies( \and( S:Symbol ( \forall { .Patterns }
527+
implicationContext( \and(_), CTXRHS )
528+
)
529+
, LHS:Patterns
530+
)
531+
, RHS:Pattern
532+
)
533+
=> \implies( \and( subst({SUBST[#rest { TopSort }]}:>Pattern, #hole { TopSort }, CTXRHS)
534+
, LHS
535+
)
536+
, RHS
537+
)
538+
</claim>
539+
<k> ( #matchResult(subst: SUBST, rest: .Patterns) ~> kt-collapse )
540+
=> noop
541+
...
542+
</k>
543+
```
544+
499545
In the context of the heuristics we implement, this becomes the following, where
500546
REST is obtained via matching:
501547

‎prover/strategies/matching.md‎

Lines changed: 27 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,19 @@ Work around OCaml not producing reasonable error messages:
9191
Recurse over assoc-only constructors (including `pto`):
9292

9393
```k
94+
// TODO: matching over context patterns
95+
rule #matchAssoc( terms: S:Symbol(T), .Patterns
96+
, pattern: V[T], .Patterns
97+
, variables: Vs
98+
, subst: SUBST
99+
, rest: REST
100+
)
101+
=> #matchResult( subst: SUBST V { getReturnSort(S(T)) } |-> S( #hole { getReturnSort(T) })
102+
, rest: .Patterns
103+
)
104+
, .MatchResults
105+
requires V { getReturnSort(S(T)) } in Vs
106+
94107
// Base case
95108
rule #matchAssoc( terms: .Patterns
96109
, pattern: .Patterns
@@ -679,37 +692,37 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil
679692
If the RHS is empty, we have nothing to do
680693

681694
```k
682-
rule <k> \implies(LHS, \exists { Vs } \and(.Patterns)) </k>
683-
<strategy> patterns-equal => noop ... </strategy>
695+
rule <claim> \implies(LHS, \exists { Vs } \and(.Patterns)) </claim>
696+
<k> patterns-equal => noop ... </k>
684697
```
685698

686699
Remove any patterns on the RHS that match a pattern on the LHS:
687700

688701
```k
689-
rule <k> \implies(\and(LHS), \exists{Vs} \and(RHS, REST)) </k>
690-
<strategy> patterns-equal
702+
rule <claim> \implies(\and(LHS), \exists{Vs} \and(RHS, REST)) </claim>
703+
<k> patterns-equal
691704
=> with-each-match( #match( terms: LHS
692705
, pattern: RHS
693706
, variables: .Patterns
694707
)
695708
, patterns-equal
696709
)
697710
...
698-
</strategy>
699-
rule <k> \implies(LHS, \exists{ Vs } \and(RHS, REST))
700-
=> \implies(LHS, \exists{ Vs } \and(REST))
701711
</k>
702-
<strategy> #matchResult(subst: .Map , rest: .Patterns)
712+
rule <claim> \implies(LHS, \exists{ Vs } \and(RHS, REST))
713+
=> \implies(LHS, \exists{ Vs } \and(REST))
714+
</claim>
715+
<k> #matchResult(subst: .Map , rest: .Patterns)
703716
~> patterns-equal
704717
=> patterns-equal
705718
...
706-
</strategy>
719+
</k>
707720
708-
rule <strategy> #matchResult(subst: .Map , rest: P, Ps)
709-
~> patterns-equal
710-
=> fail
711-
...
712-
</strategy>
721+
rule <k> #matchResult(subst: .Map , rest: P, Ps)
722+
~> patterns-equal
723+
=> fail
724+
...
725+
</k>
713726
```
714727

715728
If the RHS has no spatial part, then there is nothing to do:

‎prover/strategies/simplification.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -342,6 +342,8 @@ Bring predicate constraints to the top of a term.
342342
343343
syntax Pattern ::= #liftConstraints(Pattern) [function]
344344
syntax Patterns ::= #liftConstraintsPs(Patterns) [function]
345+
// rule #liftConstraints(S:Symbol(\and(P1, P2, Ps), ARGs)) => #liftConstraints(\and(S(P1, ARGs), S(\and(P2, Ps), ARGs)))
346+
// rule #liftConstraints(S:Symbol(\and(P, .Patterns), ARGs)) => #liftConstraints(\and(S(P, ARGs)))
345347
rule #liftConstraints(\and(Ps)) => \and(#liftConstraintsPs(Ps))
346348
rule #liftConstraintsPs(.Patterns) => .Patterns
347349
rule #liftConstraintsPs(sep(\and(.Patterns), .Patterns), REST) => #liftConstraintsPs(REST)

‎prover/t/ltl/until-implies-eventually.kore‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,4 +37,6 @@ right-unfold-Nth(0, 1)
3737
phi-implies-phi
3838
*/
3939

40-
strategy normalize . kt . right-unfold-Nth(0, 0) . normalize . patterns-equal . rhs-top
40+
strategy normalize . kt . ( ( right-unfold-Nth(0, 0) . normalize . patterns-equal . rhs-top )
41+
| ( right-unfold-Nth(0, 1) . normalize . lift-constraints . wait . patterns-equal . rhs-top )
42+
)

‎prover/t/unit/match-assoc.k‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,7 @@ module TEST-MATCH-ASSOC
110110
// Match constructor against variable
111111
rule test("match-assoc", 9)
112112
=> symbol pto ( Loc, Data ) : Heap
113+
symbol c ( Data ) : Data
113114
assert( #error("Constructors do not match")
114115
, .MatchResults
115116
== #matchAssoc( terms: X0 { Loc }, Y0 { Data }
@@ -120,4 +121,19 @@ module TEST-MATCH-ASSOC
120121
)
121122
)
122123
.Declarations
124+
// Match multiple occurances of a variable
125+
rule test("match-assoc", 10)
126+
=> symbol c ( Data ) : Data
127+
assert( #matchResult( subst: X0 |-> c( #hole { Data } )
128+
, rest: .Patterns
129+
)
130+
, .MatchResults
131+
== #matchAssoc( terms: c( W { Data } )
132+
, pattern: X0[W { Data }]
133+
, variables: X0 { Data }
134+
, subst: .Map
135+
, rest: .Patterns
136+
)
137+
)
138+
.Declarations
123139
endmodule

0 commit comments

Comments
 (0)