Unreferenced declaration (dafny-lang#5483)

### Description
- Renamed `IHasUsages` to `IHasReferences`, to be more in line with LSP
naming
- Renamed `IDeclarationOrUsage` to `IHasNavigationToken`, and its member
`NameToken` to `NavigationToken`
- Respect the `request.Context.IncludeDeclaration` value of the LSP
references request
- Enable renaming declarations that were not referred to

### How has this been tested?
- Added tests for renaming and finding references on a declaration that
is not referred to

<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.Test/ClonerTest.cs

@@ -1,6 +1,7 @@
 using Microsoft.Dafny;
 using Microsoft.Extensions.Logging;
 using Microsoft.Extensions.Logging.Abstractions;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Tomlyn;
 
 namespace DafnyCore.Test;
@@ -13,6 +14,11 @@ public DummyDecl(Cloner cloner, Declaration original) : base(cloner, original) {
     public DummyDecl(RangeToken rangeToken, Name name, Attributes attributes, bool isRefining) : base(rangeToken, name,
       attributes, isRefining) {
     }
+
+    public override SymbolKind? Kind => null;
+    public override string GetDescription(DafnyOptions options) {
+      return "";
+    }
   }
 
   [Fact]

Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs

@@ -4,7 +4,7 @@
 
 namespace Microsoft.Dafny;
 
-public class FunctionCallExpr : Expression, IHasUsages, ICloneable<FunctionCallExpr> {
+public class FunctionCallExpr : Expression, IHasReferences, ICloneable<FunctionCallExpr> {
   public string Name;
   public readonly Expression Receiver;
   public readonly IToken OpenParen;  // can be null if Args.Count == 0
@@ -144,9 +144,9 @@ public override IEnumerable<Expression> SubExpressions {
   }
 
   public override IEnumerable<Type> ComponentTypes => Util.Concat(TypeApplication_AtEnclosingClass, TypeApplication_JustFunction);
-  public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
+  public IEnumerable<IHasNavigationToken> GetReferences() {
     return Enumerable.Repeat(Function, 1);
   }
 
-  public IToken NameToken => tok;
+  public IToken NavigationToken => tok;
 }

Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs

@@ -4,7 +4,7 @@
 
 namespace Microsoft.Dafny;
 
-public class MemberSelectExpr : Expression, IHasUsages, ICloneable<MemberSelectExpr> {
+public class MemberSelectExpr : Expression, IHasReferences, ICloneable<MemberSelectExpr> {
   public readonly Expression Obj;
   public string MemberName;
   [FilledInDuringResolution] public MemberDecl Member;    // will be a Field or Function
@@ -294,9 +294,9 @@ public override IEnumerable<Expression> SubExpressions {
 
   [FilledInDuringResolution] public List<Type> ResolvedOutparameterTypes;
 
-  public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
+  public IEnumerable<IHasNavigationToken> GetReferences() {
     return new[] { Member };
   }
 
-  public IToken NameToken => tok;
+  public IToken NavigationToken => tok;
 }

Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs

@@ -8,7 +8,7 @@
 
 namespace Microsoft.Dafny;
 
-public class IdPattern : ExtendedPattern, IHasUsages {
+public class IdPattern : ExtendedPattern, IHasReferences {
   public bool HasParenthesis { get; }
   public String Id;
   public PreType PreType;
@@ -131,11 +131,11 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
     }
   }
 
-  public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
-    return new IDeclarationOrUsage[] { Ctor }.Where(x => x != null);
+  public IEnumerable<IHasNavigationToken> GetReferences() {
+    return new ISymbol[] { Ctor }.Where(x => x != null);
   }
 
-  public IToken NameToken => Tok;
+  public IToken NavigationToken => Tok;
 
   public void CheckLinearVarPattern(Type type, ResolutionContext resolutionContext, ModuleResolver resolver) {
     if (Arguments != null) {

Source/DafnyCore/AST/Expressions/Datatypes/DatatypeUpdateExpr.cs

@@ -5,7 +5,7 @@
 
 namespace Microsoft.Dafny;
 
-public class DatatypeUpdateExpr : ConcreteSyntaxExpression, IHasUsages, ICloneable<DatatypeUpdateExpr> {
+public class DatatypeUpdateExpr : ConcreteSyntaxExpression, IHasReferences, ICloneable<DatatypeUpdateExpr> {
   public readonly Expression Root;
   public readonly List<Tuple<IToken, string, Expression>> Updates;
   [FilledInDuringResolution] public List<MemberDecl> Members;
@@ -62,11 +62,11 @@ public override IEnumerable<Expression> SubExpressions {
     }
   }
 
-  public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
-    return (IEnumerable<IDeclarationOrUsage>)LegalSourceConstructors ?? Array.Empty<IDeclarationOrUsage>();
+  public IEnumerable<IHasNavigationToken> GetReferences() {
+    return (IEnumerable<ISymbol>)LegalSourceConstructors ?? Array.Empty<ISymbol>();
   }
 
-  public IToken NameToken => tok;
+  public IToken NavigationToken => tok;
 
   public override IEnumerable<Expression> PreResolveSubExpressions {
     get {

Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs

@@ -4,7 +4,7 @@
 
 namespace Microsoft.Dafny;
 
-public class DatatypeValue : Expression, IHasUsages, ICloneable<DatatypeValue>, ICanFormat {
+public class DatatypeValue : Expression, IHasReferences, ICloneable<DatatypeValue>, ICanFormat {
   public readonly string DatatypeName;
   public readonly string MemberName;
   public readonly ActualBindings Bindings;
@@ -64,11 +64,11 @@ public DatatypeValue(IToken tok, string datatypeName, string memberName, List<Ex
   public override IEnumerable<Expression> SubExpressions =>
     Arguments ?? Enumerable.Empty<Expression>();
 
-  public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
+  public IEnumerable<IHasNavigationToken> GetReferences() {
     return Enumerable.Repeat(Ctor, 1);
   }
 
-  public IToken NameToken => tok;
+  public IToken NavigationToken => tok;
   public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     formatter.SetMethodLikeIndent(StartToken, OwnedTokens, indentBefore);
     return true;

Source/DafnyCore/AST/Expressions/Heap/FrameExpression.cs

@@ -4,7 +4,7 @@
 
 namespace Microsoft.Dafny;
 
-public class FrameExpression : TokenNode, IHasUsages {
+public class FrameExpression : TokenNode, IHasReferences {
   public readonly Expression OriginalExpression; // may be a WildcardExpr
   [FilledInDuringResolution] public Expression DesugaredExpression; // may be null for modifies clauses, even after resolution
 
@@ -48,10 +48,10 @@ public FrameExpression(Cloner cloner, FrameExpression original) {
     }
   }
 
-  public IToken NameToken => tok;
+  public IToken NavigationToken => tok;
   public override IEnumerable<INode> Children => new[] { E };
   public override IEnumerable<INode> PreResolveChildren => Children;
-  public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
+  public IEnumerable<IHasNavigationToken> GetReferences() {
     return new[] { Field }.Where(x => x != null);
   }
 }

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

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

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

@@ -4,7 +4,7 @@
 
 namespace Microsoft.Dafny;
 
-public class IdentifierExpr : Expression, IHasUsages, ICloneable<IdentifierExpr> {
+public class IdentifierExpr : Expression, IHasReferences, ICloneable<IdentifierExpr> {
   [ContractInvariantMethod]
   void ObjectInvariant() {
     Contract.Invariant(Name != null);
@@ -52,11 +52,11 @@ public static bool Is(Expression expr, IVariable variable) {
     return expr.Resolved is IdentifierExpr identifierExpr && identifierExpr.Var == variable;
   }
 
-  public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
+  public IEnumerable<IHasNavigationToken> GetReferences() {
     return Enumerable.Repeat(Var, 1);
   }
 
-  public IToken NameToken => tok;
+  public IToken NavigationToken => tok;
   public override IEnumerable<INode> Children { get; } = Enumerable.Empty<Node>();
 }
 

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

@@ -138,7 +138,7 @@ public void MakeGhost() {
     IsGhost = true;
   }
 
-  public IToken NameToken => tok;
+  public IToken NavigationToken => 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;

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

@@ -8,7 +8,7 @@ namespace Microsoft.Dafny;
 /// <summary>
 /// This class is used only inside the resolver itself. It gets hung in the AST in uncompleted name segments.
 /// </summary>
-class Resolver_IdentifierExpr : Expression, IHasUsages, ICloneable<Resolver_IdentifierExpr> {
+class Resolver_IdentifierExpr : Expression, IHasReferences, ICloneable<Resolver_IdentifierExpr> {
   public readonly TopLevelDecl Decl;
   public readonly List<Type> TypeArgs;
   [ContractInvariantMethod]
@@ -75,11 +75,11 @@ public Resolver_IdentifierExpr(IToken tok, TypeParameter tp)
     Contract.Requires(tp != null);
   }
 
-  public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
+  public IEnumerable<IHasNavigationToken> GetReferences() {
     return new[] { Decl };
   }
 
-  public IToken NameToken => tok;
+  public IToken NavigationToken => tok;
   public Resolver_IdentifierExpr Clone(Cloner cloner) {
     return new Resolver_IdentifierExpr(cloner, this);
   }

Source/DafnyCore/AST/IHasUsages.cs → Source/DafnyCore/AST/IHasReferences.cs

@@ -5,12 +5,15 @@
 
 namespace Microsoft.Dafny;
 
-public interface IDeclarationOrUsage : INode {
-  IToken NameToken { get; }
+/// <summary>
+/// Node that has a token that is used to navigate to this node
+/// </summary>
+public interface IHasNavigationToken : INode {
+  IToken NavigationToken { get; }
 }
 
-public interface IHasUsages : IDeclarationOrUsage {
-  public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations();
+public interface IHasReferences : IHasNavigationToken {
+  public IEnumerable<IHasNavigationToken> GetReferences();
 }
 
 /// <summary>
@@ -59,7 +62,7 @@ public static string AsText(this IVariable variable) {
   }
 }
 
-public interface ISymbol : IDeclarationOrUsage {
+public interface ISymbol : IHasNavigationToken {
   SymbolKind? Kind { get; }
 
   string GetDescription(DafnyOptions options);

Source/DafnyCore/AST/Members/Field.cs

@@ -5,7 +5,7 @@
 
 namespace Microsoft.Dafny;
 
-public class Field : MemberDecl, ICanFormat, IHasDocstring, ISymbol {
+public class Field : MemberDecl, ICanFormat, IHasDocstring {
   public override string WhatKind => "field";
   public readonly bool IsMutable;  // says whether or not the field can ever change values
   public readonly bool IsUserMutable;  // says whether or not code is allowed to assign to the field (IsUserMutable implies IsMutable)
@@ -96,9 +96,9 @@ public string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public virtual SymbolKind? Kind => SymbolKind.Field;
+  public override SymbolKind? Kind => SymbolKind.Field;
 
-  public string GetDescription(DafnyOptions options) {
+  public override string GetDescription(DafnyOptions options) {
     var prefix = IsMutable ? "var" : "const";
     return $"{prefix} {AstExtensions.GetMemberQualification(this)}{Name}: {Type}";
   }

Source/DafnyCore/AST/Members/Function.cs

@@ -482,10 +482,10 @@ public string GetTriviaContainingDocstring() {
     return null;
   }
 
-  public SymbolKind? Kind => SymbolKind.Function;
+  public override SymbolKind? Kind => SymbolKind.Function;
   public bool ShouldVerify => true; // This could be made more accurate
   public ModuleDefinition ContainingModule => EnclosingClass.EnclosingModuleDefinition;
-  public string GetDescription(DafnyOptions options) {
+  public override string GetDescription(DafnyOptions options) {
     var formals = string.Join(", ", Ins.Select(f => f.AsText()));
     var resultType = ResultType.TypeName(options, null, false);
     return $"{WhatKind} {AstExtensions.GetMemberQualification(this)}{Name}({formals}): {resultType}";

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -93,7 +93,7 @@ public bool InferredDecreases {
 
   public IEnumerable<IToken> OwnedTokens => CwInner.OwnedTokens;
   public RangeToken RangeToken => CwInner.RangeToken;
-  public IToken NameToken => CwInner.NameToken;
+  public IToken NavigationToken => CwInner.NavigationToken;
   public SymbolKind? Kind => CwInner.Kind;
   public string GetDescription(DafnyOptions options) {
     return CwInner.GetDescription(options);
@@ -129,7 +129,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 IToken NavigationToken => throw new cce.UnreachableException();
   public SymbolKind? Kind => throw new cce.UnreachableException();
   public string GetDescription(DafnyOptions options) {
     throw new cce.UnreachableException();

Source/DafnyCore/AST/Members/MemberDecl.cs

@@ -2,10 +2,11 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using Microsoft.Dafny.Auditor;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
-public abstract class MemberDecl : Declaration {
+public abstract class MemberDecl : Declaration, ISymbol {
   public abstract string WhatKind { get; }
   public string WhatKindAndName => $"{WhatKind} '{Name}'";
   public virtual string WhatKindMentionGhost => (IsGhost ? "ghost " : "") + WhatKind;

Source/DafnyCore/AST/Members/Method.cs

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

Source/DafnyCore/AST/Modules/AliasModuleDecl.cs

@@ -60,7 +60,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
   /// 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;
+  public override IToken NavigationToken => HasAlias ? base.NavigationToken : (TargetQId.Decl?.NavigationToken ?? base.NavigationToken);
 
   private bool HasAlias => NameNode.RangeToken.IsSet();
 

Source/DafnyCore/AST/Modules/ExportSignature.cs

@@ -4,7 +4,7 @@
 
 namespace Microsoft.Dafny;
 
-public class ExportSignature : TokenNode, IHasUsages {
+public class ExportSignature : TokenNode, IHasReferences {
   public readonly IToken ClassIdTok;
   public readonly bool Opaque;
   public readonly string ClassId;
@@ -57,10 +57,10 @@ public override string ToString() {
     return Id;
   }
 
-  public IToken NameToken => Tok;
+  public IToken NavigationToken => Tok;
   public override IEnumerable<INode> Children => Enumerable.Empty<Node>();
   public override IEnumerable<INode> PreResolveChildren => Enumerable.Empty<Node>();
-  public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
+  public IEnumerable<IHasNavigationToken> GetReferences() {
     return new[] { Decl };
   }
 }

Source/DafnyCore/AST/Modules/ModuleDecl.cs

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

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -381,7 +381,7 @@ public bool IsEssentiallyEmptyModuleBody() {
     return TopLevelDecls.All(decl => decl.IsEssentiallyEmpty());
   }
 
-  public IToken NameToken => tok;
+  public IToken NavigationToken => tok;
   public override IEnumerable<INode> Children =>
     (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>()).
     Concat(DefaultClasses).