Redo pretty-printing

src/col/vct/col/ast/Node.scala

@@ -15,7 +15,7 @@ import vct.col.ast.expr.`type`._
 import vct.col.ast.expr.ambiguous._
 import vct.col.ast.expr.apply._
 import vct.col.ast.expr.binder._
-import vct.col.ast.expr.bip.{BipGuardInvocationImpl, BipLocalIncomingDataImpl, JavaBipGlueImpl}
+import vct.col.ast.expr.bip._
 import vct.col.ast.family.coercion._
 import vct.col.ast.expr.context._
 import vct.col.ast.expr.heap.alloc._
@@ -40,6 +40,7 @@ import vct.col.ast.expr.op.vec._
 import vct.col.ast.expr.resource._
 import vct.col.ast.expr.sideeffect._
 import vct.col.ast.family.accountedpredicate._
+import vct.col.ast.family.bipdata._
 import vct.col.ast.family.catchclause._
 import vct.col.ast.family.coercion._
 import vct.col.ast.family.contract._
@@ -52,6 +53,9 @@ import vct.col.ast.family.location._
 import vct.col.ast.family.loopcontract._
 import vct.col.ast.family.parregion._
 import vct.col.ast.family.signals._
+import vct.col.ast.family.bipglueelement._
+import vct.col.ast.family.bipporttype._
+import vct.col.ast.family.data._
 import vct.col.ast.lang._
 import vct.col.ast.node._
 import vct.col.ast.statement._
