Feat: Dafny format file.dfy and IDE extension

.gitignore

@@ -65,4 +65,4 @@ Source/.vs
 
 node_modules/
 package.json
-package-lock.json
+package-lock.json

CONTRIBUTING.md

@@ -62,3 +62,18 @@ Once it succeeds, one has to go back to (view 1) and re-run the failed jobs, so
 
 After doing these steps once, for other PRs, one only needs to re-run deep checks in (view 1)
 
+### How can I write portions of Dafny in Dafny itself?
+
+Since https://github.com/dafny-lang/dafny/pull/2399, it is possible to add \*.dfy files next to other source files.
+The plugin `dafny-msbuild` takes all the dafny files and compiles them into a single file `Source/DafnyCore/obj/Debug/net6.0/GeneratedFromDafny.cs`
+that is automatically included in the build process. This file contains also the Dafny run-time in C#.
+One example of such file is `Source/DafnyCore/AST/Formatting.dfy`, and you can use it as a starting point.
+
+Since Dafny cannot read C# files directly, you have to declare the C# functions it is calling using the `{:extern}` attribute to
+interoperate with Dafny.
+For example, `Formatting.dfy`
+
+- Defines `System.CsString` as an alias for c# strings and concatenation, so that we can interoperate with existing strings rather than using sequences of characters
+- Defines `CsStringEmpty` as an alias for `System.String.Empty`
+- Defines `Microsoft.Dafny.HelperString.FinishesByNewline` by also using externs. That helper is defined in `IndentationFormatter.cs`
+- Defines a trait `IIndentationFormatter` that Dafny can extend and provide to `ReindentProgramFromFirstToken`

RELEASE_NOTES.md

@@ -256,12 +256,13 @@ See [docs/dev/news/](docs/dev/news/).
 
 # 3.7.2
 
