Refactor VeyMontSeqProg to SeqProg

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

@@ -129,7 +129,7 @@ final case class TZFraction[G]()(implicit val o: Origin = DiagnosticOrigin) exte
 sealed trait DeclaredType[G] extends Type[G] with DeclaredTypeImpl[G]
 final case class TModel[G](model: Ref[G, Model[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TModelImpl[G]
 final case class TClass[G](cls: Ref[G, Class[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TClassImpl[G]
-final case class TSeqProg[G](cls: Ref[G, VeyMontSeqProg[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TSeqProgImpl[G]
+final case class TSeqProg[G](cls: Ref[G, SeqProg[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TSeqProgImpl[G]
 final case class TVeyMontThread[G](cls: Ref[G, VeyMontThread[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TVeyMontThreadImpl[G]
 final case class TAnyClass[G]()(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TAnyClassImpl[G]
 final case class TAxiomatic[G](adt: Ref[G, AxiomaticDataType[G]], args: Seq[Type[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TAxiomaticImpl[G]
@@ -220,7 +220,7 @@ final class HeapVariable[G](val t: Type[G])(implicit val o: Origin) extends Glob
 final class SimplificationRule[G](val axiom: Expr[G])(implicit val o: Origin) extends GlobalDeclaration[G] with SimplificationRuleImpl[G]
 final class AxiomaticDataType[G](val decls: Seq[ADTDeclaration[G]], val typeArgs: Seq[Variable[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with AxiomaticDataTypeImpl[G]
 final class Class[G](val declarations: Seq[ClassDeclaration[G]], val supports: Seq[Ref[G, Class[G]]], val intrinsicLockInvariant: Expr[G])(implicit val o: Origin) extends GlobalDeclaration[G] with ClassImpl[G]
-final class VeyMontSeqProg[G](val contract: ApplicableContract[G], val progArgs : Seq[Variable[G]], val threads: Seq[VeyMontThread[G]], val runMethod: ClassDeclaration[G], val methods: Seq[ClassDeclaration[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with VeyMontSeqProgImpl[G]
+final class SeqProg[G](val contract: ApplicableContract[G], val progArgs : Seq[Variable[G]], val threads: Seq[VeyMontThread[G]], val runMethod: ClassDeclaration[G], val methods: Seq[ClassDeclaration[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with VeyMontSeqProgImpl[G]
 final class VeyMontThread[G](val threadType: Type[G], val args: Seq[Expr[G]])(implicit val o: Origin) extends Declaration[G] with VeyMontThreadImpl[G]
 final class Model[G](val declarations: Seq[ModelDeclaration[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with Declarator[G] with ModelImpl[G]
 final class Function[G](val returnType: Type[G], val args: Seq[Variable[G]], val typeArgs: Seq[Variable[G]],
@@ -426,7 +426,7 @@ final case class AmbiguousThis[G]()(implicit val o: Origin) extends Expr[G] with
 
 final case class ThisObject[G](cls: Ref[G, Class[G]])(implicit val o: Origin) extends Expr[G] with ThisObjectImpl[G]
 final case class ThisModel[G](cls: Ref[G, Model[G]])(implicit val o: Origin) extends Expr[G] with ThisModelImpl[G]
-final case class ThisSeqProg[G](cls: Ref[G, VeyMontSeqProg[G]])(implicit val o: Origin) extends Expr[G] with ThisSeqProgImpl[G]
+final case class ThisSeqProg[G](cls: Ref[G, SeqProg[G]])(implicit val o: Origin) extends Expr[G] with ThisSeqProgImpl[G]
 
 final case class AmbiguousResult[G]()(implicit val o: Origin) extends Expr[G] with AmbiguousResultImpl[G] {
   var ref: Option[ResultTarget[G]] = None

src/col/vct/col/ast/declaration/global/VeyMontSeqProgImpl.scala

@@ -1,12 +1,12 @@
 package vct.col.ast.declaration.global
 
-import vct.col.ast.{Class, Declaration, VeyMontSeqProg}
+import vct.col.ast.{Class, Declaration, SeqProg}
 import vct.col.ast.util.Declarator
 import vct.col.check.{CheckContext, CheckError}
 import vct.col.origin.Origin
 import vct.col.print._
 
-trait VeyMontSeqProgImpl[G] extends Declarator[G] { this: VeyMontSeqProg[G] =>
+trait VeyMontSeqProgImpl[G] extends Declarator[G] { this: SeqProg[G] =>
   def members: Seq[Declaration[G]] = threads ++ Seq(runMethod) ++ methods
   override def declarations: Seq[Declaration[G]] = progArgs ++ members
 

src/col/vct/col/print/Namer.scala

@@ -13,7 +13,7 @@ case class Namer[G](syntax: Ctx.Syntax) {
     stack.toSeq.filter(n => f.isDefinedAt(n))
 
   private def nearestClass = nearest {
-    case _: Class[G] | _: JavaClass[G] | _: VeyMontSeqProg[G] | _: JavaInterface[G] | _: JavaAnnotationInterface[G] => ()
+    case _: Class[G] | _: JavaClass[G] | _: SeqProg[G] | _: JavaInterface[G] | _: JavaAnnotationInterface[G] => ()
   }
 
   private def nearestVariableScope = nearest {
@@ -107,7 +107,7 @@ case class Namer[G](syntax: Ctx.Syntax) {
       case decl: CPPLocalDeclaration[G] => nameKeyed(nearestVariableScope, decl)
       case decl: CPPParam[G] => nameKeyed(nearestCallable, decl)
       case decl: JavaLocalDeclaration[G] => nameKeyed(nearestCallable, decl)
-      case decl: VeyMontThread[G] => nameKeyed(nearest { case _: VeyMontSeqProg[G] => () }, decl)
+      case decl: VeyMontThread[G] => nameKeyed(nearest { case _: SeqProg[G] => () }, decl)
       case decl: JavaParam[G] => nameKeyed(nearestCallable, decl)
       case _ =>
     }

src/col/vct/col/resolve/Resolve.scala

@@ -277,7 +277,7 @@ case object ResolveReferences extends LazyLogging {
     case cls: Class[G] => ctx
       .copy(currentThis=Some(RefClass(cls)))
       .declare(cls.declarations)
-    case seqProg: VeyMontSeqProg[G] => ctx
+    case seqProg: SeqProg[G] => ctx
       .copy(currentThis = Some(RefSeqProg(seqProg)))
       .declare(seqProg.methods)
       .declare(seqProg.threads)

src/col/vct/col/resolve/ctx/Referrable.scala

@@ -154,7 +154,7 @@ case object Referrable {
     case decl: CPPLocalDeclaration[G] => return decl.decl.inits.indices.map(RefCPPLocalDeclaration(decl, _))
     case decl: JavaLocalDeclaration[G] => return decl.decls.indices.map(RefJavaLocalDeclaration(decl, _))
     case decl: PVLConstructor[G] => RefPVLConstructor(decl)
-    case decl: VeyMontSeqProg[G] => RefSeqProg(decl)
+    case decl: SeqProg[G] => RefSeqProg(decl)
     case decl: VeyMontThread[G] => RefVeyMontThread(decl)
     case decl: LlvmFunctionDefinition[G] => RefLlvmFunctionDefinition(decl)
     case decl: LlvmGlobal[G] => RefLlvmGlobal(decl)
@@ -299,7 +299,7 @@ case class RefBipConstructor[G](decl: BipConstructor[G]) extends Referrable[G]
 case class RefHeapVariable[G](decl: HeapVariable[G]) extends Referrable[G]
 
 case class RefLlvmSpecFunction[G](decl: LlvmSpecFunction[G]) extends Referrable[G] with LlvmInvocationTarget[G] with ResultTarget[G]
-case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[G] with ThisTarget[G]
+case class RefSeqProg[G](decl: SeqProg[G]) extends Referrable[G] with ThisTarget[G]
 case class RefVeyMontThread[G](decl: VeyMontThread[G]) extends Referrable[G] with PVLNameTarget[G]
 case class RefProverType[G](decl: ProverType[G]) extends Referrable[G] with SpecTypeNameTarget[G]
 case class RefProverFunction[G](decl: ProverFunction[G]) extends Referrable[G] with SpecInvocationTarget[G]

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -1757,7 +1757,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
           case JavaVariableDeclaration(name, dims, Some(v)) =>
             JavaVariableDeclaration(name, dims, Some(coerce(v, FuncTools.repeat[Type[Pre]](TArray(_), dims, declaration.t))))
         })
-      case seqProg: VeyMontSeqProg[Pre] => seqProg
+      case seqProg: SeqProg[Pre] => seqProg
       case thread: VeyMontThread[Pre] => thread
       case bc: BipConstructor[Pre] => new BipConstructor(bc.args, bc.body, bc.requires)(bc.blame)
       case bc: BipComponent[Pre] =>

src/parsers/vct/parsers/transform/PVLToCol.scala

@@ -49,7 +49,7 @@ case class PVLToCol[G](override val baseOrigin: Origin,
     case SeqProgThread(_, threadId, _, threadType, _, args, _, _) => new VeyMontThread(convert(threadType), args.map(convert(_)).getOrElse(Nil))(origin(decl).replacePrefName(convert(threadId)))
   }
 
-  def convertVeyMontProg(implicit cls: DeclVeyMontSeqProgContext): VeyMontSeqProg[G] = cls match {
+  def convertVeyMontProg(implicit cls: DeclVeyMontSeqProgContext): SeqProg[G] = cls match {
     case DeclVeyMontSeqProg0(contract, _, name, _, args, _, _, decls, _) =>
       val seqargs = args.map(convert(_)).getOrElse(Nil)
       val declseq: Seq[Declaration[G]] = decls.map(convert(_))
@@ -63,7 +63,7 @@ case class PVLToCol[G](override val baseOrigin: Origin,
         case v: VeyMontThread[G] => v
       }
       withContract(contract, contract => {
-        new VeyMontSeqProg(
+        new SeqProg(
           contract.consumeApplicableContract(blame(cls)),
           seqargs,
           threads,

src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala

@@ -97,7 +97,7 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
       currentThis.having(ThisModel[Post](succ(model))) {
         globalDeclarations.succeed(model, model.rewrite())
       }
-    case seqProg: VeyMontSeqProg[Pre] =>
+    case seqProg: SeqProg[Pre] =>
       implicit val o: Origin = seqProg.o
       currentThis.having(ThisSeqProg[Post](succ(seqProg))) {
         globalDeclarations.succeed(seqProg, seqProg.rewrite())

src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala

@@ -1,7 +1,7 @@
 package vct.col.rewrite.veymont
 
 import hre.util.ScopedStack
-import vct.col.ast.{Assign, Declaration, Deref, DerefVeyMontThread, Expr, MethodInvocation, Node, ProcedureInvocation, RunMethod, Statement, VeyMontAssignExpression, VeyMontCommExpression, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.{Assign, Declaration, Deref, DerefVeyMontThread, Expr, MethodInvocation, Node, ProcedureInvocation, RunMethod, Statement, VeyMontAssignExpression, VeyMontCommExpression, SeqProg, VeyMontThread}
 import vct.col.ref.Ref
 import vct.col.rewrite.veymont.AddVeyMontAssignmentNodes.{AddVeyMontAssignmentError, getDerefsFromExpr, getThreadDeref}
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
@@ -48,7 +48,7 @@ case class AddVeyMontAssignmentNodes[Pre <: Generation]() extends Rewriter[Pre]
 
   override def dispatch(decl: Declaration[Pre]): Unit =
     decl match {
-      case dcl: VeyMontSeqProg[Pre] => inSeqProg.having(()) {
+      case dcl: SeqProg[Pre] => inSeqProg.having(()) {
         rewriteDefault(dcl)
       }
       case _ => rewriteDefault(decl)

src/rewrite/vct/rewrite/veymont/AddVeyMontConditionNodes.scala

@@ -2,7 +2,7 @@ package vct.col.rewrite.veymont
 
 
 import hre.util.ScopedStack
-import vct.col.ast.{And, Block, BooleanValue, Branch, Declaration, Expr, Loop, Node, Statement, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.{And, Block, BooleanValue, Branch, Declaration, Expr, Loop, Node, Statement, VeyMontCondition, SeqProg, VeyMontThread}
 import vct.col.ref.Ref
 import vct.col.rewrite.veymont.AddVeyMontAssignmentNodes.{getDerefsFromExpr, getThreadDeref}
 import vct.col.rewrite.veymont.AddVeyMontConditionNodes.AddVeyMontConditionError
@@ -29,7 +29,7 @@ case class AddVeyMontConditionNodes[Pre <: Generation]() extends Rewriter[Pre] {
 
   override def dispatch(decl: Declaration[Pre]): Unit =
     decl match {
-      case dcl: VeyMontSeqProg[Pre] =>
+      case dcl: SeqProg[Pre] =>
         inSeqProg.push(dcl.threads.size)
         try {
           rewriteDefault(dcl)

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

@@ -2,7 +2,7 @@ package vct.rewrite.veymont
 
 import hre.util.ScopedStack
 import vct.col.ast.RewriteHelpers.{RewriteApplicableContract, RewriteClass, RewriteDeref, RewriteJavaClass, RewriteJavaConstructor, RewriteMethodInvocation}
-import vct.col.ast.{AbstractRewriter, ApplicableContract, Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaConstructor, JavaInvocation, JavaLocal, JavaMethod, JavaNamedType, JavaParam, JavaPublic, JavaTClass, Local, Loop, MethodInvocation, NewObject, Node, Procedure, Program, RunMethod, Scope, Statement, TClass, TVeyMontChannel, TVoid, ThisObject, ThisSeqProg, Type, UnitAccountedPredicate, Variable, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.{AbstractRewriter, ApplicableContract, Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaConstructor, JavaInvocation, JavaLocal, JavaMethod, JavaNamedType, JavaParam, JavaPublic, JavaTClass, Local, Loop, MethodInvocation, NewObject, Node, Procedure, Program, RunMethod, Scope, Statement, TClass, TVeyMontChannel, TVoid, ThisObject, ThisSeqProg, Type, UnitAccountedPredicate, Variable, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, SeqProg, VeyMontThread}
 import vct.col.origin.Origin
 import vct.col.resolve.ctx.RefJavaMethod
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, RewriterBuilderArg, Rewritten}
@@ -59,7 +59,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     decl match {
       case p: Procedure[Pre] => givenClassConstrSucc.update(p.returnType,p)
       case c : Class[Pre] => globalDeclarations.succeed(c, dispatchGivenClass(c))
-      case seqProg: VeyMontSeqProg[Pre] => dispatchThreads(seqProg)
+      case seqProg: SeqProg[Pre] => dispatchThreads(seqProg)
       case thread: VeyMontThread[Pre] => dispatchThread(thread)
       case other => rewriteDefault(other)
     }
@@ -73,7 +73,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     } else rewriteDefault(thread)
   }
 
-  private def dispatchThreads(seqProg: VeyMontSeqProg[Pre]): Unit = {
+  private def dispatchThreads(seqProg: SeqProg[Pre]): Unit = {
     val (channelClasses,indexedChannelInfo) = extractChannelInfo(seqProg)
     channelClasses.foreach{ case (t,c) =>
       globalDeclarations.declare(c)
@@ -152,7 +152,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     }
   }
 
-  private def extractChannelInfo(seqProg: VeyMontSeqProg[Pre]): (Map[Type[Pre], JavaClass[Post]], Seq[ChannelInfo[Pre]]) = {
+  private def extractChannelInfo(seqProg: SeqProg[Pre]): (Map[Type[Pre], JavaClass[Post]], Seq[ChannelInfo[Pre]]) = {
     val channelInfo = collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg)
     val indexedChannelInfo: Seq[ChannelInfo[Pre]] = channelInfo.groupBy(_.channelName).values.flatMap(chanInfoSeq =>
       if (chanInfoSeq.size <= 1) chanInfoSeq
@@ -263,13 +263,13 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     }
   }
 
-  private def collectChannelsFromRun(seqProg: VeyMontSeqProg[Pre]) =
+  private def collectChannelsFromRun(seqProg: SeqProg[Pre]) =
     seqProg.runMethod match {
       case r: RunMethod[Pre] => getChannelsFromBody(r.body, r)
       case other => throw ParalliseVeyMontThreadsError(other, "seq_program run method expected")
     }
 
-  private def collectChannelsFromMethods(seqProg: VeyMontSeqProg[Pre]) =
+  private def collectChannelsFromMethods(seqProg: SeqProg[Pre]) =
     seqProg.methods.flatMap {
       case m: InstanceMethod[Pre] => getChannelsFromBody(m.body, m)
       case other => throw ParalliseVeyMontThreadsError(other, "seq_program method expected")

src/rewrite/vct/rewrite/veymont/StructureCheck.scala

@@ -27,7 +27,7 @@ case class StructureCheck[Pre <: Generation]() extends Rewriter[Pre] {
 
   override def dispatch(decl: Declaration[Pre]): Unit =
     decl match {
-      case dcl: VeyMontSeqProg[Pre] => inSeqProg.having(()) {
+      case dcl: SeqProg[Pre] => inSeqProg.having(()) {
         rewriteDefault(dcl)
       }
       case m: InstanceMethod[Pre] =>
@@ -45,7 +45,7 @@ case class StructureCheck[Pre <: Generation]() extends Rewriter[Pre] {
 
   override def dispatch(prog : Program[Pre]) : Program[Post] = {
     if(!prog.declarations.exists {
-      case dcl: VeyMontSeqProg[Pre] =>
+      case dcl: SeqProg[Pre] =>
         if(dcl.threads.isEmpty)
           throw VeyMontStructCheckError(dcl,"A seq_program needs to have at least 1 thread, but none was found!")
         else true