Improve code navigation around import declarations with no explicit n…

…ame (#5419)

### Description
- Improve code navigation for around import declaration with no explicit
name

### 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/AstVisitor.cs

@@ -328,12 +328,12 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) {
         // Visit user-provided types
         if (stmt is VarDeclStmt varDeclStmt) {
           foreach (var local in varDeclStmt.Locals) {
-            VisitUserProvidedType(local.OptionalType, context);
+            VisitUserProvidedType(local.SyntacticType, context);
           }
 
         } else if (stmt is VarDeclPattern varDeclPattern) {
           foreach (var local in varDeclPattern.LocalVars) {
-            VisitUserProvidedType(local.OptionalType, context);
+            VisitUserProvidedType(local.SyntacticType, context);
           }
 
         } else if (stmt is AssignStmt assignStmt) {

Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs

@@ -94,7 +94,7 @@ public string AssignUniqueName(FreshIdGenerator generator) {
   }
 
   public abstract IToken NameToken { get; }
-  public SymbolKind Kind => throw new NotImplementedException();
+  public SymbolKind? Kind => throw new NotImplementedException();
   public string GetDescription(DafnyOptions options) {
     throw new NotImplementedException();
   }

Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs

@@ -8,6 +8,17 @@ namespace Microsoft.Dafny;
 public abstract class NonglobalVariable : TokenNode, IVariable {
   readonly string name;
 
+  protected NonglobalVariable(IToken tok, string name, Type type, bool isGhost) {
+    Contract.Requires(tok != null);
+    Contract.Requires(name != null);
+    Contract.Requires(type != null);
+    this.tok = tok;
+    this.name = name;
+    IsTypeExplicit = type != null;
+    this.type = type ?? new InferredTypeProxy();
+    this.isGhost = isGhost;
+  }
+
   [ContractInvariantMethod]
   void ObjectInvariant() {
     Contract.Invariant(name != null);
@@ -88,7 +99,7 @@ public static string SanitizeName(string nm) {
     compileName ??= SanitizedName;
 
   Type type;
-  public bool IsTypeExplicit = false;
+  public bool IsTypeExplicit { get; set; }
   public Type SyntacticType { get { return type; } }  // returns the non-normalized type
   public PreType PreType { get; set; }
 
@@ -127,20 +138,10 @@ public void MakeGhost() {
     IsGhost = true;
   }
 
-  public NonglobalVariable(IToken tok, string name, Type type, bool isGhost) {
-    Contract.Requires(tok != null);
-    Contract.Requires(name != null);
-    Contract.Requires(type != null);
-    this.tok = tok;
-    this.name = name;
-    this.type = type;
-    this.isGhost = isGhost;
-  }
-
   public IToken NameToken => tok;
   public override IEnumerable<INode> Children => IsTypeExplicit ? new List<Node> { Type } : Enumerable.Empty<Node>();
   public override IEnumerable<INode> PreResolveChildren => IsTypeExplicit ? new List<Node>() { Type } : Enumerable.Empty<Node>();
-  public SymbolKind Kind => SymbolKind.Variable;
+  public SymbolKind? Kind => SymbolKind.Variable;
   public string GetDescription(DafnyOptions options) {
     return this.AsText();
   }

Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs

@@ -402,7 +402,7 @@ public void PrintStatement(Statement stmt, int indent) {
             PrintAttributes(local.Attributes);
           }
           wr.Write(" {0}", local.DisplayName);
-          PrintType(": ", local.OptionalType);
+          PrintType(": ", local.SyntacticType);
           sep = ",";
         }
         if (s.Update != null) {

Source/DafnyCore/AST/IHasUsages.cs

@@ -60,7 +60,7 @@ public static string AsText(this IVariable variable) {
 }
 
 public interface ISymbol : IDeclarationOrUsage {
-  SymbolKind Kind { get; }
+  SymbolKind? Kind { get; }
 
   string GetDescription(DafnyOptions options);
 }

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -47,7 +47,7 @@ public bool InferredDecreases {
   public bool AllowsAllocation => true;
 
   public override IEnumerable<INode> Children => base.Children.Concat(new[] { Rhs }.Where(x => x != null));
-  public override SymbolKind Kind => SymbolKind.Constant;
+  public override SymbolKind? Kind => SymbolKind.Constant;
 
   public override IEnumerable<INode> PreResolveChildren => Children;
   public ModuleDefinition ContainingModule => EnclosingModule;

Source/DafnyCore/AST/Members/Constructor.cs

@@ -11,7 +11,7 @@ void ObjectInvariant() {
     Contract.Invariant(Body == null || Body is DividedBlockStmt);
   }
 
-  public override SymbolKind Kind => SymbolKind.Constructor;
+  public override SymbolKind? Kind => SymbolKind.Constructor;
   protected override string GetQualifiedName() {
     return EnclosingClass.Name;
   }

Source/DafnyCore/AST/Members/Field.cs

@@ -96,7 +96,7 @@ public string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public virtual SymbolKind Kind => SymbolKind.Field;
+  public virtual SymbolKind? Kind => SymbolKind.Field;
 
   public string GetDescription(DafnyOptions options) {
     var prefix = IsMutable ? "var" : "const";

Source/DafnyCore/AST/Members/Function.cs

@@ -482,7 +482,7 @@ public string GetTriviaContainingDocstring() {
     return null;
   }
 
-  public SymbolKind Kind => SymbolKind.Function;
+  public SymbolKind? Kind => SymbolKind.Function;
   public bool ShouldVerify => true; // This could be made more accurate
   public ModuleDefinition ContainingModule => EnclosingClass.EnclosingModuleDefinition;
   public string GetDescription(DafnyOptions options) {
@@ -491,22 +491,22 @@ public string GetDescription(DafnyOptions options) {
     return $"{WhatKind} {AstExtensions.GetMemberQualification(this)}{Name}({formals}): {resultType}";
   }
 
-  public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, DafnyOptions Options,
-    ErrorReporter Reporter) {
+  public void AutoRevealDependencies(AutoRevealFunctionDependencies rewriter, DafnyOptions options,
+    ErrorReporter reporter) {
     if (Body is null) {
       return;
     }
 
     if (ByMethodDecl is not null) {
-      ByMethodDecl.AutoRevealDependencies(Rewriter, Options, Reporter);
+      ByMethodDecl.AutoRevealDependencies(rewriter, options, reporter);
     }
 
     object autoRevealDepsVal = null;
     bool autoRevealDeps = Attributes.ContainsMatchingValue(Attributes, "autoRevealDependencies",
       ref autoRevealDepsVal, new List<Attributes.MatchingValueOption> {
         Attributes.MatchingValueOption.Bool,
         Attributes.MatchingValueOption.Int
-      }, s => Reporter.Error(MessageSource.Rewriter, ErrorLevel.Error, Tok, s));
+      }, s => reporter.Error(MessageSource.Rewriter, ErrorLevel.Error, Tok, s));
 
     // Default behavior is reveal all dependencies
     int autoRevealDepth = int.MaxValue;
@@ -522,7 +522,7 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
     var currentClass = EnclosingClass;
     List<AutoRevealFunctionDependencies.RevealStmtWithDepth> addedReveals = new();
 
-    foreach (var func in Rewriter.GetEnumerator(this, currentClass, SubExpressions)) {
+    foreach (var func in rewriter.GetEnumerator(this, currentClass, SubExpressions)) {
       var revealStmt =
         AutoRevealFunctionDependencies.BuildRevealStmt(func.Function, Tok, EnclosingClass.EnclosingModuleDefinition);
 
@@ -558,7 +558,7 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
     }
 
     if (addedReveals.Any()) {
-      Reporter.Message(MessageSource.Rewriter, ErrorLevel.Info, null, tok,
+      reporter.Message(MessageSource.Rewriter, ErrorLevel.Info, null, tok,
         AutoRevealFunctionDependencies.GenerateMessage(addedReveals, autoRevealDepth));
     }
   }

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -94,7 +94,7 @@ public bool InferredDecreases {
   public IEnumerable<IToken> OwnedTokens => CwInner.OwnedTokens;
   public RangeToken RangeToken => CwInner.RangeToken;
   public IToken NameToken => CwInner.NameToken;
-  public SymbolKind Kind => CwInner.Kind;
+  public SymbolKind? Kind => CwInner.Kind;
   public string GetDescription(DafnyOptions options) {
     return CwInner.GetDescription(options);
   }
@@ -130,7 +130,7 @@ public IEnumerable<INode> GetConcreteChildren() {
   public IEnumerable<IToken> OwnedTokens => throw new cce.UnreachableException();
   public RangeToken RangeToken => throw new cce.UnreachableException();
   public IToken NameToken => throw new cce.UnreachableException();
-  public SymbolKind Kind => throw new cce.UnreachableException();
+  public SymbolKind? Kind => throw new cce.UnreachableException();
   public string GetDescription(DafnyOptions options) {
     throw new cce.UnreachableException();
   }

Source/DafnyCore/AST/Members/Method.cs

@@ -394,7 +394,7 @@ public string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public virtual SymbolKind Kind => SymbolKind.Method;
+  public virtual SymbolKind? Kind => SymbolKind.Method;
   public string GetDescription(DafnyOptions options) {
     var qualifiedName = GetQualifiedName();
     var signatureWithoutReturn = $"{WhatKind} {qualifiedName}({string.Join(", ", Ins.Select(i => i.AsText()))})";

Source/DafnyCore/AST/Modules/AliasModuleDecl.cs

@@ -3,6 +3,7 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using Microsoft.CodeAnalysis;
+using SymbolKind = OmniSharp.Extensions.LanguageServer.Protocol.Models.SymbolKind;
 
 namespace Microsoft.Dafny;
 
@@ -50,5 +51,22 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     return true;
   }
 
+  /// <summary>
+  /// If no explicit name is given for an import declaration,
+  /// Then we consider this as a reference, not a declaration, from the IDE perspective.
+  /// So any further references to the imported module then resolve directly to the module,
+  /// Not to this import declaration.
+  ///
+  /// Code wise, it might be better not to let AliasModuleDecl inherit from Declaration,
+  /// since it is not always a declaration. 
+  /// </summary>
+  public override IToken NameToken => HasAlias ? base.NameToken : TargetQId.Decl.NameToken;
+
+  private bool HasAlias => NameNode.RangeToken.IsSet();
+
+  public override IToken Tok => HasAlias ? NameNode.StartToken : StartToken;
+
+  public override SymbolKind? Kind => !HasAlias ? null : base.Kind;
+
   public override IEnumerable<INode> Children => base.Children.Concat(new INode[] { TargetQId });
 }

Source/DafnyCore/AST/Modules/ModuleDecl.cs

@@ -81,7 +81,7 @@ public virtual string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public SymbolKind Kind => SymbolKind.Namespace;
+  public virtual SymbolKind? Kind => SymbolKind.Namespace;
   public string GetDescription(DafnyOptions options) {
     return $"module {Name}";
   }

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -1049,7 +1049,7 @@ bool InheritsFromObject(TraitDecl traitDecl) {
     return Enumerable.Empty<ISymbol>();
   });
 
-  public SymbolKind Kind => SymbolKind.Namespace;
+  public SymbolKind? Kind => SymbolKind.Namespace;
   public string GetDescription(DafnyOptions options) {
     return $"module {Name}";
   }

Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs

@@ -14,15 +14,15 @@ public class LocalVariable : RangeNode, IVariable, IAttributeBearingDeclaration
   [ContractInvariantMethod]
   void ObjectInvariant() {
     Contract.Invariant(name != null);
-    Contract.Invariant(OptionalType != null);
+    Contract.Invariant(SyntacticType != null);
   }
 
   public override IToken Tok => RangeToken.StartToken;
 
   public LocalVariable(Cloner cloner, LocalVariable original)
     : base(cloner, original) {
     name = original.Name;
-    OptionalType = cloner.CloneType(original.OptionalType);
+    SyntacticType = cloner.CloneType(original.SyntacticType);
     IsTypeExplicit = original.IsTypeExplicit;
     IsGhost = original.IsGhost;
 
@@ -37,7 +37,8 @@ public LocalVariable(RangeToken rangeToken, string name, Type type, bool isGhost
     Contract.Requires(type != null);  // can be a proxy, though
 
     this.name = name;
-    this.OptionalType = type;
+    IsTypeExplicit = type != null;
+    this.SyntacticType = type ?? new InferredTypeProxy();
     if (type is InferredTypeProxy) {
       ((InferredTypeProxy)type).KeepConstraints = true;
     }
@@ -82,8 +83,9 @@ public string AssignUniqueName(FreshIdGenerator generator) {
   public string CompileName =>
     compileName ??= SanitizedName;
 
-  public readonly Type OptionalType;  // this is the type mentioned in the declaration, if any
-  Type IVariable.OptionalType { get { return this.OptionalType; } }
+  // TODO rename and update comment? Or make it nullable?
+  public readonly Type SyntacticType;  // this is the type mentioned in the declaration, if any
+  Type IVariable.OptionalType => SyntacticType;
 
   [FilledInDuringResolution]
   internal Type type;  // this is the declared or inferred type of the variable; it is non-null after resolution (even if resolution fails)
@@ -128,16 +130,16 @@ public void MakeGhost() {
   }
 
   public IToken NameToken => RangeToken.StartToken;
-  public bool IsTypeExplicit = false;
+  public bool IsTypeExplicit { get; }
   public override IEnumerable<INode> Children =>
     (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>()).Concat(
       IsTypeExplicit ? new List<Node>() { type } : Enumerable.Empty<Node>());
 
   public override IEnumerable<INode> PreResolveChildren =>
     (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>()).Concat(
-      IsTypeExplicit ? new List<Node>() { OptionalType ?? type } : Enumerable.Empty<Node>());
+      IsTypeExplicit ? new List<Node>() { SyntacticType ?? type } : Enumerable.Empty<Node>());
 
-  public SymbolKind Kind => SymbolKind.Variable;
+  public SymbolKind? Kind => SymbolKind.Variable;
   public string GetDescription(DafnyOptions options) {
     return this.AsText();
   }

Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs

@@ -24,6 +24,9 @@ public override IToken Tok {
   [FilledInDuringResolution] public List<Statement> ResolvedStatements;
   public override IEnumerable<Statement> SubStatements => Children.OfType<Statement>();
 
+  public override IEnumerable<Expression> NonSpecificationSubExpressions =>
+    ResolvedStatements == null ? Rhss.SelectMany(r => r.NonSpecificationSubExpressions) : Enumerable.Empty<Expression>();
+
   public override IEnumerable<INode> Children => ResolvedStatements ?? Lhss.Concat<Node>(Rhss);
   public override IEnumerable<INode> PreResolveChildren => Lhss.Concat<Node>(Rhss);
 
@@ -63,6 +66,7 @@ public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentR
     Rhss = rhss;
     CanMutateKnownState = mutate;
   }
+
   public override IEnumerable<Expression> PreResolveSubExpressions {
     get {
       foreach (var e in base.PreResolveSubExpressions) {

Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs

@@ -43,12 +43,6 @@ public override IEnumerable<Expression> SpecificationSubExpressions {
           yield return e;
         }
       }
-
-      if (this.Update != null) {
-        foreach (var e in this.Update.NonSpecificationSubExpressions) {
-          yield return e;
-        }
-      }
     }
   }
 

Source/DafnyCore/AST/Substituter.cs

@@ -595,8 +595,8 @@ protected virtual List<LocalVariable> CreateLocalVarSubstitutions(List<LocalVari
       bool anythingChanged = false;
       var newVars = new List<LocalVariable>();
       foreach (var v in vars) {
-        var tt = v.OptionalType.Subst(typeMap);
-        if (!forceSubstitutionOfVars && tt == v.OptionalType) {
+        var tt = v.SyntacticType.Subst(typeMap);
+        if (!forceSubstitutionOfVars && tt == v.SyntacticType) {
           newVars.Add(v);
         } else {
           anythingChanged = true;

Source/DafnyCore/AST/Tokens.cs

@@ -205,6 +205,9 @@ public int CompareTo(Boogie.IToken other) {
 
 public static class TokenExtensions {
 
+
+  public static bool IsSet(this IToken token) => token.Uri != null;
+
   public static string TokenToString(this IToken tok, DafnyOptions options) {
     if (tok == Token.Cli) {
       return "CLI";

Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs

@@ -50,7 +50,7 @@ public string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public SymbolKind Kind => SymbolKind.EnumMember;
+  public SymbolKind? Kind => SymbolKind.EnumMember;
   public string GetDescription(DafnyOptions options) {
     var formals = string.Join(", ", Formals.Select(f => f.AsText()));
     return $"{EnclosingDatatype.Name}.{Name}({formals})";

Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs

@@ -82,7 +82,7 @@ public override bool IsEssentiallyEmpty() {
   }
 
   public override IEnumerable<ISymbol> ChildSymbols => base.ChildSymbols.Concat(Ctors);
-  public override SymbolKind Kind => SymbolKind.Enum;
+  public override SymbolKind? Kind => SymbolKind.Enum;
 
   public bool SetIndent(int indent, TokenNewIndentCollector formatter) {
     var indent2 = indent + formatter.SpaceTab;

Source/DafnyCore/AST/TypeDeclarations/Declaration.cs

@@ -16,7 +16,7 @@ void ObjectInvariant() {
   public Name NameNode;
 
   public override IToken Tok => NameNode.StartToken;
-  public IToken NameToken => NameNode.StartToken;
+  public virtual IToken NameToken => NameNode.StartToken;
 
   public string Name => NameNode.Value;
   public bool IsRefining;

Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs

@@ -67,7 +67,7 @@ public IteratorDecl(RangeToken rangeToken, Name name, ModuleDefinition module, L
     DecreasesFields = new List<Field>();
 
     YieldCountVariable = new LocalVariable(rangeToken, "_yieldCount", new EverIncreasingType(), true);
-    YieldCountVariable.type = YieldCountVariable.OptionalType;  // resolve YieldCountVariable here
+    YieldCountVariable.type = YieldCountVariable.SyntacticType;  // resolve YieldCountVariable here
   }
 
   /// <summary>