Separate UI code and business logic for the resolve and verify commands

.github/workflows/integration-tests-reusable.yml

@@ -53,6 +53,7 @@ jobs:
       shard-list: ${{ steps.populate-shard-list.outputs.shard-list }}
   test:
     needs: populate-matrix-dimensions
+    timeout-minutes: 120
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:

Source/DafnyCore/AST/Cloner.cs

@@ -232,9 +232,8 @@ public virtual Type CloneType(Type t) {
       } else if (t is MultiSetType) {
         var tt = (MultiSetType)t;
         return new MultiSetType(tt.HasTypeArg() ? CloneType(tt.Arg) : null);
-      } else if (t is MapType) {
-        var tt = (MapType)t;
-        return new MapType(tt.Finite, CloneType(tt.Domain), CloneType(tt.Range));
+      } else if (t is MapType mapType) {
+        return new MapType(this, mapType);
       } else if (t is ArrowType) {
         var tt = (ArrowType)t;
         return new ArrowType(Tok(tt.tok), tt.Args.ConvertAll(CloneType), CloneType(tt.Result));

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

@@ -1,5 +1,6 @@
 using System;
 using System.Diagnostics.Contracts;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -86,7 +87,7 @@ public string AssignUniqueName(FreshIdGenerator generator) {
   }
 
   public abstract IToken NameToken { get; }
-  public DafnySymbolKind 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

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -134,7 +135,7 @@ public NonglobalVariable(IToken tok, string name, Type type, bool 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 DafnySymbolKind Kind => DafnySymbolKind.Variable;
+  public SymbolKind Kind => SymbolKind.Variable;
   public string GetDescription(DafnyOptions options) {
     return this.AsText();
   }

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -191,7 +191,9 @@ public static string ToStringWithoutNewline(System.IO.StringWriter wr) {
     }
 
     public void PrintProgramLargeStack(Program prog, bool afterResolver) {
+#pragma warning disable VSTHRD002
       DafnyMain.LargeStackFactory.StartNew(() => PrintProgram(prog, afterResolver)).Wait();
+#pragma warning restore VSTHRD002
     }
 
     public void PrintProgram(Program prog, bool afterResolver) {

Source/DafnyCore/AST/IHasUsages.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -53,7 +54,7 @@ public static string AsText(this IVariable variable) {
 }
 
 public interface ISymbol : IDeclarationOrUsage {
-  DafnySymbolKind Kind { get; }
+  SymbolKind Kind { get; }
 
   string GetDescription(DafnyOptions options);
 }
@@ -79,38 +80,4 @@ public static ISet<ISymbol> GetSymbolDescendants(ISymbol node) {
     }
     return result;
   }
-}
-
-/// <summary>
-/// This is a copy of OmniSharp.Extensions.LanguageServer.Protocol.Models.SymbolKind
-/// In the future, we'll include that package in this project, and then this copy can be removed.
-/// For now, adding that package reference is not worth its weight.
-/// </summary>
-public enum DafnySymbolKind {
-  File = 1,
-  Module = 2,
-  Namespace = 3,
-  Package = 4,
-  Class = 5,
-  Method = 6,
-  Property = 7,
-  Field = 8,
-  Constructor = 9,
-  Enum = 10,
-  Interface = 11,
-  Function = 12,
-  Variable = 13,
-  Constant = 14,
-  String = 15,
-  Number = 16,
-  Boolean = 17,
-  Array = 18,
-  Object = 19,
-  Key = 20,
-  Null = 21,
-  EnumMember = 22,
-  Struct = 23,
-  Event = 24,
-  Operator = 25,
-  TypeParameter = 26,
 }

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -46,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 DafnySymbolKind Kind => DafnySymbolKind.Constant;
+  public override SymbolKind Kind => SymbolKind.Constant;
 
   public override IEnumerable<INode> PreResolveChildren => Children;
   public ModuleDefinition ContainingModule => EnclosingModule;

Source/DafnyCore/AST/Members/Constructor.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -10,7 +11,7 @@ void ObjectInvariant() {
     Contract.Invariant(Body == null || Body is DividedBlockStmt);
   }
 
-  public override DafnySymbolKind Kind => DafnySymbolKind.Constructor;
+  public override SymbolKind Kind => SymbolKind.Constructor;
   protected override string GetQualifiedName() {
     return EnclosingClass.Name;
   }

Source/DafnyCore/AST/Members/Field.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -95,7 +96,7 @@ public string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public virtual DafnySymbolKind Kind => DafnySymbolKind.Field;
+  public virtual SymbolKind Kind => SymbolKind.Field;
 
   public string GetDescription(DafnyOptions options) {
     var prefix = IsMutable ? "var" : "const";

Source/DafnyCore/AST/Members/Function.cs

@@ -5,6 +5,7 @@
 using System.Numerics;
 using DafnyCore;
 using Microsoft.Dafny.Auditor;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -485,7 +486,7 @@ public string GetTriviaContainingDocstring() {
     return null;
   }
 
-  public DafnySymbolKind Kind => DafnySymbolKind.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) {

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -93,7 +94,7 @@ public bool InferredDecreases {
   public IEnumerable<IToken> OwnedTokens => CwInner.OwnedTokens;
   public RangeToken RangeToken => CwInner.RangeToken;
   public IToken NameToken => CwInner.NameToken;
-  public DafnySymbolKind Kind => CwInner.Kind;
+  public SymbolKind Kind => CwInner.Kind;
   public string GetDescription(DafnyOptions options) {
     return CwInner.GetDescription(options);
   }
@@ -127,7 +128,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 DafnySymbolKind 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

@@ -3,6 +3,7 @@
 using System.Linq;
 using System.Numerics;
 using Microsoft.Dafny.Auditor;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -388,7 +389,7 @@ public string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public virtual DafnySymbolKind Kind => DafnySymbolKind.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/ModuleDecl.cs

@@ -2,6 +2,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -80,7 +81,7 @@ public virtual string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public DafnySymbolKind Kind => DafnySymbolKind.Namespace;
+  public SymbolKind Kind => SymbolKind.Namespace;
   public string GetDescription(DafnyOptions options) {
     return $"module {Name}";
   }

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -4,6 +4,7 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using Microsoft.Dafny.Auditor;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -1046,7 +1047,7 @@ bool InheritsFromObject(TraitDecl traitDecl) {
     return Enumerable.Empty<ISymbol>();
   });
 
-  public DafnySymbolKind Kind => DafnySymbolKind.Namespace;
+  public SymbolKind Kind => SymbolKind.Namespace;
   public string GetDescription(DafnyOptions options) {
     return $"module {Name}";
   }

Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs

@@ -95,6 +95,9 @@ public ModuleDecl ResolveTarget(ErrorReporter reporter) {
   }
 
   private ModuleDecl ResolveTargetUncached(ErrorReporter reporter) {
+    if (Root == null) {
+      return null;
+    }
     var decl = Root;
     for (int k = 1; k < Path.Count; k++) {
       ModuleSignature p;

Source/DafnyCore/AST/Program.cs

@@ -15,6 +15,7 @@ void ObjectInvariant() {
     Contract.Invariant(DefaultModule != null);
   }
 
+  public bool HasParseErrors { get; set; }
   public readonly string FullName;
 
   // Resolution essentially flattens the module hierarchy, for
@@ -52,6 +53,7 @@ public Program(Cloner cloner, Program original) {
     SystemModuleManager = original.SystemModuleManager;
     Reporter = original.Reporter;
     Compilation = original.Compilation;
+    HasParseErrors = original.HasParseErrors;
 
     if (cloner.CloneResolvedFields) {
       throw new NotImplementedException();

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

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -130,7 +131,7 @@ public void MakeGhost() {
     (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>()).Concat(
       IsTypeExplicit ? new List<Node>() { OptionalType ?? type } : Enumerable.Empty<Node>());
 
-  public DafnySymbolKind Kind => DafnySymbolKind.Variable;
+  public SymbolKind Kind => SymbolKind.Variable;
   public string GetDescription(DafnyOptions options) {
     return this.AsText();
   }

Source/DafnyCore/AST/Tokens.cs

@@ -56,8 +56,8 @@ string Boogie.IToken.filename {
 public class Token : IToken {
 
   public Token peekedTokens; // Used only internally by Coco when the scanner "peeks" tokens. Normally null at the end of parsing
-  public static readonly Token NoToken = new Token();
-  public static readonly Token Cli = new Token();
+  public static readonly Token NoToken = new();
+  public static readonly Token Cli = new();
   public Token() : this(0, 0) { }
 
   public Token(int linenum, int colnum) {
@@ -218,6 +218,10 @@ public static RangeToken ToRange(this IToken token) {
     if (token is BoogieRangeToken boogieRangeToken) {
       return new RangeToken(boogieRangeToken.StartToken, boogieRangeToken.EndToken);
     }
+
+    if (token is NestedToken nestedToken) {
+      return ToRange(nestedToken.Outer);
+    }
     return token as RangeToken ?? new RangeToken(token, token);
   }
 }

Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -49,7 +50,7 @@ public string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public DafnySymbolKind Kind => DafnySymbolKind.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

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -81,7 +82,7 @@ public override bool IsEssentiallyEmpty() {
   }
 
   public override IEnumerable<ISymbol> ChildSymbols => base.ChildSymbols.Concat(Ctors);
-  public override DafnySymbolKind Kind => DafnySymbolKind.Enum;
+  public override SymbolKind Kind => SymbolKind.Enum;
 
   public bool SetIndent(int indent, TokenNewIndentCollector formatter) {
     var indent2 = indent + formatter.SpaceTab;

Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -45,7 +46,7 @@ public override List<Type> ParentTypes(List<Type> typeArgs) {
     return result;
   }
 
-  public override DafnySymbolKind Kind => Class.Kind;
+  public override SymbolKind Kind => Class.Kind;
 
   public override string GetDescription(DafnyOptions options) {
     return Class.GetDescription(options);

Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -48,7 +49,7 @@ public override List<Type> ParentTypes(List<Type> typeArgs) {
   }
   public bool ShouldVerify => true; // This could be made more accurate
   public ModuleDefinition ContainingModule => EnclosingModuleDefinition;
-  public override DafnySymbolKind Kind => DafnySymbolKind.Class;
+  public override SymbolKind Kind => SymbolKind.Class;
   public override string GetDescription(DafnyOptions options) {
     return "subset type";
   }