Pass over everthing that contained location

sakehl · Jan 10, 2024 · 9fcc7a6 · 9fcc7a6
1 parent 2041586
commit 9fcc7a6
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 3 deletions.
diff --git a/src/rewrite/vct/rewrite/InlineApplicables.scala b/src/rewrite/vct/rewrite/InlineApplicables.scala
@@ -261,6 +261,14 @@ case class InlineApplicables[Pre <: Generation]() extends Rewriter[Pre] with Laz
     case Perm(loc @ InstancePredicateLocation(pred, obj, args), WritePerm()) if pred.decl.inline =>
       dispatch(InstancePredicateApply(obj, pred, args, WritePerm()(loc.o))(loc.o))
 
+    case Perm(InLinePatternLocation(loc @ PredicateLocation(pred, args), pat), WritePerm()) if pred.decl.inline =>
+      dispatch(PredicateApply(pred, args, WritePerm()(loc.o))(loc.o))
+//      TODO: Or should I do:
+//      dispatch(InlinePattern(PredicateApply(pred, args, WritePerm()(loc.o))(loc.o))(loc.o))
+
+    case Perm(InLinePatternLocation(loc @ InstancePredicateLocation(pred, obj, args), pat), WritePerm()) if pred.decl.inline =>
+      dispatch(InstancePredicateApply(obj, pred, args, WritePerm()(loc.o))(loc.o))
+
     case other => rewriteDefault(other)
   }
 }
diff --git a/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala b/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala
@@ -62,9 +62,9 @@ case class SimplifyNestedQuantifiers[Pre <: Generation]() extends Rewriter[Pre]
           case None =>
             val res = rewriteDefault(e)
             res match {
-              case Starall(_, Nil, body) if !body.exists { case InlinePattern(_, _, _) => true } =>
+              case Starall(_, Nil, body) if !body.exists { case InlinePattern(_, _, _) | InLinePatternLocation(_, _) => true} =>
                 logger.warn(f"The binder `${e.toInlineString}` contains no triggers")
-              case Forall(_, Nil, body) if !body.exists { case InlinePattern(_, _, _) => true } =>
+              case Forall(_, Nil, body) if !body.exists { case InlinePattern(_, _, _) | InLinePatternLocation(_, _) => true } =>
                 logger.warn(f"The binder `${e.toInlineString}` contains no triggers")
               case _ =>
             }
@@ -150,7 +150,7 @@ case class SimplifyNestedQuantifiers[Pre <: Generation]() extends Rewriter[Pre]
     if (e.bindings.exists(_.t != TInt())) return None
 
     // PB: do not attempt to reshape quantifiers that already have patterns
-    if (originalBody.exists { case _: InlinePattern[Pre] => true }) {
+    if (originalBody.exists { case InlinePattern(_, _, _) | InLinePatternLocation(_, _) => true }) {
       logger.debug(s"Not rewriting $e because it contains patterns")
       return None
     }