No nesting inside RangeToken.StartToken

Source/DafnyCore.Test/ClonerTest.cs

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

Source/DafnyCore.Test/NodeTests.cs

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

Source/DafnyCore/AST/Cloner.cs

@@ -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), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost,
+       : new Formal(Origin(formal.tok), 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) {
          Origin = formal.Origin,
@@ -283,7 +283,7 @@ public virtual BoundVar CloneBoundVar(BoundVar bv, bool isReference) {
           return bv;
         }
 
-        var bvNew = new BoundVar(Origin(bv.tok), bv.Name, CloneType(bv.SyntacticType));
+        var bvNew = new BoundVar(Origin(bv.tok), new Name(this, bv.NameNode), CloneType(bv.SyntacticType));
         bvNew.IsGhost = bv.IsGhost;
         return bvNew;
       });
@@ -596,14 +596,11 @@ public virtual BlockStmt CloneMethodBody(Method m) {
       }
     }
 
-    public virtual RangeToken Origin(RangeToken range) {
-      if (range == null) {
+    public virtual IOrigin Origin(IOrigin tok) {
+      if (tok == null) {
         return null;
       }
-      return new RangeToken(Origin(range.StartToken), Origin(range.EndToken));
-    }
 
-    public virtual IOrigin Origin(IOrigin tok) {
       Contract.Requires(tok != null);
       return tok;
     }

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

@@ -18,15 +18,15 @@ public override IEnumerable<Expression> SubExpressions {
     }
   }
 
-  public IOrigin CloseParen;
+  public Token CloseParen;
 
   public ApplyExpr(Cloner cloner, ApplyExpr original) : base(cloner, original) {
     Function = cloner.CloneExpr(original.Function);
     Args = original.Args.ConvertAll(cloner.CloneExpr);
-    CloseParen = cloner.Origin(original.CloseParen);
+    CloseParen = original.CloseParen;
   }
 
-  public ApplyExpr(IOrigin tok, Expression fn, List<Expression> args, IOrigin closeParen)
+  public ApplyExpr(IOrigin tok, Expression fn, List<Expression> args, Token closeParen)
     : base(tok) {
     Function = fn;
     Args = args;

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

@@ -9,7 +9,7 @@ namespace Microsoft.Dafny;
 /// </summary>
 public class ApplySuffix : SuffixExpr, ICloneable<ApplySuffix>, ICanFormat {
   public readonly IOrigin/*?*/ AtTok;
-  public readonly IOrigin CloseParen;
+  public readonly Token CloseParen;
   public readonly ActualBindings Bindings;
   public List<Expression> Args => Bindings.Arguments;
   [FilledInDuringResolution] public MethodCallInformation MethodCallInfo = null; // resolution will set to a non-null value if ApplySuffix makes a method call
@@ -30,12 +30,12 @@ public ApplySuffix Clone(Cloner cloner) {
   public ApplySuffix(Cloner cloner, ApplySuffix original) :
     base(cloner, original) {
     AtTok = original.AtTok == null ? null : cloner.Origin(original.AtTok);
-    CloseParen = cloner.Origin(original.CloseParen);
+    CloseParen = original.CloseParen;
     FormatTokens = original.FormatTokens;
     Bindings = new ActualBindings(cloner, original.Bindings);
   }
 
-  public ApplySuffix(IOrigin tok, IOrigin/*?*/ atLabel, Expression lhs, List<ActualBinding> args, IOrigin closeParen)
+  public ApplySuffix(IOrigin tok, IOrigin/*?*/ atLabel, Expression lhs, List<ActualBinding> args, Token closeParen)
     : base(tok, lhs) {
     Contract.Requires(tok != null);
     Contract.Requires(lhs != null);
@@ -69,7 +69,7 @@ public override IEnumerable<Expression> PreResolveSubExpressions {
   public static Expression MakeRawApplySuffix(IOrigin tok, string name, List<Expression> args) {
     var nameExpr = new NameSegment(tok, name, null);
     var argBindings = args.ConvertAll(arg => new ActualBinding(null, arg));
-    return new ApplySuffix(tok, null, nameExpr, argBindings, tok);
+    return new ApplySuffix(tok, null, nameExpr, argBindings, Token.NoToken);
   }
 
   public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {

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

@@ -8,7 +8,7 @@ public class FunctionCallExpr : Expression, IHasReferences, ICloneable<FunctionC
   public string Name;
   public readonly Expression Receiver;
   public readonly IOrigin OpenParen;  // can be null if Args.Count == 0
-  public readonly IOrigin CloseParen;
+  public readonly Token CloseParen;
   public readonly Label/*?*/ AtLabel;
   public readonly ActualBindings Bindings;
   public List<Expression> Args => Bindings.Arguments;
@@ -74,7 +74,7 @@ void ObjectInvariant() {
 
   [FilledInDuringResolution] public Function Function;
 
-  public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, IOrigin closeParen, [Captured] List<ActualBinding> args, Label/*?*/ atLabel = null)
+  public FunctionCallExpr(IOrigin tok, string 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);
     Contract.Requires(fn != null);
@@ -84,7 +84,7 @@ public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin ope
     Contract.Ensures(type == null);
   }
 
-  public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, IOrigin closeParen, [Captured] ActualBindings bindings, Label/*?*/ atLabel = null)
+  public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, Token closeParen, [Captured] ActualBindings bindings, Label/*?*/ atLabel = null)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(fn != null);
@@ -106,7 +106,7 @@ public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin ope
   /// 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, string fn, Expression receiver, IOrigin openParen, IOrigin closeParen, [Captured] List<Expression> args,
+  public FunctionCallExpr(IOrigin tok, string 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) {
     Bindings.AcceptArgumentExpressionsAsExactParameterList();
@@ -120,7 +120,7 @@ public FunctionCallExpr(Cloner cloner, FunctionCallExpr original) : base(cloner,
     Name = original.Name;
     Receiver = cloner.CloneExpr(original.Receiver);
     OpenParen = original.OpenParen == null ? null : cloner.Origin(original.OpenParen);
-    CloseParen = original.CloseParen == null ? null : cloner.Origin(original.CloseParen);
+    CloseParen = original.CloseParen;
     Bindings = new ActualBindings(cloner, original.Bindings);
     AtLabel = original.AtLabel;
 

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

@@ -8,14 +8,14 @@ public class SeqSelectExpr : Expression, ICloneable<SeqSelectExpr> {
   public readonly Expression Seq;
   public readonly Expression E0;
   public readonly Expression E1;
-  public readonly IOrigin CloseParen;
+  public readonly Token CloseParen;
 
   public SeqSelectExpr(Cloner cloner, SeqSelectExpr original) : base(cloner, original) {
     SelectOne = original.SelectOne;
     Seq = cloner.CloneExpr(original.Seq);
     E0 = cloner.CloneExpr(original.E0);
     E1 = cloner.CloneExpr(original.E1);
-    CloseParen = cloner.Origin(original.CloseParen);
+    CloseParen = original.CloseParen;
   }
 
   [ContractInvariantMethod]
@@ -24,7 +24,7 @@ void ObjectInvariant() {
     Contract.Invariant(!SelectOne || E1 == null);
   }
 
-  public SeqSelectExpr(IOrigin tok, bool selectOne, Expression seq, Expression e0, Expression e1, IOrigin closeParen)
+  public SeqSelectExpr(IOrigin tok, bool selectOne, Expression seq, Expression e0, Expression e1, Token closeParen)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(seq != null);

Source/DafnyCore/AST/Expressions/AttributedExpression.cs

@@ -25,7 +25,7 @@ public Attributes Attributes {
 
   string IAttributeBearingDeclaration.WhatKind => "expression";
 
-  public override RangeToken Origin => E.Origin;
+  public override IOrigin Origin => E.Origin;
 
   public bool HasAttributes() {
     return Attributes != null;

Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs

@@ -54,7 +54,7 @@ public List<BoundVar> UncompilableBoundVars() {
     return BoundedPool.MissingBounds(BoundVars, Bounds, v);
   }
 
-  public ComprehensionExpr(IOrigin tok, RangeToken rangeOrigin, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
+  public ComprehensionExpr(IOrigin tok, IOrigin rangeOrigin, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(cce.NonNullElements(bvars));

Source/DafnyCore/AST/Expressions/Comprehensions/ExistsExpr.cs

@@ -7,7 +7,7 @@ public class ExistsExpr : QuantifierExpr, ICloneable<ExistsExpr> {
   public override string WhatKind => "exists expression";
   protected override BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.Or; } }
 
-  public ExistsExpr(IOrigin tok, RangeToken rangeOrigin, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
+  public ExistsExpr(IOrigin tok, IOrigin rangeOrigin, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
     : base(tok, rangeOrigin, bvars, range, term, attrs) {
     Contract.Requires(cce.NonNullElements(bvars));
     Contract.Requires(tok != null);

Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs

@@ -7,7 +7,7 @@ public class ForallExpr : QuantifierExpr, ICloneable<ForallExpr> {
   public override string WhatKind => "forall expression";
   protected override BinaryExpr.ResolvedOpcode SplitResolvedOp => BinaryExpr.ResolvedOpcode.And;
 
-  public ForallExpr(IOrigin tok, RangeToken rangeOrigin, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
+  public ForallExpr(IOrigin tok, IOrigin rangeOrigin, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
     : base(tok, rangeOrigin, bvars, range, term, attrs) {
     Contract.Requires(cce.NonNullElements(bvars));
     Contract.Requires(tok != null);

Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs

@@ -10,7 +10,7 @@ public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr>, IFrameScope
 
   public readonly Specification<FrameExpression> Reads;
 
-  public LambdaExpr(IOrigin tok, RangeToken rangeOrigin, List<BoundVar> bvars, Expression requires, Specification<FrameExpression> reads, Expression body)
+  public LambdaExpr(IOrigin tok, IOrigin rangeOrigin, List<BoundVar> bvars, Expression requires, Specification<FrameExpression> reads, Expression body)
     : base(tok, rangeOrigin, bvars, requires, body, null) {
     Contract.Requires(reads != null);
     Reads = reads;

Source/DafnyCore/AST/Expressions/Comprehensions/MapComprehension.cs

@@ -20,7 +20,7 @@ public MapComprehension(Cloner cloner, MapComprehension original) : base(cloner,
     Finite = original.Finite;
   }
 
-  public MapComprehension(IOrigin tok, RangeToken rangeOrigin, bool finite, List<BoundVar> bvars, Expression range, Expression/*?*/ termLeft, Expression termRight, Attributes attrs)
+  public MapComprehension(IOrigin tok, IOrigin rangeOrigin, bool finite, List<BoundVar> bvars, Expression range, Expression/*?*/ termLeft, Expression termRight, Attributes attrs)
     : base(tok, rangeOrigin, bvars, range, termRight, attrs) {
     Contract.Requires(tok != null);
     Contract.Requires(cce.NonNullElements(bvars));

Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs

@@ -50,7 +50,7 @@ public String Refresh(string prefix, FreshIdGenerator idGen) {
     return idGen.FreshId(prefix);
   }
 
-  public QuantifierExpr(IOrigin tok, RangeToken rangeOrigin, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
+  public QuantifierExpr(IOrigin tok, IOrigin rangeOrigin, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
     : base(tok, rangeOrigin, bvars, range, term, attrs) {
     Contract.Requires(tok != null);
     Contract.Requires(cce.NonNullElements(bvars));

Source/DafnyCore/AST/Expressions/Comprehensions/SetComprehension.cs

@@ -27,7 +27,7 @@ public SetComprehension(Cloner cloner, SetComprehension original) : base(cloner,
     Finite = original.Finite;
   }
 
-  public SetComprehension(IOrigin tok, RangeToken rangeOrigin, bool finite, List<BoundVar> bvars, Expression range, Expression/*?*/ term, Attributes attrs)
+  public SetComprehension(IOrigin tok, IOrigin rangeOrigin, bool finite, List<BoundVar> bvars, Expression range, Expression/*?*/ term, Attributes attrs)
     : base(tok, rangeOrigin, bvars, range, term ?? new IdentifierExpr(tok, bvars[0].Name), attrs) {
     Contract.Requires(tok != null);
     Contract.Requires(cce.NonNullElements(bvars));

Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs

@@ -9,7 +9,7 @@ public class NestedMatchCaseStmt : NestedMatchCase, IAttributeBearingDeclaration
   public readonly List<Statement> Body;
   public Attributes Attributes { get; set; }
   string IAttributeBearingDeclaration.WhatKind => "match statement case";
-  public NestedMatchCaseStmt(RangeToken rangeOrigin, ExtendedPattern pat, List<Statement> body) : base(rangeOrigin.StartToken, pat) {
+  public NestedMatchCaseStmt(IOrigin rangeOrigin, ExtendedPattern pat, List<Statement> body) : base(rangeOrigin.StartToken, pat) {
     Origin = rangeOrigin;
     Contract.Requires(body != null);
     this.Body = body;

Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs

@@ -72,7 +72,7 @@ public override IEnumerable<Expression> NonSpecificationSubExpressions {
     }
   }
 
-  public NestedMatchStmt(RangeToken rangeOrigin, Expression source, [Captured] List<NestedMatchCaseStmt> cases, bool usesOptionalBraces, Attributes attrs = null)
+  public NestedMatchStmt(IOrigin rangeOrigin, Expression source, [Captured] List<NestedMatchCaseStmt> cases, bool usesOptionalBraces, Attributes attrs = null)
     : base(rangeOrigin, attrs) {
     Contract.Requires(source != null);
     Contract.Requires(cce.NonNullElements(cases));

Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs

@@ -41,7 +41,6 @@ protected DefaultValueExpression(IOrigin tok, Formal formal, Expression/*?*/ rec
     this.formal = formal;
     this.receiver = receiver;
     this.substMap = substMap;
-    Origin = new RangeToken(tok, tok);
   }
 
   protected DefaultValueExpression(Cloner cloner, DefaultValueExpression original) : base(cloner, original) {

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -752,7 +752,7 @@ public static Expression CreateResolvedCall(IOrigin tok, Expression receiver, Fu
     Contract.Requires(function.Ins.Count == arguments.Count);
     Contract.Requires(function.TypeArgs.Count == typeArguments.Count);
 
-    var call = new FunctionCallExpr(tok, function.Name, receiver, tok, tok, arguments) {
+    var call = new FunctionCallExpr(tok, function.Name, receiver, tok, Token.NoToken, arguments) {
       Function = function,
       Type = function.ResultType,
       TypeApplication_AtEnclosingClass = receiver.Type.TypeArgs,
@@ -775,7 +775,7 @@ public static Expression WrapResolvedCall(FunctionCallExpr call, SystemModuleMan
     };
 
     subst = TypeParameter.SubstitutionMap(call.Function.TypeArgs, call.TypeApplication_JustFunction);
-    return new ApplySuffix(call.tok, null, exprDotName, new ActualBindings(call.Args).ArgumentBindings, call.tok) {
+    return new ApplySuffix(call.tok, null, exprDotName, new ActualBindings(call.Args).ArgumentBindings, call.CloseParen) {
       ResolvedExpression = call,
       Type = call.Function.ResultType.Subst(subst)
     };

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

@@ -8,7 +8,11 @@ namespace Microsoft.Dafny;
 [DebuggerDisplay("Bound<{name}>")]
 public class BoundVar : NonglobalVariable {
   public override bool IsMutable => false;
-  public BoundVar(IOrigin tok, string name, Type type)
+
+  public BoundVar(string name, Type type) : this(Token.NoToken, new Name(Token.NoToken, name), type) { }
+  public BoundVar(IOrigin origin, string name, Type type) : this(origin, new Name(origin.StartToken, name), type) { }
+
+  public BoundVar(IOrigin tok, Name name, Type type)
     : base(tok, name, type, false) {
     Contract.Requires(tok != null);
     Contract.Requires(name != null);
@@ -86,6 +90,10 @@ class QuantifiedVariableDomainCloner : Cloner {
   public static readonly QuantifiedVariableDomainCloner Instance = new QuantifiedVariableDomainCloner();
   private QuantifiedVariableDomainCloner() { }
   public override IOrigin Origin(IOrigin tok) {
+    if (tok == null) {
+      return null;
+    }
+
     return new QuantifiedVariableDomainOrigin(tok);
   }
 }
@@ -94,6 +102,10 @@ class QuantifiedVariableRangeCloner : Cloner {
   public static readonly QuantifiedVariableRangeCloner Instance = new QuantifiedVariableRangeCloner();
   private QuantifiedVariableRangeCloner() { }
   public override IOrigin Origin(IOrigin tok) {
+    if (tok == null) {
+      return null;
+    }
+
     return new QuantifiedVariableRangeOrigin(tok);
   }
 }

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

@@ -18,19 +18,26 @@ public class Formal : NonglobalVariable {
   public Formal(IOrigin tok, string name, Type type, bool inParam, bool isGhost, Expression defaultValue,
     Attributes attributes = null,
     bool isOld = false, bool isNameOnly = false, bool isOlder = false, string nameForCompilation = null)
-    : base(tok, name, type, isGhost) {
+    : this(tok, new Name(tok.StartToken, name), type, inParam, isGhost, defaultValue, attributes,
+      isOld, isNameOnly, isOlder, nameForCompilation) {
+  }
+
+  public Formal(IOrigin tok, Name nameNode, Type type, bool inParam, bool isGhost, Expression defaultValue,
+    Attributes attributes = null,
+    bool isOld = false, bool isNameOnly = false, bool isOlder = false, string nameForCompilation = null)
+    : base(tok, nameNode, type, isGhost) {
     Contract.Requires(tok != null);
-    Contract.Requires(name != null);
+    Contract.Requires(nameNode != null);
     Contract.Requires(type != null);
     Contract.Requires(inParam || defaultValue == null);
-    Contract.Requires(!isNameOnly || (inParam && !name.StartsWith("#")));
+    Contract.Requires(!isNameOnly || (inParam && !nameNode.Value.StartsWith("#")));
     InParam = inParam;
     IsOld = isOld;
     DefaultValue = defaultValue;
     Attributes = attributes;
     IsNameOnly = isNameOnly;
     IsOlder = isOlder;
-    NameForCompilation = nameForCompilation ?? name;
+    NameForCompilation = nameForCompilation ?? nameNode.Value;
   }
 
   public bool HasName => !Name.StartsWith("#");