Feat: Added ranges to expression

RELEASE_NOTES.md

@@ -10,6 +10,7 @@
 - fix: Allow datatype update expressions for constructors with nameonly parameters (https://github.com/dafny-lang/dafny/pull/1949)
 - fix: Fix malformed Java code generated for comprehensions that use maps (https://github.com/dafny-lang/dafny/pull/1939)
 - feat: Recognize `!in` operator when looking for compilable comprehensions (https://github.com/dafny-lang/dafny/pull/1939)
+- feat: The dafny language server now returns expressions ranges instead of token ranges to better report errors (https://github.com/dafny-lang/dafny/pull/1985)
 
 # 3.5.0
 

Source/Dafny/AST/DafnyAst.cs

@@ -6927,6 +6927,16 @@ public virtual IEnumerable<Expression> NonSpecificationSubExpressions {
  }
  }
  }
+
+ [FilledInDuringResolution] private IToken rangeToken;
+ public virtual IToken RangeToken {
+ get {
+ if (rangeToken == null) {
+ rangeToken = new RangeToken(Tok, EndTok);
+ }
+ return rangeToken;
+ }
+ }
  }
 
  public class LList<T> {
@@ -8884,6 +8894,25 @@ public virtual string val {
  }
  }
 
+ public class RangeToken : TokenWrapper {
+ // The wrapped token is the startTok
+ private IToken endTok;
+
+ public IToken StartToken => WrappedToken;
+ public IToken EndToken => endTok;
+
+ // Used for range reporting
+ override public string val {
+ get {
+ return new string(' ', endTok.pos + endTok.val.Length - pos);
+ }
+ }
+
+ public RangeToken(IToken startTok, IToken endTok) : base(startTok) {
+ this.endTok = endTok;
+ }
+ }
+
  public class NestedToken : TokenWrapper {
  public NestedToken(IToken outer, IToken inner, string message = null)
  : base(outer) {
@@ -8997,6 +9026,38 @@ public virtual IEnumerable<Expression> SubExpressions {
  get { yield break; }
  }
 
+ private RangeToken rangeToken;
+
+ /// Creates a token on the entire range of the expression.
+ /// Used only for error reporting.
+ public RangeToken RangeToken {
+ get {
+ if (rangeToken == null) {
+ var startTok = tok;
+ var endTok = tok;
+ foreach (var e in SubExpressions) {
+ if (e.tok.filename != tok.filename || e.IsImplicit) {
+ // Ignore auto-generated expressions, if any.
+ continue;
+ }
+
+ if (e.StartToken.pos < startTok.pos) {
+ startTok = e.StartToken;
+ } else if (e.EndToken.pos > endTok.pos) {
+ endTok = e.EndToken;
+ }
+ }
+
+ rangeToken = new RangeToken(startTok, endTok);
+ }
+
+ return rangeToken;
+ }
+ }
+
+ public IToken StartToken => RangeToken.StartToken;
+ public IToken EndToken => RangeToken.EndToken;
+
  /// <summary>
  /// Returns the list of types that appear in this expression proper (that is, not including types that
  /// may appear in subexpressions). Types occurring in sub-statements of the expression are not included.

Source/Dafny/Verifier/Translator.TrStatement.cs

@@ -547,7 +547,7 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder,
  bool splitHappened;
  var ss = TrSplitExpr(stmt.Expr, etran, true, out splitHappened);
  if (!splitHappened) {
- var tok = enclosingToken == null ? stmt.Expr.tok : new NestedToken(enclosingToken, stmt.Expr.tok);
+ var tok = enclosingToken == null ? GetToken(stmt.Expr) : new NestedToken(enclosingToken, GetToken(stmt.Expr));
  var desc = new PODesc.AssertStatement(errorMessage);
  (proofBuilder ?? b).Add(Assert(tok, etran.TrExpr(stmt.Expr), desc, stmt.Tok,
  etran.TrAttributes(stmt.Attributes, null)));
@@ -1640,7 +1640,7 @@ void TrCallStmt(CallStmt s, BoogieStmtListBuilder builder, List<Variable> locals
  builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, initHeap, etran.HeapExpr));
  }
  builder.Add(new CommentCmd("TrCallStmt: Before ProcessCallStmt"));
- ProcessCallStmt(s.Tok, tySubst, GetTypeParams(s.Method), s.Receiver, actualReceiver, s.Method, s.MethodSelect.AtLabel, s.Args, bLhss, lhsTypes, builder, locals, etran);
+ ProcessCallStmt(GetToken(s), tySubst, GetTypeParams(s.Method), s.Receiver, actualReceiver, s.Method, s.MethodSelect.AtLabel, s.Args, bLhss, lhsTypes, builder, locals, etran);
  builder.Add(new CommentCmd("TrCallStmt: After ProcessCallStmt"));
  for (int i = 0; i < lhsBuilders.Count; i++) {
  var lhs = s.Lhs[i];