From f2551d66c30b4046e9f55355312308889eedaede Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Wed, 18 Oct 2023 16:10:29 +0200
Subject: [PATCH] Salvage early resolve stuff and tests

---
 src/col/vct/col/resolve/Resolve.scala         |  7 +++++++
 .../examples/TechnicalVeymontSpec.scala       | 21 +++++++++++++++++++
 2 files changed, 28 insertions(+)

diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala
index 277b41d3b6..3384f2e32a 100644
--- a/src/col/vct/col/resolve/Resolve.scala
+++ b/src/col/vct/col/resolve/Resolve.scala
@@ -277,6 +277,11 @@ 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)
@@ -376,6 +381,8 @@ 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) =>
diff --git a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala
index 960d77642b..7b2df27bf0 100644
--- a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala
+++ b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala
@@ -20,8 +20,29 @@ 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();