VeyMont produces output

src/main/vct/main/modes/VeyMont.scala

@@ -14,7 +14,7 @@ object VeyMont extends LazyLogging {
 
   def verifyWithOptions(options: Options, inputs: Seq[PathOrStd]) = {
     val collector = BlameCollector()
-    val stages = Stages.veymontOfOptions(options, ConstantBlameProvider(collector))
+    val stages = Stages.veymontTransformationOfOptions(options, ConstantBlameProvider(collector))
     logger.debug("Stages: " ++ stages.flatNames.map(_._1).mkString(", "))
     stages.run(inputs) match {
       case Left(value) => logger.error(value.text)

src/main/vct/main/stages/CodeGeneration.scala

@@ -0,0 +1,67 @@
+package vct.main.stages
+
+import hre.progress.Progress
+import hre.stages.Stage
+import vct.col.ast.{JavaClass, Node, Verification}
+import vct.col.print.Ctx
+import vct.col.rewrite.{Generation, PrettifyBlocks, RewriterBuilder}
+import vct.importer.Util
+import vct.main.stages.Transformation.writeOutFunctions
+import vct.options.Options
+import vct.options.types.{Backend, PathOrStd}
+import vct.rewrite.veymont.ParalleliseVeyMontThreads
+
+object CodeGeneration {
+
+  private def writeOutFunctions(m: Map[String, PathOrStd]): Seq[(String, Verification[_ <: Generation] => Unit)] =
+    m.toSeq.map {
+      case (key, out) => (key, (program: Verification[_ <: Generation]) => out.write { writer =>
+        program.write(writer)(Ctx().namesIn(program))
+      })
+    }
+
+  def veymontGenerationOfOptions(options: Options): VeyMontGeneration =
+    options.backend match {
+      case Backend.Silicon | Backend.Carbon =>
+        VeyMontGeneration(
+          onBeforePassKey = writeOutFunctions(options.outputBeforePass),
+          onAfterPassKey = writeOutFunctions(options.outputAfterPass),
+          channelClass = Util.loadJavaClass(options.veymontChannel),
+        )
+    }
+}
+
+class CodeGeneration(val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)],
+                     val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)],
+                     val passes: Seq[RewriterBuilder]
+                       ) extends Stage[Verification[_ <: Generation], Verification[_ <: Generation]] {
+  override def friendlyName: String = "Generating VeyMont output"
+
+  override def progressWeight: Int = 1
+
+  override def run(input: Verification[_ <: Generation]): Verification[_ <: Generation] = {
+    var result: Verification[_ <: Generation] = input
+    Progress.foreach(passes, (pass: RewriterBuilder) => pass.key) { pass =>
+      onBeforePassKey.foreach {
+        case (key, action) => if (pass.key == key) action(result)
+      }
+
+      result = pass().dispatch(result)
+
+      onAfterPassKey.foreach {
+        case (key, action) => if (pass.key == key) action(result)
+      }
+
+      result = PrettifyBlocks().dispatch(result)
+    }
+    result
+  }
+
+}
+
+case class VeyMontGeneration(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
+                             override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
+                             channelClass: JavaClass[_])
+  extends CodeGeneration(onBeforePassKey, onAfterPassKey, Seq(
+    ParalleliseVeyMontThreads.withArg(channelClass),
+  ))

src/main/vct/main/stages/Stages.scala

@@ -58,10 +58,11 @@ case object Stages {
       .thenRun(ExpectedErrors.ofOptions(options))
   }
 
-  def veymontOfOptions(options: Options, blameProvider: BlameProvider): Stages[Seq[Readable], Unit] = {
+  def veymontTransformationOfOptions(options: Options, blameProvider: BlameProvider): Stages[Seq[Readable], Unit] = {
     Parsing.ofOptions(options, blameProvider)
       .thenRun(Resolution.ofOptions(options, blameProvider))
-      .thenRun(Transformation.veymontOfOptions(options))
+      .thenRun(Transformation.veymontTransformationOfOptions(options))
+      .thenRun(CodeGeneration.veymontGenerationOfOptions(options))
       .thenRun(Output.veymontOfOptions(options))
   }
 

src/main/vct/main/stages/Transformation.scala

@@ -65,13 +65,12 @@ object Transformation {
         )
     }
 
-  def veymontOfOptions(options: Options): Transformation =
+  def veymontTransformationOfOptions(options: Options): Transformation =
     options.backend match {
       case Backend.Silicon | Backend.Carbon =>
         VeyMontTransformation(
           onBeforePassKey = writeOutFunctions(options.outputBeforePass),
           onAfterPassKey = writeOutFunctions(options.outputAfterPass),
-          channelClass = Util.loadJavaClass(options.veymontChannel),
         )
     }
 }
@@ -289,12 +288,12 @@ case class SilverTransformation
   ))
 
 case class VeyMontTransformation(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
-                                 override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
-                                 val channelClass: JavaClass[_])
+                                 override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil)
   extends Transformation(onBeforePassKey, onAfterPassKey, Seq(
     AddVeyMontAssignmentNodes,
     AddVeyMontConditionNodes,
     StructureCheck,
-    ParalleliseVeyMontThreads.withArg(channelClass),
   ))
 
+
+

src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala

@@ -158,7 +158,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     }
 
     override def dispatch(decl: Declaration[Pre]): Unit = decl match {
-      case jc: JavaConstructor[Pre] => classDeclarations.declare(jc.rewrite(name = getChannelClassName(channelType))) //TODO: deze rewrite verwijderd de constructor..
+      case jc: JavaConstructor[Pre] => classDeclarations.declare(jc.rewrite(name = getChannelClassName(channelType)))
       case other => rewriteDefault(other)
     }
   }