@@ -591,7 +595,7 @@ final case class Length[G](arr: Expr[G])(val blame: Blame[ArrayNull])(implicit v
 final case class Size[G](obj: Expr[G])(implicit val o: Origin) extends Expr[G] with SizeImpl[G]
 final case class PointerBlockLength[G](pointer: Expr[G])(val blame: Blame[PointerNull])(implicit val o: Origin) extends Expr[G] with PointerBlockLengthImpl[G]
 final case class PointerBlockOffset[G](pointer: Expr[G])(val blame: Blame[PointerNull])(implicit val o: Origin) extends Expr[G] with PointerBlockOffsetImpl[G]
-final case class PointerLength[G](pointer: Expr[G])(val blame: Blame[PointerNull])(implicit val o: Origin) extends Expr[G] with PointerLengthtImpl[G]
+final case class PointerLength[G](pointer: Expr[G])(val blame: Blame[PointerNull])(implicit val o: Origin) extends Expr[G] with PointerLengthImpl[G]
 final case class SharedMemSize[G](pointer: Expr[G])(implicit val o: Origin) extends Expr[G] with SharedMemSizeImpl[G]
 final case class NdIndex[G](indices: Seq[Expr[G]], dimensions: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with NdIndexImpl[G]
 final case class NdPartialIndex[G](indices: Seq[Expr[G]], linearIndex: Expr[G], dimensions: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with NdPartialIndexImpl[G]
@@ -874,47 +878,47 @@ final case class JavaNewLiteralArray[G](baseType: Type[G], dims: Int, initialize
 final case class JavaNewDefaultArray[G](baseType: Type[G], specifiedDims: Seq[Expr[G]], moreDims: Int)(val blame: Blame[ArraySizeError])(implicit val o: Origin) extends JavaExpr[G] with JavaNewDefaultArrayImpl[G]
 final case class JavaStringValue[G](data: String, t: Type[G])(implicit val o: Origin) extends JavaExpr[G] with JavaStringValueImpl[G]
 
-final class JavaBipGlueContainer[G](val job: Expr[G])(implicit val o: Origin) extends JavaGlobalDeclaration[G]
+final class JavaBipGlueContainer[G](val job: Expr[G])(implicit val o: Origin) extends JavaGlobalDeclaration[G] with JavaBipGlueContainerImpl[G]
 
 final case class JavaBipGlue[G](elems: Seq[JavaBipGlueElement[G]])(val blame: Blame[BipGlueFailure])(implicit val o: Origin) extends JavaExpr[G] with JavaBipGlueImpl[G]
 
-final case class JavaBipGlueName[G](t: Type[G], e: Expr[G])(implicit val o: Origin) extends NodeFamily[G] {
+final case class JavaBipGlueName[G](t: Type[G], e: Expr[G])(implicit val o: Origin) extends NodeFamily[G] with JavaBipGlueNameImpl[G] {
   var data: Option[(JavaClass[G], String)] = None
 }
 sealed trait JavaBipGlueElement[G] extends NodeFamily[G]
-final case class JavaBipGlueRequires[G](port: JavaBipGlueName[G], others: Seq[JavaBipGlueName[G]])(implicit val o: Origin) extends JavaBipGlueElement[G]
-final case class JavaBipGlueAccepts[G](port: JavaBipGlueName[G], others: Seq[JavaBipGlueName[G]])(implicit val o: Origin) extends JavaBipGlueElement[G]
-final case class JavaBipGlueSynchron[G](port0: JavaBipGlueName[G], port1: JavaBipGlueName[G])(implicit val o: Origin) extends JavaBipGlueElement[G]
-final case class JavaBipGlueDataWire[G](dataOut: JavaBipGlueName[G], dataIn: JavaBipGlueName[G])(implicit val o: Origin) extends JavaBipGlueElement[G]
+final case class JavaBipGlueRequires[G](port: JavaBipGlueName[G], others: Seq[JavaBipGlueName[G]])(implicit val o: Origin) extends JavaBipGlueElement[G] with JavaBipGlueRequiresImpl[G]
+final case class JavaBipGlueAccepts[G](port: JavaBipGlueName[G], others: Seq[JavaBipGlueName[G]])(implicit val o: Origin) extends JavaBipGlueElement[G] with JavaBipGlueAcceptsImpl[G]
+final case class JavaBipGlueSynchron[G](port0: JavaBipGlueName[G], port1: JavaBipGlueName[G])(implicit val o: Origin) extends JavaBipGlueElement[G] with JavaBipGlueSynchronImpl[G]
+final case class JavaBipGlueDataWire[G](dataOut: JavaBipGlueName[G], dataIn: JavaBipGlueName[G])(implicit val o: Origin) extends JavaBipGlueElement[G] with JavaBipGlueDataWireImpl[G]
 
 final class BipGlue[G](val requires: Seq[BipGlueRequires[G]], val accepts: Seq[BipGlueAccepts[G]], val dataWires: Seq[BipGlueDataWire[G]])(val blame: Blame[BipGlueFailure])(implicit val o: Origin) extends GlobalDeclaration[G]
-final case class BipGlueRequires[G](port: Ref[G, BipPort[G]], others: Seq[Ref[G, BipPort[G]]])(implicit val o: Origin) extends NodeFamily[G]
-final case class BipGlueAccepts[G](port: Ref[G, BipPort[G]], others: Seq[Ref[G, BipPort[G]]])(implicit val o: Origin) extends NodeFamily[G]
-final case class BipGlueDataWire[G](dataOut: Ref[G, BipOutgoingData[G]], dataIn: Ref[G, BipIncomingData[G]])(implicit val o: Origin) extends NodeFamily[G]
+final case class BipGlueRequires[G](port: Ref[G, BipPort[G]], others: Seq[Ref[G, BipPort[G]]])(implicit val o: Origin) extends NodeFamily[G] with BipGlueRequiresImpl[G]
+final case class BipGlueAccepts[G](port: Ref[G, BipPort[G]], others: Seq[Ref[G, BipPort[G]]])(implicit val o: Origin) extends NodeFamily[G] with BipGlueAcceptsImpl[G]
+final case class BipGlueDataWire[G](dataOut: Ref[G, BipOutgoingData[G]], dataIn: Ref[G, BipIncomingData[G]])(implicit val o: Origin) extends NodeFamily[G] with BipGlueDataWireImpl[G]
 
 sealed trait BipData[G] extends ClassDeclaration[G] with BipDataImpl[G]
-final class BipIncomingData[G](val t: Type[G])(implicit val o: Origin) extends BipData[G]
-final class BipOutgoingData[G](val t: Type[G], val body: Statement[G], val pure: Boolean)(val blame: Blame[CallableFailure])(implicit val o: Origin) extends BipData[G]
+final class BipIncomingData[G](val t: Type[G])(implicit val o: Origin) extends BipData[G] with BipIncomingDataImpl[G]
+final class BipOutgoingData[G](val t: Type[G], val body: Statement[G], val pure: Boolean)(val blame: Blame[CallableFailure])(implicit val o: Origin) extends BipData[G] with BipOutgoingDataImpl[G]
 final case class BipLocalIncomingData[G](ref: Ref[G, BipIncomingData[G]])(implicit val o: Origin) extends Expr[G] with BipLocalIncomingDataImpl[G]
 
-final class BipStatePredicate[G](val expr: Expr[G])(implicit val o: Origin) extends ClassDeclaration[G] { }
+final class BipStatePredicate[G](val expr: Expr[G])(implicit val o: Origin) extends ClassDeclaration[G] with BipStatePredicateImpl[G]
 final case class BipTransitionSignature[G](portName: String, sourceStateName: String, targetStateName: String, textualGuard: Option[String])(implicit val o: Origin) extends NodeFamily[G] with BipTransitionSignatureImpl[G]
 final class BipTransition[G](val signature: BipTransitionSignature[G],
                              val port: Ref[G, BipPort[G]],
                              val source: Ref[G, BipStatePredicate[G]], val target: Ref[G, BipStatePredicate[G]],
                              val data: Seq[Ref[G, BipIncomingData[G]]], val guard: Expr[G],
                              val requires: Expr[G], val ensures: Expr[G], val body: Statement[G]
-                            )(val blame: Blame[BipTransitionFailure])(implicit val o: Origin) extends ClassDeclaration[G]
-final class BipGuard[G](val data: Seq[Ref[G, BipIncomingData[G]]], val body: Statement[G], val pure: Boolean)(val blame: Blame[BipGuardFailure])(implicit val o: Origin) extends ClassDeclaration[G]
+                            )(val blame: Blame[BipTransitionFailure])(implicit val o: Origin) extends ClassDeclaration[G] with BipTransitionImpl[G]
+final class BipGuard[G](val data: Seq[Ref[G, BipIncomingData[G]]], val body: Statement[G], val pure: Boolean)(val blame: Blame[BipGuardFailure])(implicit val o: Origin) extends ClassDeclaration[G] with BipGuardImpl[G]
 final case class BipGuardInvocation[G](obj: Expr[G], guard: Ref[G, BipGuard[G]])(implicit val o: Origin) extends Expr[G] with BipGuardInvocationImpl[G]
 final class BipComponent[G](val fqn: Seq[String], val constructors: Seq[Ref[G, Procedure[G]]], val invariant: Expr[G],
-                            val initial: Ref[G, BipStatePredicate[G]])(implicit val o: Origin) extends ClassDeclaration[G]
+                            val initial: Ref[G, BipStatePredicate[G]])(implicit val o: Origin) extends ClassDeclaration[G] with BipComponentImpl[G]
 
-final class BipPort[G](val t: BipPortType[G])(implicit val o: Origin) extends ClassDeclaration[G]
+final class BipPort[G](val t: BipPortType[G])(implicit val o: Origin) extends ClassDeclaration[G] with BipPortImpl[G]
 sealed trait BipPortType[G] extends NodeFamily[G]
-final case class BipEnforceable[G]()(implicit val o: Origin = DiagnosticOrigin) extends BipPortType[G]
-final case class BipSpontaneous[G]()(implicit val o: Origin = DiagnosticOrigin) extends BipPortType[G]
-final case class BipInternal[G]()(implicit val o: Origin = DiagnosticOrigin) extends BipPortType[G]
+final case class BipEnforceable[G]()(implicit val o: Origin = DiagnosticOrigin) extends BipPortType[G] with BipEnforceableImpl[G]
+final case class BipSpontaneous[G]()(implicit val o: Origin = DiagnosticOrigin) extends BipPortType[G] with BipSpontaneousImpl[G]
+final case class BipInternal[G]()(implicit val o: Origin = DiagnosticOrigin) extends BipPortType[G] with BipInternalImpl[G]
 
 final case class BipPortSynchronization[G](ports: Seq[Ref[G, BipPort[G]]], wires: Seq[BipGlueDataWire[G]])(val blame: Blame[BipSynchronizationFailure])(implicit val o: Origin) extends GlobalDeclaration[G] with BipPortSynchronizationImpl[G]
 final case class BipTransitionSynchronization[G](transitions: Seq[Ref[G, BipTransition[G]]], wires: Seq[BipGlueDataWire[G]])(val blame: Blame[BipSynchronizationFailure])(implicit val o: Origin) extends GlobalDeclaration[G] with BipTransitionSynchronizationImpl[G]

src/col/vct/col/ast/declaration/adt/ADTAxiomImpl.scala

@@ -2,7 +2,13 @@ package vct.col.ast.declaration.adt
 
 import vct.col.ast.{ADTAxiom, TBool}
 import vct.col.check.{CheckContext, CheckError}
+import vct.col.print._
 
 trait ADTAxiomImpl[G] { this: ADTAxiom[G] =>
   override def check(context: CheckContext[G]): Seq[CheckError] = axiom.checkSubType(TBool())
+
+  override def layout(implicit ctx: Ctx): Doc = ctx.syntax match {
+    case Ctx.Silver => Group(Text("axiom") <+> "{" <>> axiom.show <+/> "}")
+    case _ => Text("axiom") <+> axiom
+  }
 }

src/col/vct/col/ast/declaration/adt/ADTFunctionImpl.scala

@@ -2,7 +2,13 @@ package vct.col.ast.declaration.adt
 
 import vct.col.ast.declaration.category.ApplicableImpl
 import vct.col.ast.{ADTFunction, Node}
+import vct.col.print._
 
 trait ADTFunctionImpl[G] extends ApplicableImpl[G] with ADTDeclarationImpl[G] { this: ADTFunction[G] =>
   override def body: Option[Node[G]] = None
+
+  override def layout(implicit ctx: Ctx): Doc = ctx.syntax match {
+    case Ctx.Silver => Group(Text("function") <+> ctx.name(this) <> "(" <> Doc.args(args) <> "):" <+> returnType)
+    case _ => Group(Text("pure") <+> returnType <+> ctx.name (this) <> "(" <> Doc.args(args) <> ");")
+  }
 }

src/col/vct/col/ast/declaration/cls/BipComponentImpl.scala

@@ -0,0 +1,17 @@
+package vct.col.ast.declaration.cls
+
+import vct.col.ast.BipComponent
+import vct.col.print._
+
+trait BipComponentImpl[G] { this: BipComponent[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      Text("/*"),
+      Text("javaBipComponent(") <> Doc.args(Seq(
+        Text("name =") <+> ctx.name(this),
+        Text("state =") <+> ctx.name(initial),
+        Text("invariant =") <+> invariant,
+      )) <> ")",
+      Text("*/"),
+    ))
+}

src/col/vct/col/ast/declaration/cls/BipGuardImpl.scala

@@ -0,0 +1,13 @@
+package vct.col.ast.declaration.cls
+
+import vct.col.ast.BipGuard
+import vct.col.print.{Ctx, Doc, Group, Text, Empty}
+
+trait BipGuardImpl[G] { this: BipGuard[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      if(pure) Text("@Pure") else Empty,
+      Text("@Guard(name =") <+> ctx.name(this) <> ")",
+      Text("public boolean") <+> ctx.name(this) <> "()" <+> body.layoutAsBlock
+    ))
+}

src/col/vct/col/ast/declaration/cls/BipPortImpl.scala

@@ -0,0 +1,13 @@
+package vct.col.ast.declaration.cls
+
+import vct.col.ast.BipPort
+import vct.col.print._
+
+trait BipPortImpl[G] { this: BipPort[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      Text("/*"),
+      t.show <+> "javaBipPort" <+> ctx.name(this),
+      Text("*/"),
+    ))
+}

