fix pretty printer for termination measures

viperproject · Jan 10, 2025 · 0dccf35 · 0dccf35
1 parent 56e5d9a
commit 0dccf35
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 9 deletions.
diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
@@ -10,6 +10,7 @@ import scala.language.implicitConversions
 import scala.collection.immutable.Queue
 import scala.collection.immutable.Queue.{empty => emptyDq}
 import viper.silver.ast._
+import viper.silver.plugin.standard.termination.DecreasesClause
 import viper.silver.verifier.DummyNode
 
 import scala.annotation.tailrec
@@ -528,13 +529,17 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       case Field(name, typ) =>
         text("field") <+> name <> ":" <+> show(typ)
       case Method(name, formalArgs, formalReturns, pres, posts, body) =>
+        // for the time being, the termination plugin transforms decreases clauses into preconditions or postconditions
+        val (terminationMeasuresInPres, actualPres) = pres.partition(exp => exp.isInstanceOf[DecreasesClause])
+        val (terminationMeasuresInPosts, actualPosts) = posts.partition(exp => exp.isInstanceOf[DecreasesClause])
         group(text("method") <+> name <> nest(defaultIndent, parens(showVars(formalArgs))) <> {
           if (formalReturns.isEmpty) nil
           else nest(defaultIndent, line <> "returns" <+> parens(showVars(formalReturns)))
         }) <>
           nest(defaultIndent,
-            showContracts("requires", pres) <>
-            showContracts("ensures", posts)
+            showContracts("requires", actualPres) <>
+              showContracts("ensures", actualPosts) <>
+              showDecreasesClauses(terminationMeasuresInPres ++ terminationMeasuresInPosts)
           ) <>
           line <> (
           body match {
@@ -549,11 +554,15 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
           case Some(exp) => braces(nest(defaultIndent, line <> show(exp)) <> line)
         })
       case Function(name, formalArgs, typ, pres, posts, optBody) =>
+        // for the time being, the termination plugin transforms decreases clauses into preconditions or postconditions
+        val (terminationMeasuresInPres, actualPres) = pres.partition(exp => exp.isInstanceOf[DecreasesClause])
+        val (terminationMeasuresInPosts, actualPosts) = posts.partition(exp => exp.isInstanceOf[DecreasesClause])
         text("function") <+> name <> nest(defaultIndent, parens(showVars(formalArgs))) <>
           ":" <+> show(typ) <>
           nest(defaultIndent,
-            showContracts("requires", pres) <>
-              showContracts("ensures", posts)
+            showContracts("requires", actualPres) <>
+              showContracts("ensures", actualPosts) <>
+              showDecreasesClauses(terminationMeasuresInPres ++ terminationMeasuresInPosts)
           ) <>
           line <>
           (optBody match {
@@ -576,6 +585,11 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       lineIfSomeNonEmpty(contracts) <> ssep(contracts.map(c => text(name) <+> nest(defaultIndent, show(c))), line)
   }
 
+  /** Shows a list of termination measures. */
+  def showDecreasesClauses(measures: Seq[Exp]): Cont = {
+      lineIfSomeNonEmpty(measures) <> ssep(measures.map(c => nest(defaultIndent, show(c))), line)
+  }
+
   /** Returns `n` lines if at least one element of `s` is non-empty, and an empty document otherwise. */
   def lineIfSomeNonEmpty[T](s: Seq[T]*)(implicit n: Int = 1) = {
     if (s.forall(e => e != null && e.isEmpty)) nil
@@ -692,11 +706,11 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
           ssep((if (locals == null) Nil else locals map (text("var") <+> showVar(_))) ++ (stmtsToShow map show), line)
         }
       case While(cond, invs, body) =>
+        val (terminationMeasures, actualInvs) = invs.partition(exp => exp.isInstanceOf[DecreasesClause])
         text("while") <+> parens(show(cond)) <>
-          nest(defaultIndent,
-            showContracts("invariant", invs)
-          ) <+> lineIfSomeNonEmpty(invs) <>
-          showBlock(body)
+          nest(defaultIndent, showContracts("invariant", actualInvs) <> showDecreasesClauses(terminationMeasures)) <+>
+            lineIfSomeNonEmpty(invs) <>
+            showBlock(body)
       case If(cond, thn, els) =>
         text("if") <+> parens(show(cond)) <+> showBlock(thn) <> showElse(els)
       case Label(name, invs) =>

diff --git a/.../scala/viper/silver/plugin/standard/predicateinstance/PredicateInstanceASTExtension.scala b/.../scala/viper/silver/plugin/standard/predicateinstance/PredicateInstanceASTExtension.scala
@@ -23,7 +23,7 @@ case class PredicateInstance(p: String, args: Seq[Exp])(override val pos: Positi
   override def verifyExtExp(): VerificationResult = ???
 
   override def prettyPrint: PrettyPrintPrimitives#Cont =
-    text("@") <> text(p) <> parens(ssep(args map show, char (',') <> space))
+    text(p) <> parens(ssep(args map show, char (',') <> space))
 
   override lazy val check: Seq[ConsistencyError] = {
     args.flatMap(Consistency.checkPure)