improve support for triggers

actually adds trigger parsing support in forall expressions fixes a bug where empty triggers where generated in the viper code
stg-tud · Jul 4, 2023 · 03fa984 · 03fa984
1 parent 2530067
commit 03fa984
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 6 deletions.
diff --git a/src/main/scala/lore/AST.scala b/src/main/scala/lore/AST.scala
@@ -226,7 +226,7 @@ sealed trait TQuantifier extends TBoolean:
   def body: Term
 case class TForall(
     vars: NonEmptyList[TArgT],
-    triggers: Seq[TViper],
+    triggers: List[NonEmptyList[Term]],
     body: Term,
     sourcePos: Option[SourcePos] = None
 ) extends TQuantifier

diff --git a/src/main/scala/lore/Optics.scala b/src/main/scala/lore/Optics.scala
@@ -117,7 +117,7 @@ given HasChildren[Term] with
       case TFalse(sourcePos)                => List.empty
       case TNeg(body, sourcePos)            => List(body)
       case TForall(vars, triggers, body, sourcePos) =>
-        vars.toList ++ triggers.toList :+ body
+        vars.toList ++ triggers.map(_.toList).flatten :+ body
       case TExists(vars, body, sourcePos)          => vars.toList :+ body
       case TParens(inner, sourcePos)               => List(inner)
       case TString(value, sourcePos)               => List.empty
@@ -177,7 +177,9 @@ val children: Fold[Term, Term] =
         case TInvariant(condition, sourcePos) => f(condition)
         case TNeg(body, sourcePos)            => f(body)
         case TForall(vars, triggers, body, sourcePos) =>
-          Monoid[M].combineAll((vars.toList ++ triggers.toList :+ body).map(f))
+          Monoid[M].combineAll(
+            (vars.toList ++ triggers.map(_.toList).flatten :+ body).map(f)
+          )
         case TExists(vars, body, sourcePos) =>
           Monoid[M].combineAll(((vars.toList :+ body).map(f)))
         case TParens(inner, sourcePos) => f(inner)

diff --git a/src/main/scala/lore/Parser.scala b/src/main/scala/lore/Parser.scala
@@ -251,7 +251,11 @@ object Parser:
   // quantifiers
   val quantifierVars: P[NonEmptyList[TArgT]] =
     (argT).repSep(ws.soft ~ P.char(',') ~ wsOrNl)
-  val triggers: P0[List[TViper]] = P.unit.as(List[TViper]())
+  val trigger: P[NonEmptyList[Term]] =
+    P.char('{') ~ wsOrNl *> inSetFactor.repSep(
+      wsOrNl ~ P.char(',') ~ wsOrNl
+    ) <* wsOrNl ~ P.char('}')
+  val triggers: P0[List[NonEmptyList[Term]]] = trigger.repSep0(wsOrNl)
   val forall: P[TForall] =
     withSourcePos(
       ((P.string("forall") ~ ws *> quantifierVars) <* wsOrNl ~ P.string(

diff --git a/src/main/scala/lore/backends/ViperBackend.scala b/src/main/scala/lore/backends/ViperBackend.scala
@@ -414,10 +414,15 @@ object ViperBackend:
             case f: TForall =>
               (
                 "forall",
-                s"{${f.triggers.map(expressionToViper).mkString(", ")}}"
+                f.triggers
+                  .map(x =>
+                    s"{${x.map(expressionToViper).toList.mkString(", ")}}"
+                  )
+                  .mkString(" ")
+                // s"{${f.triggers.map(expressionToViper).mkString(", ")}}"
               )
             case e: TExists => ("exists", "")
-          s"$keyword $varString :: $triggers ${expressionToViper(t.body)}"
+          s"$keyword $varString ::${if triggers.isEmpty() then "" else " "}$triggers ${expressionToViper(t.body)}"
         case t: TNum    => t.value.toString
         case t: TParens => s"(${expressionToViper(t.inner)})"
         case TFunC(