src/col/vct/col/ast/declaration/cls/BipStatePredicateImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.declaration.cls
+
+import vct.col.ast.BipStatePredicate
+import vct.col.print.{Ctx, Doc, Text, Group}
+
+trait BipStatePredicateImpl[G] { this: BipStatePredicate[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Group(Text("javaBipStatePredicate") <+> ctx.name(this) <+> "{" <>> expr <+/> "}")
+}

src/col/vct/col/ast/declaration/cls/BipTransitionImpl.scala

@@ -0,0 +1,26 @@
+package vct.col.ast.declaration.cls
+
+import vct.col.ast.BipTransition
+import vct.col.print.{Ctx, Doc, Empty, Group, Text}
+import vct.col.util.AstBuildHelpers.tt
+
+import scala.util.Try
+
+trait BipTransitionImpl[G] { this: BipTransition[G] =>
+  def layoutAnnotation(implicit ctx: Ctx): Doc =
+    Group(Text("@Transition(") <> Doc.args(Seq(
+      Text("name =") <+> ctx.name(this),
+      Text("source =") <+> ctx.name(source),
+      Text("target =") <+> ctx.name(target),
+      if (requires == tt[G]) Empty else Text("requires =") <+> requires,
+    )) <> ")")
+
+  def layoutArgs(implicit ctx: Ctx): Doc =
+    Doc.args(data.map { name =>
+      Text("@Data(name =") <+> ctx.name(name) <> ")" <+> Try(name.decl.t).getOrElse(Text("?brokenref?")) <+> ctx.name(name)
+    })
+
+  override def layout(implicit ctx: Ctx): Doc =
+    layoutAnnotation </>
+      Group(Text("public void") <+> ctx.name(this) <> "(" <> layoutArgs <> ")") <+> body.layoutAsBlock
+}

src/col/vct/col/ast/declaration/cls/InstanceFieldImpl.scala

@@ -1,7 +1,11 @@
 package vct.col.ast.declaration.cls
 
 import vct.col.ast.{Final, InstanceField}
+import vct.col.print._
 
 trait InstanceFieldImpl[G] { this: InstanceField[G] =>
   def isFinal = flags.collectFirst { case _: Final[G] => () }.isDefined
+
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.rspread(flags) <> t.show <+> ctx.name(this) <> ";"
 }

src/col/vct/col/ast/declaration/cls/InstanceFunctionImpl.scala

@@ -1,7 +1,24 @@
 package vct.col.ast.declaration.cls
 
 import vct.col.ast.InstanceFunction
+import vct.col.print._
+
+import scala.collection.immutable.ListMap
 
 trait InstanceFunctionImpl[G] { this: InstanceFunction[G] =>
+  def layoutModifiers(implicit ctx: Ctx): Seq[Doc] = ListMap(
+    inline -> "inline",
+    threadLocal -> "thread_local",
+  ).filter(_._1).values.map(Text).map(Doc.inlineSpec).toSeq
 
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      contract,
+      Group(
+        Doc.rspread(layoutModifiers) <> Text("pure") <+> returnType <+> ctx.name(this) <>
+          (if(typeArgs.nonEmpty) Text("<") <> Doc.args(typeArgs.map(ctx.name).map(Text)) <> ">" else Empty) <>
+          "(" <> Doc.args(args) <> ")" <>
+          body.map(Text(" =") <>> _ <> ";").getOrElse(Text(";"))
+      ),
+    ))
 }

