Revert "Save work"

This reverts commit d666db9.

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

@@ -55,7 +55,6 @@ import vct.col.ast.family.javavar.JavaVariableDeclarationImpl
 import vct.col.ast.family.location._
 import vct.col.ast.family.loopcontract._
 import vct.col.ast.family.parregion._
-import vct.col.ast.family.pvlcommunicate.{PVLCommunicateSubjectImpl, PVLFamilyRangeImpl, PVLIndexedFamilyNameImpl, PVLThreadNameImpl}
 import vct.col.ast.family.signals._
 import vct.col.ast.lang._
 import vct.col.ast.lang.smt._
@@ -1212,17 +1211,17 @@ final case class PVLNew[G](t: Type[G], args: Seq[Expr[G]], givenMap: Seq[(Ref[G,
 sealed trait PVLClassDeclaration[G] extends ClassDeclaration[G] with PVLClassDeclarationImpl[G]
 final class PVLConstructor[G](val contract: ApplicableContract[G], val args: Seq[Variable[G]], val body: Option[Statement[G]])(val blame: Blame[ConstructorFailure])(implicit val o: Origin) extends PVLClassDeclaration[G] with PVLConstructorImpl[G]
 
-sealed trait PVLCommunicateSubject[G] extends NodeFamily[G]  with PVLCommunicateSubjectImpl[G]
-case class PVLThreadName[G](name: String)(implicit val o: Origin) extends PVLCommunicateSubject[G] with PVLThreadNameImpl[G] {
+sealed trait PVLCommunicateSubject[G] extends NodeFamily[G]
+case class PVLThreadName[G](name: String)(implicit val o: Origin) extends PVLCommunicateSubject[G] {
   var ref: Option[PVLNameTarget[G]] = None
 }
-case class PVLIndexedFamilyName[G](family: String, index: Expr[G])(implicit val o: Origin) extends PVLCommunicateSubject[G] with PVLIndexedFamilyNameImpl[G] {
+case class PVLIndexedFamilyName[G](family: String, index: Expr[G])(implicit val o: Origin) extends PVLCommunicateSubject[G] {
   var ref: Option[PVLNameTarget[G]] = None
 }
-case class PVLFamilyRange[G](family: String, binder: String, start: Expr[G], end: Expr[G])(implicit val o: Origin) extends PVLCommunicateSubject[G] with PVLFamilyRangeImpl[G] {
+case class PVLFamilyRange[G](family: String, binder: String, start: Expr[G], end: Expr[G])(implicit val o: Origin) extends PVLCommunicateSubject[G] {
   var ref: Option[PVLNameTarget[G]] = None
 }
-case class PVLCommunicateAccess[G](subjectX: PVLCommunicateSubject[G], field: String)(implicit val o: Origin) extends NodeFamily[G] with PVLCommunicateAccessImpl[G] {
+case class PVLCommunicateAccess[G](subjectX: PVLCommunicateSubject[G], field: String)(implicit val o: Origin) extends NodeFamily[G] {
   var ref: Option[PVLDerefTarget[G]] = None
 }
 case class PVLCommunicate[G](sender: PVLCommunicateAccess[G], receiver: PVLCommunicateAccess[G])(implicit val o: Origin) extends Statement[G]

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

@@ -277,11 +277,6 @@ case object ResolveReferences extends LazyLogging {
     case cls: Class[G] => ctx
       .copy(currentThis=Some(RefClass(cls)))
       .declare(cls.declarations)
-    case seqProg: VeyMontSeqProg[G] => ctx
-      .copy(currentThis=Some(RefSeqProg(seqProg)))
-      .declare(seqProg.methods)
-      .declare(seqProg.threads)
-      .declare(seqProg.progArgs)
     case method: JavaMethod[G] => ctx
       .copy(currentResult=Some(RefJavaMethod(method)))
       .copy(inStaticJavaContext=method.modifiers.collectFirst { case _: JavaStatic[_] => () }.nonEmpty)
@@ -381,8 +376,6 @@ case object ResolveReferences extends LazyLogging {
       local.ref = Some(PVL.findName(name, ctx).getOrElse(throw NoSuchNameError("local", name, local)))
     case local@Local(ref) =>
       ref.tryResolve(name => Spec.findLocal(name, ctx).getOrElse(throw NoSuchNameError("local", name, local)))
-    case local @ PVLThreadName(name) =>
-      local.ref = Some(PVL.findName(name, ctx).getOrElse(throw NoSuchNameError("VeyMont thread", name, local)))
     case local@TVar(ref) =>
       ref.tryResolve(name => Spec.findLocal(name, ctx).getOrElse(throw NoSuchNameError("type variable", name, local)))
     case funcOf@FunctionOf(v, vars) =>

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

@@ -296,7 +296,7 @@ case class RefBipTransitionSynchronization[G](decl: BipTransitionSynchronization
 case class RefBipConstructor[G](decl: BipConstructor[G]) extends Referrable[G]
 
 case class RefLlvmSpecFunction[G](decl: LlvmSpecFunction[G]) extends Referrable[G] with SpecInvocationTarget[G] with ResultTarget[G]
-case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[G] with ThisTarget[G]
+case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[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]

test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala

@@ -20,29 +20,8 @@ class TechnicalVeymontSpec extends VercorsSpec {
      }
   """
 
-  vercors should error withCode "noSuchName" in "non-existent thread name in communicate fails" pvl
-  """
-    seq_program Example() {
-       run {
-         communicate charlie.x <- charlie.x;
-       }
-    }
-  """
-
-  vercors should error withCode "???" in "non-existent field in communicate fails" pvl
-  """
-    class Storage { int x; }
-    seq_program Example() {
-       thread charlie = Storage();
-       run {
-         communicate charlie.nonExistent <- charlie.nonExistent;
-       }
-    }
-  """
-
   vercors should error withCode "parseError" in "parameterized sends not yet supported " pvl
   """
-    class Storage { int x; }
     seq_program Example() {
       thread alice[10] = Storage();
       thread bob[10] = Storage();