-- fix: Hovering over variables and methods inside cases of nested match statements work again. (https://github.com/dafny-lang/dafny/pull/2334)
+- fix: Hovering over variables and methods inside cases of nested match statements works again. (https://github.com/dafny-lang/dafny/pull/2334)
 - fix: Fix bug in translation of two-state predicates with heap labels. (https://github.com/dafny-lang/dafny/pull/2300)
 - fix: Check that arguments of 'unchanged' satisfy enclosing reads clause. (https://github.com/dafny-lang/dafny/pull/2302)
+- feat: Whitespaces and comments are kept in relevant parts of the AST (https://github.com/dafny-lang/dafny/pull/1801)
 - fix: Underconstrained closures don't crash Dafny anymore. (https://github.com/dafny-lang/dafny/pull/2382)
 - fix: Caching in the language server does not prevent gutter icons from being updated correctly. (https://github.com/dafny-lang/dafny/pull/2312)
-- fix: Last edited verified first & corrected display of verification status. (https://github.com/dafny-lang/dafny/pull/2352)
+- fix: Last edited file verified first & corrected display of verification status. (https://github.com/dafny-lang/dafny/pull/2352)
 - fix: Correctly infer type of numeric arguments, where the type is a subset type of a newtype. (https://github.com/dafny-lang/dafny/pull/2314)
 - fix: Fix concurrency bug that sometimes led to an exception during the production of verification logs. (https://github.com/dafny-lang/dafny/pull/2398)
 

Source/DafnyCore/AST/DafnyAst.cs

@@ -90,13 +90,29 @@ public string Name {
       }
     }
 
+    /// Get the first token that is in the same file as the DefaultModule.RootToken.FileName
+    /// (skips included tokens)
     public IToken GetFirstTopLevelToken() {
-      return DefaultModuleDef.GetFirstTopLevelToken();
+      if (DefaultModule.RootToken.Next == null) {
+        return null;
+      }
+
+      var firstToken = DefaultModule.RootToken.Next;
+      // We skip all included files
+      while (firstToken is { Next: { } } && firstToken.Next.Filename != DefaultModule.RootToken.Filename) {
+        firstToken = firstToken.Next;
+      }
+
+      if (firstToken == null || firstToken.kind == 0) {
+        return null;
+      }
+
+      return firstToken;
     }
 
     public override IEnumerable<Node> Children => new[] { DefaultModule };
 
-    public IEnumerable<Node> ConcreteChildren => Children;
+    public override IEnumerable<Node> PreResolveChildren => Children;
   }
 
   public class Include : TokenNode, IComparable {
@@ -125,6 +141,7 @@ public int CompareTo(object obj) {
     }
 
     public override IEnumerable<Node> Children => Enumerable.Empty<Node>();
+    public override IEnumerable<Node> PreResolveChildren => Enumerable.Empty<Node>();
   }
 
   /// <summary>
@@ -316,6 +333,8 @@ public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object
       Prev == null
         ? Enumerable.Empty<Node>()
         : new List<Node> { Prev });
+
+    public override IEnumerable<Node> PreResolveChildren => Children;
   }
 
   public static class AttributesExtensions {
@@ -575,7 +594,8 @@ public NonglobalVariable(IToken tok, string name, Type type, bool isGhost) {
     }
 
     public IToken NameToken => tok;
-    public override IEnumerable<Node> Children => IsTypeExplicit ? Type.Nodes : Enumerable.Empty<Node>();
+    public override IEnumerable<Node> Children => IsTypeExplicit ? new List<Node>() { Type } : Enumerable.Empty<Node>();
+    public override IEnumerable<Node> PreResolveChildren => IsTypeExplicit ? new List<Node>() { Type } : Enumerable.Empty<Node>();
   }
 
   public class Formal : NonglobalVariable {
@@ -722,7 +742,8 @@ public class ActualBinding : TokenNode {
     public readonly bool IsGhost;
 
     public override IEnumerable<Node> Children => new List<Node> { Actual }.Where(x => x != null);
-    // Names are owned by the method call
+
+    public override IEnumerable<Node> PreResolveChildren => Children;
 
     public ActualBinding(IToken /*?*/ formalParameterName, Expression actual, bool isGhost = false) {
       Contract.Requires(actual != null);
@@ -768,6 +789,7 @@ public void AcceptArgumentExpressionsAsExactParameterList(List<Expression> args
     }
 
     public override IEnumerable<Node> Children => arguments == null ? ArgumentBindings : arguments;
+    public override IEnumerable<Node> PreResolveChildren => Children;
   }
 
   class QuantifiedVariableDomainCloner : Cloner {
@@ -808,6 +830,7 @@ public bool HasAttributes() {
     }
 
     public override IEnumerable<Node> Children => Expressions;
+    public override IEnumerable<Node> PreResolveChildren => Children;
   }
 
   public class BottomUpVisitor {
@@ -874,6 +897,7 @@ public void Visit(Function function) {
       Visit(function.Ens);
       Visit(function.Decreases.Expressions);
       if (function.Body != null) { Visit(function.Body); }
+      if (function.ByMethodBody != null) { Visit(function.ByMethodBody); }
       //TODO More?
     }
     public void Visit(Expression expr) {
@@ -904,11 +928,17 @@ protected virtual void VisitOneStmt(Statement stmt) {
     }
   }
   public class TopDownVisitor<State> {
+    protected bool preResolve = false;
+
     public void Visit(Expression expr, State st) {
       Contract.Requires(expr != null);
       if (VisitOneExpr(expr, ref st)) {
-        // recursively visit all subexpressions and all substatements
-        expr.SubExpressions.Iter(e => Visit(e, st));
+        if (preResolve && expr is ConcreteSyntaxExpression concreteSyntaxExpression) {
+          concreteSyntaxExpression.PreResolveSubExpressions.Iter(e => Visit(e, st));
+        } else {
+          // recursively visit all subexpressions and all substatements
+          expr.SubExpressions.Iter(e => Visit(e, st));
+        }
         if (expr is StmtExpr) {
           // a StmtExpr also has a substatement
           var e = (StmtExpr)expr;
@@ -920,8 +950,13 @@ public void Visit(Statement stmt, State st) {
       Contract.Requires(stmt != null);
       if (VisitOneStmt(stmt, ref st)) {
         // recursively visit all subexpressions and all substatements
-        stmt.SubExpressions.Iter(e => Visit(e, st));
-        stmt.SubStatements.Iter(s => Visit(s, st));
+        if (preResolve) {
+          stmt.PreResolveSubExpressions.Iter(e => Visit(e, st));
+          stmt.PreResolveSubStatements.Iter(s => Visit(s, st));
+        } else {
+          stmt.SubExpressions.Iter(e => Visit(e, st));
+          stmt.SubStatements.Iter(s => Visit(s, st));
+        }
       }
     }
     public void Visit(IEnumerable<Expression> exprs, State st) {

Source/DafnyCore/AST/Expressions/ComprehensionExpr.cs

@@ -23,7 +23,7 @@ namespace Microsoft.Dafny;
 /// LambdaExpr also inherits from this base class but isn't really a comprehension,
 /// and should be considered implementation inheritance.
 /// </summary>
-public abstract class ComprehensionExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBearingExpression {
+public abstract class ComprehensionExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBearingExpression, ICanFormat {
   public virtual string WhatKind => "comprehension";
   public readonly List<BoundVar> BoundVars;
   public readonly Expression Range;
@@ -444,6 +444,7 @@ protected ComprehensionExpr(Cloner cloner, ComprehensionExpr original) : base(cl
     }
   }
   public override IEnumerable<Node> Children => (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>()).Concat(SubExpressions);
+  public override IEnumerable<Node> PreResolveChildren => Children;
 
   public override IEnumerable<Expression> SubExpressions {
     get {
@@ -456,4 +457,42 @@ public override IEnumerable<Expression> SubExpressions {
   }
 
   public override IEnumerable<Type> ComponentTypes => BoundVars.Select(bv => bv.Type);
+  public virtual bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
+    var alreadyAligned = false;
+    var assignOpIndent = indentBefore;
+
+    foreach (var token in OwnedTokens) {
+      switch (token.val) {
+        case "forall":
+        case "exists":
+        case "map":
+        case "set":
+        case "imap":
+        case "iset": {
+            indentBefore = formatter.ReduceBlockiness ? indentBefore : formatter.GetNewTokenVisualIndent(token, indentBefore);
+            assignOpIndent = formatter.ReduceBlockiness ? indentBefore + formatter.SpaceTab : indentBefore;
+            formatter.SetOpeningIndentedRegion(token, indentBefore);
+            break;
+          }
+        case ":=":
+        case "::": {
+            var afterAssignIndent = (formatter.ReduceBlockiness && token.Prev.line == token.line) || token.line == token.Next.line ? assignOpIndent : assignOpIndent + formatter.SpaceTab;
+            if (alreadyAligned) {
+              formatter.SetIndentations(token, afterAssignIndent, assignOpIndent, afterAssignIndent);
+            } else {
+              if (TokenNewIndentCollector.IsFollowedByNewline(token)) {
+                formatter.SetIndentations(token, afterAssignIndent, assignOpIndent, afterAssignIndent);
+              } else {
+                alreadyAligned = true;
+                formatter.SetAlign(assignOpIndent, token, out afterAssignIndent, out assignOpIndent);
+                assignOpIndent -= 1; // because "::" or ":=" has one more char than a comma 
+              }
+            }
+            break;
+          }
+      }
+    }
+
+    return true;
+  }
 }

Source/DafnyCore/AST/Expressions/DisjunctivePattern.cs

@@ -12,6 +12,7 @@ public DisjunctivePattern(IToken tok, List<ExtendedPattern> alternatives, bool i
   }
 
   public override IEnumerable<Node> Children => Alternatives;
+  public override IEnumerable<Node> PreResolveChildren => Children;
   public override void Resolve(Resolver resolver, ResolutionContext resolutionContext,
     Type sourceType, bool isGhost, bool mutable,
     bool inPattern, bool inDisjunctivePattern) {