src/col/vct/col/ast/declaration/cls/InstanceMethodImpl.scala

@@ -2,7 +2,30 @@ package vct.col.ast.declaration.cls
 
 import vct.col.ast.InstanceMethod
 import vct.col.ast.declaration.category.AbstractMethodImpl
+import vct.col.print._
+
+import scala.collection.immutable.ListMap
 
 trait InstanceMethodImpl[G] extends ClassDeclarationImpl[G] with AbstractMethodImpl[G] { this: InstanceMethod[G] =>
+  def layoutModifiers(implicit ctx: Ctx): Seq[Doc] = ListMap(
+    pure -> "pure",
+    inline -> "inline",
+  ).filter(_._1).values.map(Text).map(Doc.inlineSpec).toSeq
+
+  private def layoutNameAndArgs(implicit ctx: Ctx): Doc = ctx.syntax match {
+    case Ctx.Java =>
+      (if(typeArgs.nonEmpty) Text("<") <> Doc.args(typeArgs.map(ctx.name).map(Text)) <+> Empty else Empty) <>
+        ctx.name(this)
+    case _ =>
+      Text(ctx.name(this)) <> (if(typeArgs.nonEmpty) Text("<") <> Doc.args(typeArgs.map(ctx.name).map(Text)) else Empty)
+  }
 
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      contract,
+      Group(Group(Doc.rspread(layoutModifiers) <> returnType <+> layoutNameAndArgs) <>
+        "(" <> Doc.args(args) <> ")") <>
+        (if(outArgs.nonEmpty) Text(" returns") <+> "(" <> Doc.args(outArgs) <> ")" else Empty) <>
+        body.map(Text(" ") <> _.layoutAsBlock).getOrElse(Text(";")),
+    ))
 }

