Merge remote-tracking branch 'origin/master' into improveErrorLocations

Source/DafnyBenchmarkingPlugin/JavaBenchmarkCompilationInstrumenter.cs

@@ -21,7 +21,7 @@ public override void BeforeMethod(Method m, ConcreteSyntaxTree wr) {
     if (Attributes.Contains(m.EnclosingClass.Attributes, "benchmarks")) {
       if (m is Constructor) {
         if (m.Ins.Any()) {
-          Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, m.Tok,
+          Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, m.Origin,
             $"Classes with {{:benchmarks}} can not accept parameters in their constructors");
         }
 
@@ -34,7 +34,7 @@ public override void BeforeMethod(Method m, ConcreteSyntaxTree wr) {
         wr.WriteLine("@org.openjdk.jmh.annotations.Setup(org.openjdk.jmh.annotations.Level.Iteration)");
       } else if (Attributes.Contains(m.Attributes, "benchmarkTearDown")) {
         if (m.Ins.Any()) {
-          Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, m.Tok,
+          Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, m.Origin,
             $"Methods with {{:benchmarkTearDown}} can not accept parameters");
         }
         wr.WriteLine("@org.openjdk.jmh.annotations.TearDown(org.openjdk.jmh.annotations.Level.Iteration)");

Source/DafnyCore.Test/ClonerTest.cs

@@ -11,7 +11,7 @@ class DummyDecl : Declaration {
     public DummyDecl(Cloner cloner, Declaration original) : base(cloner, original) {
     }
 
-    public DummyDecl(IOrigin rangeOrigin, Name name, Attributes attributes, bool isRefining) : base(rangeOrigin, name,
+    public DummyDecl(IOrigin origin, Name name, Attributes attributes, bool isRefining) : base(origin, name,
       attributes, isRefining) {
     }
 

Source/DafnyCore.Test/NodeTests.cs

@@ -6,12 +6,12 @@ namespace DafnyCore.Test;
 public class NodeTests {
 
   class ConcreteNode : Node {
-    public ConcreteNode(IOrigin rangeOrigin, IEnumerable<INode>? children = null) {
-      Origin = rangeOrigin;
+    public ConcreteNode(IOrigin origin, IEnumerable<INode>? children = null) {
+      Origin = origin;
       Children = children ?? Enumerable.Empty<INode>();
     }
 
-    public override IOrigin Origin { get; set; }
+    public override IOrigin Origin { get; }
     public override IEnumerable<INode> Children { get; }
     public override IEnumerable<INode> PreResolveChildren => Children;
   }

Source/DafnyCore/AST/Attributes.cs

@@ -45,7 +45,7 @@ public BuiltInAtAttributeSyntax Filter(Func<IAttributeBearingDeclaration, bool>
   }
 }
 
-public class Attributes : TokenNode, ICanFormat {
+public class Attributes : NodeWithComputedRange, ICanFormat {
   [ContractInvariantMethod]
   void ObjectInvariant() {
     Contract.Invariant(Name != null);
@@ -64,7 +64,7 @@ void ObjectInvariant() {
   public readonly List<Expression> Args;
 
   public readonly Attributes Prev;
-  public Attributes(string name, [Captured] List<Expression> args, Attributes prev) {
+  public Attributes(string name, [Captured] List<Expression> args, Attributes prev) : base(Token.NoToken) {
     Contract.Requires(name != null);
     Contract.Requires(cce.NonNullElements(args));
     Contract.Requires(name != UserSuppliedAtAttribute.AtName || this is UserSuppliedAtAttribute);
@@ -612,7 +612,7 @@ private static void ResolveLikeDatatypeConstructor(Program program, Formal[] for
     UserSuppliedAtAttribute attrs, ActualBindings bindings, ModuleResolver resolver) {
     var resolutionContext = new ResolutionContext(new NoContext(program.DefaultModuleDef), false); ;
     var typeMap = new Dictionary<TypeParameter, Type>();
-    resolver.ResolveActualParameters(bindings, formals.ToList(), attrs.Tok,
+    resolver.ResolveActualParameters(bindings, formals.ToList(), attrs.Origin,
       attrs, resolutionContext, typeMap, null);
     resolver.FillInDefaultValueExpressions();
     resolver.SolveAllTypeConstraints();
@@ -689,13 +689,13 @@ public class UserSuppliedAttributes : Attributes {
   public readonly IOrigin OpenBrace;
   public readonly IOrigin CloseBrace;
   public bool Recognized;  // set to true to indicate an attribute that is processed by some part of Dafny; this allows it to be colored in the IDE
-  public UserSuppliedAttributes(IOrigin tok, IOrigin openBrace, IOrigin closeBrace, List<Expression> args, Attributes prev)
-    : base(tok.val, args, prev) {
-    Contract.Requires(tok != null);
+  public UserSuppliedAttributes(IOrigin origin, IOrigin openBrace, IOrigin closeBrace, List<Expression> args, Attributes prev)
+    : base(origin.val, args, prev) {
+    Contract.Requires(origin != null);
     Contract.Requires(openBrace != null);
     Contract.Requires(closeBrace != null);
     Contract.Requires(args != null);
-    this.tok = tok;
+    SetOrigin(origin);
     OpenBrace = openBrace;
     CloseBrace = closeBrace;
   }
@@ -707,11 +707,11 @@ public class UserSuppliedAtAttribute : Attributes {
   public readonly IOrigin AtSign;
   public bool Builtin;  // set to true to indicate it was recognized as a builtin attribute
   // Otherwise it's a user-defined one and Arg needs to be fully resolved
-  public UserSuppliedAtAttribute(IOrigin tok, Expression arg, Attributes prev)
+  public UserSuppliedAtAttribute(IOrigin origin, Expression arg, Attributes prev)
     : base(AtName, new List<Expression>() { arg }, prev) {
-    Contract.Requires(tok != null);
-    this.tok = tok;
-    this.AtSign = tok;
+    Contract.Requires(origin != null);
+    SetOrigin(origin);
+    this.AtSign = origin;
   }
 
   public Expression Arg => Args[0];

Source/DafnyCore/AST/Cloner.cs

@@ -237,7 +237,7 @@ public virtual Type CloneType(Type t) {
         return new MapType(this, mapType);
       } else if (t is ArrowType) {
         var tt = (ArrowType)t;
-        return new ArrowType(Origin(tt.Tok), tt.Args.ConvertAll(CloneType), CloneType(tt.Result));
+        return new ArrowType(Origin(tt.Origin), tt.Args.ConvertAll(CloneType), CloneType(tt.Result));
       } else if (t is UserDefinedType) {
         var tt = (UserDefinedType)t;
 #if TEST_TYPE_SYNONYM_TRANSPARENCY
@@ -269,7 +269,7 @@ public virtual Type CloneType(Type t) {
     public virtual Formal CloneFormal(Formal formal, bool isReference) {
       return (Formal)clones.GetOrCreate(formal, () => isReference
        ? formal
-       : new Formal(Origin(formal.Tok), new Name(this, formal.NameNode), CloneType(formal.Type), formal.InParam, formal.IsGhost,
+       : new Formal(Origin(formal.Origin), new Name(this, formal.NameNode), CloneType(formal.Type), formal.InParam, formal.IsGhost,
          CloneExpr(formal.DefaultValue), CloneAttributes(formal.Attributes),
          formal.IsOld, formal.IsNameOnly, formal.IsOlder, formal.NameForCompilation) {
          IsTypeExplicit = formal.IsTypeExplicit
@@ -282,7 +282,7 @@ public virtual BoundVar CloneBoundVar(BoundVar bv, bool isReference) {
           return bv;
         }
 
-        var bvNew = new BoundVar(Origin(bv.Tok), new Name(this, bv.NameNode), CloneType(bv.SyntacticType));
+        var bvNew = new BoundVar(Origin(bv.Origin), new Name(this, bv.NameNode), CloneType(bv.SyntacticType));
         bvNew.IsGhost = bv.IsGhost;
         return bvNew;
       });
@@ -334,21 +334,21 @@ public Attributes CloneAttributes(Attributes attrs) {
         // skip this attribute, since it would have been produced during resolution
         return CloneAttributes(attrs.Prev);
       } else if (attrs is UserSuppliedAttributes usa) {
-        return new UserSuppliedAttributes(Origin(usa.Tok), Origin(usa.OpenBrace), Origin(usa.CloseBrace),
+        return new UserSuppliedAttributes(Origin(usa.Origin), Origin(usa.OpenBrace), Origin(usa.CloseBrace),
           attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev));
       } else if (attrs is UserSuppliedAtAttribute usaa) {
         var arg = CloneExpr(usaa.Arg);
         if (usaa.Arg.Type != null) { // The attribute has already been expanded
           arg.Type = usaa.Arg.Type;
           arg.PreType = usaa.Arg.PreType;
         }
-        return new UserSuppliedAtAttribute(Origin(usaa.Tok), arg, CloneAttributes(usaa.Prev)) {
+        return new UserSuppliedAtAttribute(Origin(usaa.Origin), arg, CloneAttributes(usaa.Prev)) {
           Builtin = usaa.Builtin
         };
       } else {
-        return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev)) {
-          Origin = Origin(attrs.Origin)
-        };
+        var result = new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev));
+        result.SetOrigin(Origin(attrs.Origin));
+        return result;
       }
     }
 
@@ -380,13 +380,13 @@ public virtual Expression CloneExpr(Expression expr) {
     public MatchCaseExpr CloneMatchCaseExpr(MatchCaseExpr c) {
       Contract.Requires(c != null);
       Contract.Requires(c.Arguments != null);
-      return new MatchCaseExpr(Origin(c.Tok), c.Ctor, c.FromBoundVar,
+      return new MatchCaseExpr(Origin(c.Origin), c.Ctor, c.FromBoundVar,
         c.Arguments.ConvertAll(bv => CloneBoundVar(bv, false)), CloneExpr(c.Body), CloneAttributes(c.Attributes));
     }
 
     public NestedMatchCaseExpr CloneNestedMatchCaseExpr(NestedMatchCaseExpr c) {
       Contract.Requires(c != null);
-      return new NestedMatchCaseExpr(Origin(c.Tok), CloneExtendedPattern(c.Pat), CloneExpr(c.Body),
+      return new NestedMatchCaseExpr(Origin(c.Origin), CloneExtendedPattern(c.Pat), CloneExpr(c.Body),
         CloneAttributes(c.Attributes));
     }
 
@@ -465,11 +465,11 @@ public MatchCaseStmt CloneMatchCaseStmt(MatchCaseStmt c) {
     public ExtendedPattern CloneExtendedPattern(ExtendedPattern pat) {
       switch (pat) {
         case LitPattern p:
-          return new LitPattern(p.Tok, CloneExpr(p.OrigLit));
+          return new LitPattern(p.Origin, CloneExpr(p.OrigLit));
         case IdPattern p:
           return new IdPattern(this, p);
         case DisjunctivePattern p:
-          return new DisjunctivePattern(p.Tok, p.Alternatives.ConvertAll(CloneExtendedPattern), p.IsGhost);
+          return new DisjunctivePattern(p.Origin, p.Alternatives.ConvertAll(CloneExtendedPattern), p.IsGhost);
         default:
           Contract.Assert(false);
           return null;
@@ -478,7 +478,7 @@ public ExtendedPattern CloneExtendedPattern(ExtendedPattern pat) {
 
     public NestedMatchCaseStmt CloneNestedMatchCaseStmt(NestedMatchCaseStmt c) {
       Contract.Requires(c != null);
-      return new NestedMatchCaseStmt(c.Tok, CloneExtendedPattern(c.Pat), c.Body.ConvertAll(stmt => CloneStmt(stmt, false)),
+      return new NestedMatchCaseStmt(c.Origin, CloneExtendedPattern(c.Pat), c.Body.ConvertAll(stmt => CloneStmt(stmt, false)),
         CloneAttributes(c.Attributes));
     }
 
@@ -507,7 +507,7 @@ public void AddStmtLabels(Statement s, LList<Label> node) {
     }
 
     public GuardedAlternative CloneGuardedAlternative(GuardedAlternative alt) {
-      return new GuardedAlternative(Origin(alt.Tok), alt.IsBindingGuard, CloneExpr(alt.Guard),
+      return new GuardedAlternative(Origin(alt.Origin), alt.IsBindingGuard, CloneExpr(alt.Guard),
         alt.Body.ConvertAll(stmt => CloneStmt(stmt, false)), CloneAttributes(alt.Attributes));
     }
 
@@ -613,7 +613,7 @@ public virtual AttributedToken AttributedTok(AttributedToken tok) {
   public class ClonerKeepParensExpressions : Cloner {
     public override Expression CloneExpr(Expression expr) {
       if (expr is ParensExpression parensExpression) {
-        return new ParensExpression(Origin(parensExpression.Tok), CloneExpr(parensExpression.E));
+        return new ParensExpression(Origin(parensExpression.Origin), CloneExpr(parensExpression.E));
       }
 
       return base.CloneExpr(expr);

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

@@ -4,7 +4,7 @@
 
 namespace Microsoft.Dafny;
 
-public class ActualBindings : TokenNode {
+public class ActualBindings : NodeWithComputedRange {
   public readonly List<ActualBinding> ArgumentBindings;
 
   public ActualBindings(List<ActualBinding> argumentBindings) {
@@ -43,7 +43,7 @@ public void AcceptArgumentExpressionsAsExactParameterList(List<Expression> args
   public override IEnumerable<INode> PreResolveChildren => Children;
 }
 
-public class ActualBinding : TokenNode {
+public class ActualBinding : NodeWithComputedRange {
   public readonly IOrigin /*?*/ FormalParameterName;
   public readonly Expression Actual;
   public readonly bool IsGhost;

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

@@ -26,8 +26,8 @@ public ApplyExpr(Cloner cloner, ApplyExpr original) : base(cloner, original) {
     CloseParen = original.CloseParen;
   }
 
-  public ApplyExpr(IOrigin tok, Expression fn, List<Expression> args, Token closeParen)
-    : base(tok) {
+  public ApplyExpr(IOrigin origin, Expression fn, List<Expression> args, Token closeParen)
+    : base(origin) {
     Function = fn;
     Args = args;
     CloseParen = closeParen;

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

@@ -35,9 +35,9 @@ public ApplySuffix(Cloner cloner, ApplySuffix original) :
     Bindings = new ActualBindings(cloner, original.Bindings);
   }
 
-  public ApplySuffix(IOrigin tok, IOrigin/*?*/ atLabel, Expression lhs, List<ActualBinding> args, Token closeParen)
-    : base(tok, lhs) {
-    Contract.Requires(tok != null);
+  public ApplySuffix(IOrigin origin, IOrigin/*?*/ atLabel, Expression lhs, List<ActualBinding> args, Token closeParen)
+    : base(origin, lhs) {
+    Contract.Requires(origin != null);
     Contract.Requires(lhs != null);
     Contract.Requires(cce.NonNullElements(args));
     AtTok = atLabel;

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

@@ -33,9 +33,9 @@ public ExprDotName(Cloner cloner, ExprDotName original) : base(cloner, original)
     OptTypeArguments = original.OptTypeArguments?.ConvertAll(cloner.CloneType);
   }
 
-  public ExprDotName(IOrigin tok, Expression obj, Name suffixName, List<Type> optTypeArguments)
-    : base(tok, obj) {
-    Contract.Requires(tok != null);
+  public ExprDotName(IOrigin origin, Expression obj, Name suffixName, List<Type> optTypeArguments)
+    : base(origin, obj) {
+    Contract.Requires(origin != null);
     Contract.Requires(obj != null);
     Contract.Requires(suffixName != null);
     this.SuffixNameNode = suffixName;

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

@@ -81,19 +81,19 @@ public FunctionCallExpr(string fn, Expression receiver, IOrigin openParen, Token
       atLabel) {
   }
 
-  public FunctionCallExpr(IOrigin tok, Name fn, Expression receiver, IOrigin openParen, Token closeParen, [Captured] List<ActualBinding> args, Label/*?*/ atLabel = null)
-    : this(tok, fn, receiver, openParen, closeParen, new ActualBindings(args), atLabel) {
-    Contract.Requires(tok != null);
+  public FunctionCallExpr(IOrigin origin, Name fn, Expression receiver, IOrigin openParen, Token closeParen, [Captured] List<ActualBinding> args, Label/*?*/ atLabel = null)
+    : this(origin, fn, receiver, openParen, closeParen, new ActualBindings(args), atLabel) {
+    Contract.Requires(origin != null);
     Contract.Requires(fn != null);
     Contract.Requires(receiver != null);
     Contract.Requires(cce.NonNullElements(args));
     Contract.Requires(openParen != null || args.Count == 0);
     Contract.Ensures(type == null);
   }
 
-  public FunctionCallExpr(IOrigin tok, Name fn, Expression receiver, IOrigin openParen, Token closeParen, [Captured] ActualBindings bindings, Label/*?*/ atLabel = null)
-    : base(tok) {
-    Contract.Requires(tok != null);
+  public FunctionCallExpr(IOrigin origin, Name fn, Expression receiver, IOrigin openParen, Token closeParen, [Captured] ActualBindings bindings, Label/*?*/ atLabel = null)
+    : base(origin) {
+    Contract.Requires(origin != null);
     Contract.Requires(fn != null);
     Contract.Requires(receiver != null);
     Contract.Requires(bindings != null);
@@ -113,9 +113,9 @@ public FunctionCallExpr(IOrigin tok, Name fn, Expression receiver, IOrigin openP
   /// This constructor is intended to be used when constructing a resolved FunctionCallExpr. The "args" are expected
   /// to be already resolved, and are all given positionally.
   /// </summary>
-  public FunctionCallExpr(IOrigin tok, Name fn, Expression receiver, IOrigin openParen, Token closeParen, [Captured] List<Expression> args,
+  public FunctionCallExpr(IOrigin origin, Name fn, Expression receiver, IOrigin openParen, Token closeParen, [Captured] List<Expression> args,
     Label /*?*/ atLabel = null)
-    : this(tok, fn, receiver, openParen, closeParen, args.ConvertAll(e => new ActualBinding(null, e)), atLabel) {
+    : this(origin, fn, receiver, openParen, closeParen, args.ConvertAll(e => new ActualBinding(null, e)), atLabel) {
     Bindings.AcceptArgumentExpressionsAsExactParameterList();
   }
 

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

@@ -215,9 +215,9 @@ public MemberSelectExpr(Cloner cloner, MemberSelectExpr original) : base(cloner,
     }
   }
 
-  public MemberSelectExpr(IOrigin tok, Expression obj, Name memberName)
-    : base(tok) {
-    Contract.Requires(tok != null);
+  public MemberSelectExpr(IOrigin origin, Expression obj, Name memberName)
+    : base(origin) {
+    Contract.Requires(origin != null);
     Contract.Requires(obj != null);
     Contract.Requires(memberName != null);
     this.Obj = obj;
@@ -227,9 +227,9 @@ public MemberSelectExpr(IOrigin tok, Expression obj, Name memberName)
   /// <summary>
   /// Returns a resolved MemberSelectExpr for a field.
   /// </summary>
-  public MemberSelectExpr(IOrigin tok, Expression obj, Field field)
-    : this(tok, obj, new Name(field.Name)) {
-    Contract.Requires(tok != null);
+  public MemberSelectExpr(IOrigin origin, Expression obj, Field field)
+    : this(origin, obj, new Name(field.Name)) {
+    Contract.Requires(origin != null);
     Contract.Requires(obj != null);
     Contract.Requires(field != null);
     Contract.Requires(obj.Type != null);  // "obj" is required to be resolved

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

@@ -19,9 +19,9 @@ public MultiSelectExpr(Cloner cloner, MultiSelectExpr original) : base(cloner, o
     Array = cloner.CloneExpr(original.Array);
   }
 
-  public MultiSelectExpr(IOrigin tok, Expression array, List<Expression> indices)
-    : base(tok) {
-    Contract.Requires(tok != null);
+  public MultiSelectExpr(IOrigin origin, Expression array, List<Expression> indices)
+    : base(origin) {
+    Contract.Requires(origin != null);
     Contract.Requires(array != null);
     Contract.Requires(cce.NonNullElements(indices) && 1 <= indices.Count);
 

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

@@ -8,9 +8,9 @@ public class NameSegment : ConcreteSyntaxExpression, ICloneable<NameSegment>, IC
   public readonly string Name;
   public Name NameNode => new Name(Origin, Name);
   public readonly List<Type> OptTypeArguments;
-  public NameSegment(IOrigin tok, string name, List<Type> optTypeArguments)
-    : base(tok) {
-    Contract.Requires(tok != null);
+  public NameSegment(IOrigin origin, string name, List<Type> optTypeArguments)
+    : base(origin) {
+    Contract.Requires(origin != null);
     Contract.Requires(name != null);
     Contract.Requires(optTypeArguments == null || optTypeArguments.Count > 0);
     Name = name;

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

@@ -24,9 +24,9 @@ void ObjectInvariant() {
     Contract.Invariant(!SelectOne || E1 == null);
   }
 
-  public SeqSelectExpr(IOrigin tok, bool selectOne, Expression seq, Expression e0, Expression e1, Token closeParen)
-    : base(tok) {
-    Contract.Requires(tok != null);
+  public SeqSelectExpr(IOrigin origin, bool selectOne, Expression seq, Expression e0, Expression e1, Token closeParen)
+    : base(origin) {
+    Contract.Requires(origin != null);
     Contract.Requires(seq != null);
     Contract.Requires(!selectOne || e1 == null);