fix pretty printing of termination measures (#847)

Author: jcp19

src/main/scala/viper/silver/plugin/standard/termination/TerminationASTExtension.scala

@@ -52,7 +52,8 @@ case class DecreasesTuple(tupleExpressions: Seq[Exp] = Nil, override val conditi
 
   override lazy val prettyPrint: PrettyPrintPrimitives#Cont = {
     text("decreases") <>
-      (if (tupleExpressions.nonEmpty) space <> ssep(tupleExpressions map (toParenDoc(_)), char(',') <> space) else nil)
+      (if (tupleExpressions.nonEmpty) space <> ssep(tupleExpressions map (toParenDoc(_)), char(',') <> space) else nil) <>
+      (if (condition.nonEmpty) space <> "if" <+> toParenDoc(condition.get) else nil)
   }
 
   override val extensionSubnodes: Seq[Node] = tupleExpressions ++ condition
@@ -76,7 +77,10 @@ case class DecreasesWildcard(override val condition: Option[Exp] = None)
 
   override val typ: Type = Bool
 
-  override lazy val prettyPrint: PrettyPrintPrimitives#Cont = text("decreases _")
+  override lazy val prettyPrint: PrettyPrintPrimitives#Cont = {
+    text("decreases _") <>
+      (if (condition.nonEmpty) space <> "if" <+> toParenDoc(condition.get) else nil)
+  }
 
   override val extensionSubnodes: Seq[Node] = condition.toSeq
 

src/test/scala/PrettyPrinterTest.scala

@@ -118,5 +118,45 @@ class PrettyPrinterTest extends AnyFunSuite with Matchers {
     assert(origString == resString)
   }
 
+  test("Test pretty printing conditional wildcard termination measures") {
+    import viper.silver.plugin.standard.termination.DecreasesWildcard
+
+    val m = Method(
+      name = "f",
+      formalArgs = Seq.empty,
+      formalReturns = Seq.empty,
+      pres = Seq(DecreasesWildcard(Some(TrueLit()()))()),
+      posts = Seq.empty,
+      body = None
+    )()
+    val actual = m.toString().trim
+    val expected =
+      """
+        |method f()
+        |  decreases _ if true
+        |""".stripMargin.trim
+    assert(actual == expected)
+  }
+
+  test("Test pretty printing conditional tuple termination measures") {
+    import viper.silver.plugin.standard.termination.DecreasesTuple
+
+    val m = Method(
+      name = "f",
+      formalArgs = Seq.empty,
+      formalReturns = Seq.empty,
+      pres = Seq(DecreasesTuple(Seq(IntLit(1)()), Some(TrueLit()()))()),
+      posts = Seq.empty,
+      body = None
+    )()
+    val actual = m.toString().trim
+    val expected =
+      """
+        |method f()
+        |  decreases 1 if true
+        |""".stripMargin.trim
+    assert(actual == expected)
+  }
+
 
 }