src/col/vct/col/ast/declaration/cls/InstanceOperatorFunctionImpl.scala

@@ -1,7 +1,24 @@
 package vct.col.ast.declaration.cls
 
 import vct.col.ast.{InstanceOperatorFunction, Variable}
+import vct.col.print._
+
+import scala.collection.immutable.ListMap
 
 trait InstanceOperatorFunctionImpl[G] { this: InstanceOperatorFunction[G] =>
   def typeArgs: Seq[Variable[G]] = Nil
+
+  def layoutModifiers(implicit ctx: Ctx): Seq[Doc] = ListMap(
+    inline -> "inline",
+    threadLocal -> "thread_local",
+  ).filter(_._1).values.map(Text).map(Doc.inlineSpec).toSeq
+
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      contract,
+      Group(
+        Doc.rspread(layoutModifiers) <> "pure" <+> returnType <+> operator <> "(" <> Doc.args(args) <> ")" <>
+          body.map(Text(" =") <>> _ <> ";").getOrElse(Text(";"))
+      ),
+    ))
 }

src/col/vct/col/ast/declaration/cls/InstanceOperatorMethodImpl.scala

@@ -1,8 +1,23 @@
 package vct.col.ast.declaration.cls
 
 import vct.col.ast.{InstanceOperatorMethod, Type, Variable}
