more wip on until implies eventually

Author: lucaspena

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)

prover/strategies/knaster-tarski.md

@@ -384,7 +384,9 @@ Move #holes to the front
 ```
 
 ```k
-  rule <k> \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { SORT }, _) , _ ) , _ ) , _ ) </k>
+  rule <k> \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { Bool }, _) , _ ) , _ ) , _ ) </k>
+       <strategy> normalize-implication-context => noop ... </strategy>
+  rule <k> \implies(\and( S:Symbol(\forall { UNIVs } implicationContext( \and(#hole { TopSort }, _) , _ )) , _ ) , _ ) </k>
        <strategy> normalize-implication-context => noop ... </strategy>
   rule <k> \implies(\and( sep(\forall { UNIVs } implicationContext( \and(sep(#hole { Heap }, _), _) , _ ) , _ ), _ ), _ ) </k>
        <strategy> normalize-implication-context => noop ... </strategy>
@@ -496,6 +498,50 @@ of heaps.
        </strategy>
 ```
 
+```k
+  syntax UpperName ::= "#rest" [token]
+  rule <k> \implies( \and( S:Symbol ( \forall { UNIVs }
+                                      implicationContext(\and(CTXLHS), CTXRHS)
+                                    )
+                         , LHS:Patterns
+                         )
+                   , RHS:Pattern
+                   )
+       </k>
+       <strategy> 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
+                                 )
+                  ...
+       </strategy>
+```
+
+```k
+  rule <k> \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
+                    )
+       </k>
+       <strategy> ( #matchResult(subst: SUBST, rest: .Patterns) ~> kt-collapse )
+               => noop
+                  ...
+       </strategy>
+```
+
 In the context of the heuristics we implement, this becomes the following, where
 REST is obtained via matching:
 

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

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)

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 )
+                          )

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