Add manual override for package wand

viperproject · Mar 1, 2025 · 063279a · 063279a
1 parent 8a32a03
commit 063279a
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 3 deletions.
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1525,7 +1525,9 @@ case class PFold(fold: PKw.Fold, e: PExp)(val pos: (Position, Position)) extends
 
 case class PUnfold(unfold: PKw.Unfold, e: PExp)(val pos: (Position, Position)) extends PStmt
 
-case class PPackageWand(pckg: PKw.Package, e: PExp, proofScript: Option[PSeqn])(val pos: (Position, Position)) extends PStmt
+case class PPackageWand(pckg: PKw.Package, e: PExp, proofScript: Option[PSeqn])(val pos: (Position, Position)) extends PStmt {
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = show(pckg) <> show(e) <+> showOption(proofScript)
+}
 
 case class PApplyWand(apply: PKw.Apply, e: PExp)(val pos: (Position, Position)) extends PStmt
 

diff --git a/src/test/resources/reformatter/methods.vpr b/src/test/resources/reformatter/methods.vpr
@@ -130,4 +130,10 @@ method empty_assign() {
 }
 
 method with_inhale_exhale(lock: Ref)
-    ensures [true,forperm r: Ref [r.held] :: false]
+    ensures [true,forperm r: Ref [r.held] :: false]
+
+method package_wand(lock: Ref) {
+    package A(p, plvs) --* B{
+        fold acc(Tree(p))
+    }
+}
diff --git a/src/test/resources/reformatter/methods_expected.vpr b/src/test/resources/reformatter/methods_expected.vpr
@@ -134,4 +134,10 @@ method empty_assign() {
 }
 
 method with_inhale_exhale(lock: Ref)
-    ensures [true, forperm r: Ref [r.held] :: false]
+    ensures [true, forperm r: Ref [r.held] :: false]
+
+method package_wand(lock: Ref) {
+    package A(p, plvs) --* B {
+        fold acc(Tree(p))
+    }
+}