diff --git a/Source/DafnyCore/AST/AstVisitor.cs b/Source/DafnyCore/AST/AstVisitor.cs index b0aae35dc8d..cf1388b50d9 100644 --- a/Source/DafnyCore/AST/AstVisitor.cs +++ b/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) { diff --git a/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs b/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs index 9ebe8a5af79..a6d07e90efd 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs +++ b/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(); } diff --git a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs index 98c24af35d7..d32968c0d1d 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs +++ b/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 Children => IsTypeExplicit ? new List { Type } : Enumerable.Empty(); public override IEnumerable PreResolveChildren => IsTypeExplicit ? new List() { Type } : Enumerable.Empty(); - public SymbolKind Kind => SymbolKind.Variable; + public SymbolKind? Kind => SymbolKind.Variable; public string GetDescription(DafnyOptions options) { return this.AsText(); } diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs index 151ac8a0037..57143782976 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs +++ b/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) { diff --git a/Source/DafnyCore/AST/IHasUsages.cs b/Source/DafnyCore/AST/IHasUsages.cs index 31c31f280a0..8a97a081785 100644 --- a/Source/DafnyCore/AST/IHasUsages.cs +++ b/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); } diff --git a/Source/DafnyCore/AST/Members/ConstantField.cs b/Source/DafnyCore/AST/Members/ConstantField.cs index 7ec15279603..490443f42f2 100644 --- a/Source/DafnyCore/AST/Members/ConstantField.cs +++ b/Source/DafnyCore/AST/Members/ConstantField.cs @@ -47,7 +47,7 @@ public bool InferredDecreases { public bool AllowsAllocation => true; public override IEnumerable 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 PreResolveChildren => Children; public ModuleDefinition ContainingModule => EnclosingModule; diff --git a/Source/DafnyCore/AST/Members/Constructor.cs b/Source/DafnyCore/AST/Members/Constructor.cs index 7c8b2b7bb4e..b40feeaf963 100644 --- a/Source/DafnyCore/AST/Members/Constructor.cs +++ b/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; } diff --git a/Source/DafnyCore/AST/Members/Field.cs b/Source/DafnyCore/AST/Members/Field.cs index eaf9aa29b1a..1666563b6bb 100644 --- a/Source/DafnyCore/AST/Members/Field.cs +++ b/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"; diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs index 2c1beeb1069..49523e37ffe 100644 --- a/Source/DafnyCore/AST/Members/Function.cs +++ b/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,14 +491,14 @@ 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; @@ -506,7 +506,7 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn ref autoRevealDepsVal, new List { 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 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)); } } diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs index b314efc9bd0..639ae230e50 100644 --- a/Source/DafnyCore/AST/Members/ICodeContext.cs +++ b/Source/DafnyCore/AST/Members/ICodeContext.cs @@ -94,7 +94,7 @@ public bool InferredDecreases { public IEnumerable 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 GetConcreteChildren() { public IEnumerable 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(); } diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs index 1d615e908a7..ca6965ca10d 100644 --- a/Source/DafnyCore/AST/Members/Method.cs +++ b/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()))})"; diff --git a/Source/DafnyCore/AST/Modules/AliasModuleDecl.cs b/Source/DafnyCore/AST/Modules/AliasModuleDecl.cs index 29fe792fba8..44da2e453fe 100644 --- a/Source/DafnyCore/AST/Modules/AliasModuleDecl.cs +++ b/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; } + /// + /// 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. + /// + 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 Children => base.Children.Concat(new INode[] { TargetQId }); } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Modules/ModuleDecl.cs b/Source/DafnyCore/AST/Modules/ModuleDecl.cs index 588913b92a4..5b28afe6419 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDecl.cs +++ b/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}"; } diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 7a0514e757b..e0372cd9e8e 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -1049,7 +1049,7 @@ bool InheritsFromObject(TraitDecl traitDecl) { return Enumerable.Empty(); }); - public SymbolKind Kind => SymbolKind.Namespace; + public SymbolKind? Kind => SymbolKind.Namespace; public string GetDescription(DafnyOptions options) { return $"module {Name}"; } diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs index 880044f70ee..551a8ed1737 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs @@ -14,7 +14,7 @@ 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; @@ -22,7 +22,7 @@ void ObjectInvariant() { 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 Children => (Attributes != null ? new List { Attributes } : Enumerable.Empty()).Concat( IsTypeExplicit ? new List() { type } : Enumerable.Empty()); public override IEnumerable PreResolveChildren => (Attributes != null ? new List { Attributes } : Enumerable.Empty()).Concat( - IsTypeExplicit ? new List() { OptionalType ?? type } : Enumerable.Empty()); + IsTypeExplicit ? new List() { SyntacticType ?? type } : Enumerable.Empty()); - public SymbolKind Kind => SymbolKind.Variable; + public SymbolKind? Kind => SymbolKind.Variable; public string GetDescription(DafnyOptions options) { return this.AsText(); } diff --git a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs index e4d22f33497..cc3fe0507f1 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs @@ -24,6 +24,9 @@ public override IToken Tok { [FilledInDuringResolution] public List ResolvedStatements; public override IEnumerable SubStatements => Children.OfType(); + public override IEnumerable NonSpecificationSubExpressions => + ResolvedStatements == null ? Rhss.SelectMany(r => r.NonSpecificationSubExpressions) : Enumerable.Empty(); + public override IEnumerable Children => ResolvedStatements ?? Lhss.Concat(Rhss); public override IEnumerable PreResolveChildren => Lhss.Concat(Rhss); @@ -63,6 +66,7 @@ public UpdateStmt(RangeToken rangeToken, List lhss, List PreResolveSubExpressions { get { foreach (var e in base.PreResolveSubExpressions) { diff --git a/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs index 06141701139..72bbed6ffc0 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs @@ -43,12 +43,6 @@ public override IEnumerable SpecificationSubExpressions { yield return e; } } - - if (this.Update != null) { - foreach (var e in this.Update.NonSpecificationSubExpressions) { - yield return e; - } - } } } diff --git a/Source/DafnyCore/AST/Substituter.cs b/Source/DafnyCore/AST/Substituter.cs index ea0a86f23c2..85836e9524f 100644 --- a/Source/DafnyCore/AST/Substituter.cs +++ b/Source/DafnyCore/AST/Substituter.cs @@ -595,8 +595,8 @@ protected virtual List CreateLocalVarSubstitutions(List(); 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; diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index 3c780e926e0..ac755b994f8 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/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"; diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs index 6721d1ce0ab..54c42f5bd74 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs +++ b/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})"; diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs index b12e70ee970..a8b82c29e9a 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs @@ -82,7 +82,7 @@ public override bool IsEssentiallyEmpty() { } public override IEnumerable 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; diff --git a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs index 2da42641516..d8e744bb993 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs +++ b/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; diff --git a/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs index 93b51ee07c5..5eca423d3ae 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs @@ -67,7 +67,7 @@ public IteratorDecl(RangeToken rangeToken, Name name, ModuleDefinition module, L DecreasesFields = new List(); YieldCountVariable = new LocalVariable(rangeToken, "_yieldCount", new EverIncreasingType(), true); - YieldCountVariable.type = YieldCountVariable.OptionalType; // resolve YieldCountVariable here + YieldCountVariable.type = YieldCountVariable.SyntacticType; // resolve YieldCountVariable here } /// diff --git a/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs index f17da2136b1..4ec1f512753 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs @@ -46,7 +46,7 @@ public override List ParentTypes(List typeArgs) { return result; } - public override SymbolKind Kind => Class.Kind; + public override SymbolKind? Kind => Class.Kind; public override string GetDescription(DafnyOptions options) { return Class.GetDescription(options); diff --git a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs index 54c4932a159..f9d0970a25b 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs @@ -59,7 +59,7 @@ public override List ParentTypes(List typeArgs) { } public bool ShouldVerify => true; // This could be made more accurate public ModuleDefinition ContainingModule => EnclosingModuleDefinition; - public override SymbolKind Kind => SymbolKind.Class; + public override SymbolKind? Kind => SymbolKind.Class; public override string GetDescription(DafnyOptions options) { return "subset type"; } diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs index 2a6ef2161c4..ddc7a89af77 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs @@ -267,7 +267,7 @@ public void RegisterMembers(ModuleResolver resolver, Dictionary ChildSymbols => Members.OfType(); - public virtual SymbolKind Kind => SymbolKind.Class; + public virtual SymbolKind? Kind => SymbolKind.Class; public virtual string GetDescription(DafnyOptions options) { return $"{WhatKind} {Name}"; } diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs index b3687324a13..0e41dc16a5d 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs @@ -12,7 +12,7 @@ public TypeSynonymDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParam } public TopLevelDecl AsTopLevelDecl => this; public TypeDeclSynonymInfo SynonymInfo { get; set; } - public override SymbolKind Kind => SymbolKind.Class; + public override SymbolKind? Kind => SymbolKind.Class; public override string GetDescription(DafnyOptions options) { return "type synonym"; } @@ -24,7 +24,7 @@ public InternalTypeSynonymDecl(RangeToken rangeToken, Name name, TypeParameter.T : base(rangeToken, name, characteristics, typeArgs, module, rhs, attributes) { } - public override SymbolKind Kind => SymbolKind.Class; + public override SymbolKind? Kind => SymbolKind.Class; public override string GetDescription(DafnyOptions options) { return "type synonym"; } diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs index 8ce7193f41b..8ef8df9d1b4 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs @@ -123,7 +123,7 @@ public string GetTriviaContainingDocstring() { return GetTriviaContainingDocstringFromStartTokenOrNull(); } - public abstract SymbolKind Kind { get; } + public abstract SymbolKind? Kind { get; } public abstract string GetDescription(DafnyOptions options); public string Designator => WhatKind; } \ No newline at end of file diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index d3e988f09ff..fc45713db39 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -371,7 +371,7 @@ ModuleImport | QualifiedModuleExport (. submodule = new AliasModuleDecl(theOptions, new RangeToken(startToken, t), new ModuleQualifiedId(namePath), - new Name(new RangeToken(startToken,startToken), namePath[^1].Value), parent, opened, idExports, Guid.NewGuid()); + new Name(RangeToken.NoToken, namePath[^1].Value), parent, opened, idExports, Guid.NewGuid()); .) ) . @@ -781,7 +781,7 @@ NewtypeDecl ] ( IF(IsIdentColonOrBar()) LocalVarName - [ ":" Type ] (. if (baseType == null) { baseType = new InferredTypeProxy(); } .) + [ ":" Type ] "|" Expression (. var witnessKind = SubsetTypeDecl.WKind.CompiledZero; .) @@ -796,9 +796,7 @@ NewtypeDecl ] [ TypeMembers ] (. td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, module, - new BoundVar(bvId, bvId.val, baseType){ - IsTypeExplicit = true - }, + new BoundVar(bvId, bvId.val, baseType), constraint, witnessKind, witness, parentTraits, members, attrs, isRefining: false); .) | Type @@ -841,7 +839,7 @@ SynonymTypeDecl ] (. if (ty == null) { ty = new InferredTypeProxy(); } .) + [ ":" Type ] "|" Expression (. var witnessKind = SubsetTypeDecl.WKind.CompiledZero; .) @@ -855,7 +853,7 @@ SynonymTypeDecl -= (. IToken id; Type ty; Type optType = null; += (. IToken id; Type ty = null; IToken startToken = null; .) WildIdent (. startToken = t; .) - [ ":" Type (. optType = ty; .) + [ ":" Type ] - (. var = new LocalVariable(new RangeToken(startToken, t), id.val, optType == null ? new InferredTypeProxy() : optType, isGhost) { - IsTypeExplicit = optType != null - }; + (. var = new LocalVariable(new RangeToken(startToken, t), id.val, ty, isGhost); .) . IdentTypeOptional = (. Contract.Ensures(Contract.ValueAtReturn(out var) != null); - Type ty; Type optType = null; + Type ty = null; .) WildIdentN - [ IF( la.kind == _colon) ":" Type (. optType = ty; .) + [ IF( la.kind == _colon) ":" Type // CoCo warns about this optional ':', because it is ambiguous with a ':' that follows the IdentTypeOptional. // An IdentTypeOptional can be the last thing in an Expression (a SetComprehension) // Also, a ':' can follow an Expression in a slices-by-length construct. So a ':' here might be the start @@ -960,8 +956,7 @@ IdentTypeOptional // disambiguate, it makes sense to force the colon to consider the ': type' here. Hence the semantic predicate. // Also a SetComprehension would be the wrong type in a slices-by-length construct. ] - (. var = new BoundVar(name.Tok, name.Value, optType == null ? new InferredTypeProxy() : optType) { - IsTypeExplicit = optType != null, + (. var = new BoundVar(name.Tok, name.Value, ty) { RangeToken = new RangeToken(name.StartToken, t) }; .) . @@ -1418,14 +1413,14 @@ Formals<.bool incoming, bool allowGhostKeyword, bool allowNewKeyword, bool allow GIdentType ParameterDefaultValue (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attributes, isOld, isNameOnly, isOlder) - { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range, IsTypeExplicit = ty != null } + { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range } ); .) { "," { Attribute } GIdentType ParameterDefaultValue (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attributes, isOld, isNameOnly, isOlder) - { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range, IsTypeExplicit = ty != null } + { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range } ); .) } ] @@ -1456,12 +1451,12 @@ FormalsOptionalIds<.List/*!*/ formals.> [ TypeIdentOptional (. formals.Add(new Formal(name.Tok, name.Value, ty, true, isGhost, defaultValue, attributes, false, isNameOnly) - { RangeToken = range, IsTypeExplicit = ty != null} + { RangeToken = range } ); .) { "," TypeIdentOptional (. formals.Add(new Formal(name.Tok, name.Value, ty, true, isGhost, defaultValue, attributes, false, isNameOnly) - { RangeToken = range, IsTypeExplicit = ty != null} + { RangeToken = range } ); .) } @@ -1751,7 +1746,7 @@ FunctionDecl GIdentType (. Contract.Assert(!resultIsGhost && !isOld && !isNameOnly && !isOlder); result = new Formal(resultName.Tok, resultName.Value, ty, false, false, null, null, false) - { RangeToken = range2, IsTypeExplicit = ty != null }; + { RangeToken = range2 }; .) ")" | Type @@ -2056,7 +2051,7 @@ PredicateResult SemErr(ErrorId.p_predicate_return_type_must_be_bool, new RangeToken(ty.StartToken, t), $"{name} return type should be bool, got {ty}"); } result = new Formal(nameId.Tok, nameId.Value, ty, false, false, null, attributes, false) - { RangeToken = range, IsTypeExplicit = ty != null }; + { RangeToken = range }; .) ")" | Type (. SemErr(ErrorId.p_no_return_type_for_predicate, new RangeToken(returnType.StartToken, t), $"{name}s do not have an explicitly declared return type; it is always bool. Unless you want to name the result: ': (result: bool)'"); .) diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 74b60de77cd..566fb5c6f7a 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -3664,9 +3664,9 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext // Resolve the types of the locals foreach (var local in s.Locals) { int prevErrorCount = reporter.Count(ErrorLevel.Error); - ResolveType(local.Tok, local.OptionalType, resolutionContext, ResolveTypeOptionEnum.InferTypeProxies, null); + ResolveType(local.Tok, local.SyntacticType, resolutionContext, ResolveTypeOptionEnum.InferTypeProxies, null); if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { - local.type = local.OptionalType; + local.type = local.SyntacticType; } else { local.type = new InferredTypeProxy(); } @@ -3701,9 +3701,9 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext VarDeclPattern s = (VarDeclPattern)stmt; foreach (var local in s.LocalVars) { int prevErrorCount = reporter.Count(ErrorLevel.Error); - ResolveType(local.Tok, local.OptionalType, resolutionContext, ResolveTypeOptionEnum.InferTypeProxies, null); + ResolveType(local.Tok, local.SyntacticType, resolutionContext, ResolveTypeOptionEnum.InferTypeProxies, null); if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { - local.type = local.OptionalType; + local.type = local.SyntacticType; } else { local.type = new InferredTypeProxy(); } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index 6b204f89f9b..f9dac43cbfa 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -249,8 +249,8 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext var s = (VarDeclPattern)stmt; foreach (var local in s.LocalVars) { int prevErrorCount = ErrorCount; - resolver.ResolveType(local.Tok, local.OptionalType, resolutionContext, ResolveTypeOptionEnum.InferTypeProxies, null); - local.type = ErrorCount == prevErrorCount ? local.type = local.OptionalType : new InferredTypeProxy(); + resolver.ResolveType(local.Tok, local.SyntacticType, resolutionContext, ResolveTypeOptionEnum.InferTypeProxies, null); + local.type = ErrorCount == prevErrorCount ? local.type = local.SyntacticType : new InferredTypeProxy(); local.PreType = Type2PreType(local.type); } ResolveExpression(s.RHS, resolutionContext); @@ -616,8 +616,8 @@ private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement update, List { private readonly CompilationData compilation; private readonly ErrorReporter reporter; - public PrecedenceLinterVisitor(CompilationData compilation, ErrorReporter reporter) { + public PrecedenceLinterVisitor(CompilationData compilation, ErrorReporter reporter) : base(false) { this.compilation = compilation; this.reporter = reporter; } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 31eff057f1f..d4fafaef967 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -657,7 +657,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re // to BVD what this variable stands for and display it as such to the user. Type et = p.Type.Subst(e.GetTypeArgumentSubstitutions()); LocalVariable local = new LocalVariable(p.RangeToken, "##" + p.Name, et, p.IsGhost); - local.type = local.OptionalType; // resolve local here + local.type = local.SyntacticType; // resolve local here IdentifierExpr ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)); ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here substMap.Add(p, ie); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index f377d7afd75..a0febafabaf 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -628,7 +628,7 @@ private void TrAssertStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, Lis if (v is LocalVariable) { var vcopy = new LocalVariable(stmt.RangeToken, string.Format("##{0}#{1}", name, v.Name), v.Type, v.IsGhost); - vcopy.type = vcopy.OptionalType; // resolve local here + vcopy.type = vcopy.SyntacticType; // resolve local here IdentifierExpr ie = new IdentifierExpr(vcopy.Tok, vcopy.AssignUniqueName(currentDeclaration.IdGenerator)); ie.Var = vcopy; @@ -1875,7 +1875,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E for (int i = 0; i < callee.Ins.Count; i++) { var formal = callee.Ins[i]; var local = new LocalVariable(formal.RangeToken, formal.Name + "#", formal.Type.Subst(tySubst), formal.IsGhost); - local.type = local.OptionalType; // resolve local here + local.type = local.SyntacticType; // resolve local here var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)); ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here substMap.Add(formal, ie); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index f5cd19f26e0..69e54f8a328 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -2550,6 +2550,7 @@ void CloneVariableAsBoundVar(IToken tok, IVariable iv, string prefix, out BoundV bv = new BoundVar(tok, CurrentIdGenerator.FreshId(prefix), iv.Type); // use this temporary variable counter, but for a Dafny name (the idea being that the number and the initial "_" in the name might avoid name conflicts) ie = new IdentifierExpr(tok, bv.Name); + bv.RangeToken = iv.RangeToken; ie.Var = bv; // resolve here ie.Type = bv.Type; // resolve here } @@ -3577,7 +3578,7 @@ Dictionary SetupBoundVarsAsLocals(List boundVar var substMap = new Dictionary(); foreach (BoundVar bv in boundVars) { LocalVariable local = new LocalVariable(bv.RangeToken, nameSuffix == null ? bv.Name : bv.Name + nameSuffix, bv.Type, bv.IsGhost); - local.type = local.OptionalType; // resolve local here + local.type = local.SyntacticType; // resolve local here IdentifierExpr ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)); ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here substMap.Add(bv, ie); @@ -3622,7 +3623,7 @@ Bpl.Expr SetupVariableAsLocal(IVariable v, Dictionary sub Contract.Requires(etran != null); var local = new LocalVariable(v.RangeToken, v.Name, v.Type, v.IsGhost); - local.type = local.OptionalType; // resolve local here + local.type = local.SyntacticType; // resolve local here var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)); ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here substMap.Add(v, ie); diff --git a/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs b/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs index 40587f4f9ed..dede5dcb5a4 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs @@ -12,6 +12,27 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup { public class DocumentSymbolTest : ClientBasedLanguageServerTest { + [Fact] + public async Task ExportImport() { + var source = @" +module Low { + const x := 3 +} + +module High { + import Low + + export + provides + Low +} +".TrimStart(); + + var documentItem = CreateAndOpenTestDocument(source); + var symbols = (await RequestDocumentSymbol(documentItem)).ToList(); + Assert.Equal(2, symbols.Count); + } + [Fact] public async Task NamelessClass() { var source = @"class { diff --git a/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs b/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs index 5c2b8874bf7..19c3c6a5d71 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs @@ -98,12 +98,12 @@ module [>Used<] { public async Task ModuleImport2() { var source = @" module User { - [>import<] Used + import Used const x := Us>Used<] { const x := 3 }".TrimStart(); await AssertPositionsLineUpWithRanges(source); @@ -302,7 +302,7 @@ method DoIt() { [Fact] public async Task JumpToOtherModule() { var source = @" -module Provider { +module {>2:Provider<} { class A { var [>x<]: int; @@ -326,7 +326,7 @@ method DoIt() returns (x: int) { } module Consumer2 { - [>import<] Provider + import Provider type A2 = Pro>C<]) => 3; + var c: [>C<] := Cons; +} +".TrimStart(); + + await AssertReferences(source, "ExportNamedImport.dfy"); + } + + [Fact] + public async Task ExportNamedImport() { + var source = @" +module Low { + const x := 3 +} + +module High { + import >MyLow<] +} +".TrimStart(); + + await AssertReferences(source, "ExportNamedImport.dfy"); + } + + [Fact] + public async Task ExportNamelessImport() { + var source = @" +module >Low<] + + export + provides + [>Low<] +} +".TrimStart(); + + await AssertReferences(source, "ExportImport.dfy"); + } + [Fact] public async Task AliasModuleDecl() { var source = @" diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs index 6abdd1a4f16..a0a0b33994d 100644 --- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs @@ -438,7 +438,7 @@ protected async Task AssertPositionsLineUpWithRanges(string source, string fileP var documentItem = await CreateOpenAndWaitForResolve(cleanSource, filePath); for (var index = 0; index < positions.Count; index++) { var position = positions[index]; - var range = ranges.ContainsKey(string.Empty) ? ranges[string.Empty][index] : ranges[index.ToString()].Single(); + var range = ranges.ContainsKey(index.ToString()) ? ranges[index.ToString()].Single() : ranges[string.Empty][index]; var result = (await RequestDefinition(documentItem, position)).Single(); Assert.Equal(range, result.Location!.Range); } diff --git a/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs index 52055ff8cd9..88f313222bb 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs @@ -55,7 +55,7 @@ private IEnumerable FromSymbol(ISymbol symbol) { } } - if (string.IsNullOrEmpty(symbol.NameToken.val)) { + if (!symbol.Kind.HasValue || string.IsNullOrEmpty(symbol.NameToken.val)) { return children; } @@ -66,7 +66,7 @@ private IEnumerable FromSymbol(ISymbol symbol) { Name = symbol.NameToken.val, Detail = documentation, Range = range, - Kind = (SymbolKind)symbol.Kind, + Kind = symbol.Kind.Value, SelectionRange = symbol.NameToken == Token.NoToken ? range : symbol.NameToken.ToRange().ToLspRange() } }; diff --git a/Source/DafnyLanguageServer/Handlers/DafnyWorkspaceSymbolHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyWorkspaceSymbolHandler.cs index 62004d65b0a..47868da604e 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyWorkspaceSymbolHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyWorkspaceSymbolHandler.cs @@ -37,6 +37,12 @@ protected override WorkspaceSymbolRegistrationOptions CreateRegistrationOptions( var state = await projectManager.GetStateAfterParsingAsync(); foreach (var def in state.SymbolTable.Definitions) { cancellationToken.ThrowIfCancellationRequested(); + + if (!def.Kind.HasValue) { + logger.LogWarning($"Definition without kind in symbol table: {def}"); + continue; + } + // CreateLocation called below uses the .Uri field of Tokens which // seems to occasionally be null while testing this from VSCode if (def.NameToken == null || def.NameToken.Uri == null) { @@ -57,7 +63,7 @@ protected override WorkspaceSymbolRegistrationOptions CreateRegistrationOptions( result.TryAdd(new SymbolInformation { Name = name, ContainerName = def.Kind.ToString(), - Kind = def.Kind, + Kind = def.Kind.Value, Location = DiagnosticUtil.CreateLocation(def.NameToken) }, matchDistance); } diff --git a/Source/DafnyLanguageServer/Workspace/SymbolTable.cs b/Source/DafnyLanguageServer/Workspace/SymbolTable.cs index 3121d196667..0872e2d046d 100644 --- a/Source/DafnyLanguageServer/Workspace/SymbolTable.cs +++ b/Source/DafnyLanguageServer/Workspace/SymbolTable.cs @@ -43,7 +43,7 @@ public static SymbolTable CreateFrom(ILogger logger, Program program, Cancellati // a suffix tree. var definitions = visited .OfType() - .Where(symbol => relevantDafnySymbolKinds.Contains(symbol.Kind)) + .Where(symbol => symbol.Kind.HasValue && relevantDafnySymbolKinds.Contains(symbol.Kind.Value)) .ToImmutableList(); return new SymbolTable(usages, definitions); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrecedenceLinter.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrecedenceLinter.dfy.expect index 386a142dc13..292a24df4dd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrecedenceLinter.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrecedenceLinter.dfy.expect @@ -18,6 +18,9 @@ PrecedenceLinter.dfy(313,28): Warning: unusual indentation in left-hand operand PrecedenceLinter.dfy(334,19): Warning: unusual indentation in right-hand operand of <==> (which ends at line 335, column 8); do you perhaps need parentheses? PrecedenceLinter.dfy(349,2): Warning: unusual indentation in else branch of if-then-else (which ends at line 353, column 5); do you perhaps need parentheses? PrecedenceLinter.dfy(365,2): Warning: unusual indentation in else branch of if-then-else (which ends at line 369, column 5); do you perhaps need parentheses? +PrecedenceLinter.dfy(401,43): Warning: unusual indentation in right-hand operand of ==> (which ends at line 402, column 11); do you perhaps need parentheses? +PrecedenceLinter.dfy(403,43): Warning: unusual indentation in right-hand operand of ==> (which ends at line 404, column 11); do you perhaps need parentheses? +PrecedenceLinter.dfy(431,11): Warning: unusual indentation in else branch of if-then-else (which ends at line 434, column 6); do you perhaps need parentheses? PrecedenceLinter.dfy(463,11): Warning: unusual indentation in else branch of if-then-else (which ends at line 464, column 20); do you perhaps need parentheses? PrecedenceLinter.dfy(478,17): Warning: unusual indentation in else branch of if-then-else (which ends at line 479, column 9); do you perhaps need parentheses? PrecedenceLinter.dfy(480,17): Warning: unusual indentation in else branch of if-then-else (which ends at line 481, column 13); do you perhaps need parentheses? diff --git a/docs/dev/news/5419.fix b/docs/dev/news/5419.fix new file mode 100644 index 00000000000..352950c6b5c --- /dev/null +++ b/docs/dev/news/5419.fix @@ -0,0 +1,2 @@ +- Fix a code navigation bug that could occur when navigating to and from module imports +- Fix a code navigation bug that could occur when navigating to and from explicit types of variables \ No newline at end of file