+import vct.col.print._
+
+import scala.collection.immutable.ListMap
 
 trait InstanceOperatorMethodImpl[G] { this: InstanceOperatorMethod[G] =>
   def typeArgs: Seq[Variable[G]] = Nil
   def outArgs: Seq[Variable[G]] = Nil
+
+  def layoutModifiers(implicit ctx: Ctx): Seq[Doc] = ListMap(
+    pure -> "pure",
+    inline -> "inline",
+  ).filter(_._1).values.map(Text).map(Doc.inlineSpec).toSeq
+
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      contract,
+      Group(Doc.rspread(layoutModifiers) <> returnType.show <+> operator <> "(" <> Doc.args(args) <> ")") <>
+        body.map(Text(" ") <> _.layoutAsBlock).getOrElse(Text(";")),
+    ))
 }

src/col/vct/col/ast/declaration/cls/InstancePredicateImpl.scala

@@ -2,7 +2,18 @@ package vct.col.ast.declaration.cls
 
 import vct.col.ast.InstancePredicate
 import vct.col.ast.declaration.category.AbstractPredicateImpl
+import vct.col.print._
+
+import scala.collection.immutable.ListMap
 
 trait InstancePredicateImpl[G] extends ClassDeclarationImpl[G] with AbstractPredicateImpl[G] { this: InstancePredicate[G] =>
+  def layoutModifiers(implicit ctx: Ctx): Seq[Doc] = ListMap(
+    inline -> "inline",
+    threadLocal -> "thread_local",
+  ).filter(_._1).values.map(Text).map(Doc.inlineSpec).toSeq
 
+  override def layout(implicit ctx: Ctx): Doc = Group(
+    Doc.rspread(layoutModifiers) <> "resource" <+> ctx.name(this) <> "(" <> Doc.args(args) <> ")" <>
+      body.map(Text(" =") <>> _).getOrElse(Text(";"))
+  )
 }

src/col/vct/col/ast/declaration/cls/RunMethodImpl.scala

@@ -1,7 +1,12 @@
 package vct.col.ast.declaration.cls
 
 import vct.col.ast.RunMethod
+import vct.col.print._
 
 trait RunMethodImpl[G] { this: RunMethod[G] =>
-
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      contract.show,
+      Text("run") <> body.map(Empty <+> _.layoutAsBlock).getOrElse(Text(";")),
+    ))
 }