Verification in the IDE now works correctly when declaring nested mod… (

#5651)

Fixes #5650

### Description
Verification in the IDE now works correctly when declaring nested module
in a different file than their parent.

### How has this been tested?
Added an IDE test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -94,6 +94,7 @@ public bool InferredDecreases {
 
   public bool AllowsAllocation => CwInner.AllowsAllocation;
 
+  public bool SingleFileToken => CwInner.SingleFileToken;
   public IEnumerable<IToken> OwnedTokens => CwInner.OwnedTokens;
   public RangeToken RangeToken => CwInner.RangeToken;
   public IToken NavigationToken => CwInner.NavigationToken;
@@ -105,41 +106,6 @@ public string GetDescription(DafnyOptions options) {
   public string Designator => WhatKind;
 }
 
-
-public class DontUseICallable : ICallable {
-  public string WhatKind { get { throw new cce.UnreachableException(); } }
-  public bool IsGhost { get { throw new cce.UnreachableException(); } }
-  public List<TypeParameter> TypeArgs { get { throw new cce.UnreachableException(); } }
-  public List<Formal> Ins { get { throw new cce.UnreachableException(); } }
-  public ModuleDefinition EnclosingModule { get { throw new cce.UnreachableException(); } }
-  public bool MustReverify { get { throw new cce.UnreachableException(); } }
-  public string FullSanitizedName { get { throw new cce.UnreachableException(); } }
-  public bool AllowsNontermination { get { throw new cce.UnreachableException(); } }
-  public IToken Tok { get { throw new cce.UnreachableException(); } }
-  public IEnumerable<INode> Children => throw new cce.UnreachableException();
-  public IEnumerable<INode> PreResolveChildren => throw new cce.UnreachableException();
-
-  public string NameRelativeToModule { get { throw new cce.UnreachableException(); } }
-  public Specification<Expression> Decreases { get { throw new cce.UnreachableException(); } }
-  public bool InferredDecreases {
-    get { throw new cce.UnreachableException(); }
-    set { throw new cce.UnreachableException(); }
-  }
-  public bool AllowsAllocation => throw new cce.UnreachableException();
-  public IEnumerable<INode> GetConcreteChildren() {
-    throw new cce.UnreachableException();
-  }
-
-  public IEnumerable<IToken> OwnedTokens => throw new cce.UnreachableException();
-  public RangeToken RangeToken => throw new cce.UnreachableException();
-  public IToken NavigationToken => throw new cce.UnreachableException();
-  public SymbolKind? Kind => throw new cce.UnreachableException();
-  public string GetDescription(DafnyOptions options) {
-    throw new cce.UnreachableException();
-  }
-  public string Designator => WhatKind;
-}
-
 /// <summary>
 /// An IMethodCodeContext is a Method or IteratorDecl.
 /// </summary>

Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs

@@ -20,6 +20,9 @@ public override ModuleSignature AccessibleSignature(bool ignoreExports) {
     }
     return this.AccessibleSignature();
   }
+
+  public override bool SingleFileToken => ModuleDef.SingleFileToken;
+
   public override ModuleSignature AccessibleSignature() {
     if (DefaultExport == null) {
       if (emptySignature == null) {

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -29,6 +29,7 @@ public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, IClonea
   public string DafnyName => NameNode.StartToken.val; // The (not-qualified) name as seen in Dafny source code
   public Name NameNode; // (Last segment of the) module name
 
+  public override bool SingleFileToken => !ResolvedPrefixNamedModules.Any();
   public override IToken Tok => NameNode.StartToken;
 
   public string Name => NameNode.Value;
@@ -130,11 +131,12 @@ public ModuleDefinition(Cloner cloner, ModuleDefinition original) : base(cloner,
     // For cloning modules into their compiled variants, we don't want to copy resolved fields, but we do need to copy this.
     // We're hoping to remove the copying of modules into compiled variants altogether,
     // and then this can be moved to inside the `if (cloner.CloneResolvedFields)` block
-    foreach (var tup in original.ResolvedPrefixNamedModules) {
-      ResolvedPrefixNamedModules.Add(cloner.CloneDeclaration(tup, this));
-    }
 
     if (cloner.CloneResolvedFields) {
+      foreach (var tup in original.ResolvedPrefixNamedModules) {
+        ResolvedPrefixNamedModules.Add(cloner.CloneDeclaration(tup, this));
+      }
+
       Height = original.Height;
     }
   }

Source/DafnyCore/Generic/Node.cs

@@ -10,6 +10,7 @@
 namespace Microsoft.Dafny;
 
 public interface INode {
+  bool SingleFileToken { get; }
   public IToken StartToken => RangeToken.StartToken;
   public IToken EndToken => RangeToken.EndToken;
   IEnumerable<IToken> OwnedTokens { get; }
@@ -33,6 +34,7 @@ public abstract class Node : INode {
 
   protected IReadOnlyList<IToken> OwnedTokensCache;
 
+  public virtual bool SingleFileToken => true;
   public IToken StartToken => RangeToken?.StartToken;
 
   public IToken EndToken => RangeToken?.EndToken;

Source/DafnyCore/Generic/NodeExtensions.cs

@@ -129,7 +129,9 @@ private static LList<INode> FindNodeChain(this INode node, Uri uri, DafnyPositio
         return node.FindNodeChain(position, parent, predicate);
       }
 
-      return null;
+      if (node.SingleFileToken) {
+        return null;
+      }
     }
 
     var newParent = new LList<INode>(node, parent);

Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs

@@ -15,6 +15,27 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization;
 
 public class VerificationStatusTest : ClientBasedLanguageServerTest {
 
+  [Fact]
+  public async Task ParentModuleProjectFileVerification() {
+
+    await SetUp(options => {
+      options.Set(ProjectManager.Verification, VerifyOnMode.Never);
+    });
+    var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
+    Directory.CreateDirectory(directory);
+    await File.WriteAllTextAsync(Path.Combine(directory, "dfyconfig.toml"), "");
+    await File.WriteAllTextAsync(Path.Combine(directory, "a.dfy"), "module A {}");
+    // var project = CreateAndOpenTestDocument("", Path.Combine(directory, "dfyconfig.toml"));
+    // var a = CreateAndOpenTestDocument("module A {}", Path.Combine(directory, "a.dfy"));
+    var b = CreateAndOpenTestDocument("module A.B { \n  method Test() { assert true; }\n}", Path.Combine(directory, "b.dfy"));
+
+    var methodHeader = new Position(1, 11);
+    verificationStatusReceiver.GetLatestAndClearQueue(_ => true);
+    await client.RunSymbolVerification(new TextDocumentIdentifier(b.Uri), methodHeader, CancellationToken);
+    var result = await WaitUntilAllStatusAreCompleted(b);
+    Assert.Equal(PublishedVerificationStatus.Correct, result.NamedVerifiables[0].Status);
+  }
+
   /// <summary>
   /// The client does not correctly migrate symbolStatus information,
   /// so we have to republish it if the positions change.

docs/dev/news/5650.fix

@@ -0,0 +1 @@
+Verification in the IDE now works correctly when declaring nested module in a different file than their parent.