Two renames related to tokens (#5990)

### What was changed?
- Replace some usages of `.tok` with `.Tok`
- Rename `RangeToken` to `SourceOrigin`

### How has this been tested?
Pure refactoring

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

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.Tok,
             $"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.Tok,
             $"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

@@ -24,14 +24,14 @@ public override string GetDescription(DafnyOptions options) {
   [Fact]
   public void ClonerKeepsBodyStartTok() {
     var tokenBodyStart = new Token() { line = 2 };
-    var rangeToken = new RangeToken(Token.NoToken, Token.NoToken);
+    var rangeToken = new SourceOrigin(Token.NoToken, Token.NoToken);
     var specificationFrame = new LiteralExpr(Microsoft.Dafny.Token.NoToken, 1);
     var formal1 = new Formal(Token.NoToken, "a", Microsoft.Dafny.Type.Bool, true, false, null) {
-      Origin = new RangeToken(tokenBodyStart, tokenBodyStart),
+      Origin = new SourceOrigin(tokenBodyStart, tokenBodyStart),
       IsTypeExplicit = true
     };
     var formal2 = new Formal(Token.NoToken, "b", Microsoft.Dafny.Type.Bool, true, false, null) {
-      Origin = new RangeToken(tokenBodyStart, tokenBodyStart),
+      Origin = new SourceOrigin(tokenBodyStart, tokenBodyStart),
       IsTypeExplicit = false
     };
     var dummyDecl = new Method(rangeToken, new Name(rangeToken, "hello"),

Source/DafnyCore.Test/NodeTests.cs

@@ -17,15 +17,15 @@ public ConcreteNode(IOrigin rangeOrigin, IEnumerable<INode>? children = null) {
     public override IEnumerable<INode> PreResolveChildren => Children;
   }
 
-  private static RangeToken CreateRange(Uri uri, int startLine, int startColumn, int endLine, int endColumn) {
-    return new RangeToken(new Token(startLine + 1, startColumn + 1) { Uri = uri }, new Token(endLine + 1, endColumn + 1) { Uri = uri });
+  private static SourceOrigin CreateRange(Uri uri, int startLine, int startColumn, int endLine, int endColumn) {
+    return new SourceOrigin(new Token(startLine + 1, startColumn + 1) { Uri = uri }, new Token(endLine + 1, endColumn + 1) { Uri = uri });
   }
 
   [Fact]
   public void FindNodeWithTokenLessIntermediate() {
     var uri = new Uri(Directory.GetCurrentDirectory());
     var child = new ConcreteNode(CreateRange(uri, 0, 1, 0, 2));
-    var parent = new ConcreteNode(RangeToken.NoToken, (IEnumerable<INode>)new INode[] { child });
+    var parent = new ConcreteNode(SourceOrigin.NoToken, (IEnumerable<INode>)new INode[] { child });
     var grandParent = new ConcreteNode(CreateRange(uri, 0, 0, 0, 3), (IEnumerable<INode>)new INode[] { parent });
 
     var shouldBeChild = grandParent.FindNode<INode>(uri, new DafnyPosition(0, 1));
@@ -35,7 +35,7 @@ public void FindNodeWithTokenLessIntermediate() {
   [Fact]
   public void SkipTokenlessLeaf() {
     var uri = new Uri(Directory.GetCurrentDirectory());
-    var child1 = new ConcreteNode(RangeToken.NoToken);
+    var child1 = new ConcreteNode(SourceOrigin.NoToken);
     var child2 = new ConcreteNode(CreateRange(uri, 0, 1, 0, 2));
 
     var parent = new ConcreteNode(CreateRange(uri, 0, 0, 0, 3), (IEnumerable<INode>)new[] { child1, child2 });

Source/DafnyCore/AST/Attributes.cs

@@ -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.Tok,
       attrs, resolutionContext, typeMap, null);
     resolver.FillInDefaultValueExpressions();
     resolver.SolveAllTypeConstraints();

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.Tok), 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.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), new Name(this, bv.NameNode), CloneType(bv.SyntacticType));
+        var bvNew = new BoundVar(Origin(bv.Tok), new Name(this, bv.NameNode), CloneType(bv.SyntacticType));
         bvNew.IsGhost = bv.IsGhost;
         return bvNew;
       });
@@ -335,7 +335,7 @@ 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.Tok), Origin(usa.OpenBrace), Origin(usa.CloseBrace),
           attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev)) {
           Origin = Origin(usa.Origin)
         };
@@ -345,7 +345,7 @@ public Attributes CloneAttributes(Attributes attrs) {
           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.Tok), arg, CloneAttributes(usaa.Prev)) {
           Origin = Origin(usaa.Origin),
           Builtin = usaa.Builtin
         };
@@ -384,7 +384,7 @@ 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.Tok), c.Ctor, c.FromBoundVar,
         c.Arguments.ConvertAll(bv => CloneBoundVar(bv, false)), CloneExpr(c.Body), CloneAttributes(c.Attributes));
     }
 
@@ -617,7 +617,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.Tok), CloneExpr(parensExpression.E));
       }
 
       return base.CloneExpr(expr);

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

@@ -17,12 +17,12 @@ public ThisExpr(IOrigin tok)
   /// to obtain a Dafny "this" expression.
   /// </summary>
   public ThisExpr(MemberDecl m)
-    : base(m.tok) {
+    : base(m.Tok) {
     Contract.Requires(m != null);
-    Contract.Requires(m.tok != null);
+    Contract.Requires(m.Tok != null);
     Contract.Requires(m.EnclosingClass != null);
     Contract.Requires(!m.IsStatic);
-    Type = ModuleResolver.GetReceiverType(m.tok, m);
+    Type = ModuleResolver.GetReceiverType(m.Tok, m);
   }
 
   /// <summary>
@@ -31,10 +31,10 @@ public ThisExpr(MemberDecl m)
   /// to obtain a Dafny "this" expression.
   /// </summary>
   public ThisExpr(TopLevelDeclWithMembers cl)
-    : base(cl.tok) {
+    : base(cl.Tok) {
     Contract.Requires(cl != null);
-    Contract.Requires(cl.tok != null);
-    Type = ModuleResolver.GetThisType(cl.tok, cl);
+    Contract.Requires(cl.Tok != null);
+    Type = ModuleResolver.GetThisType(cl.Tok, cl);
   }
 
   public ThisExpr Clone(Cloner cloner) {

Source/DafnyCore/AST/Expressions/AutoGeneratedExpression.cs

@@ -30,7 +30,7 @@ public AutoGeneratedExpression(Cloner cloner, AutoGeneratedExpression original)
   /// </summary>
   public static AutoGeneratedExpression Create(Expression e, IOrigin token = null) {
     Contract.Requires(e != null);
-    var a = new AutoGeneratedExpression(token ?? e.tok, e);
+    var a = new AutoGeneratedExpression(token ?? e.Tok, e);
     a.type = e.Type;
     a.ResolvedExpression = e;
     return a;

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

@@ -86,8 +86,8 @@ protected ComprehensionExpr(Cloner cloner, ComprehensionExpr original) : base(cl
 
   public override IEnumerable<INode> PreResolveChildren =>
     Attributes.AsEnumerable()
-      .Concat<Node>(Range != null && Range.tok.line > 0 ? new List<Node>() { Range } : new List<Node>())
-    .Concat(Term != null && Term.tok.line > 0 ? new List<Node> { Term } : new List<Node>());
+      .Concat<Node>(Range != null && Range.Tok.line > 0 ? new List<Node>() { Range } : new List<Node>())
+    .Concat(Term != null && Term.Tok.line > 0 ? new List<Node> { Term } : new List<Node>());
 
   public override IEnumerable<Expression> SubExpressions {
     get {

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

@@ -25,7 +25,7 @@ public override Expression LogicalBody(bool bypassSplitQuantifier = false) {
     if (Range == null) {
       return Term;
     }
-    var body = new BinaryExpr(Term.tok, BinaryExpr.Opcode.And, Range, Term);
+    var body = new BinaryExpr(Term.Tok, BinaryExpr.Opcode.And, Range, Term);
     body.ResolvedOp = BinaryExpr.ResolvedOpcode.And;
     body.Type = Term.Type;
     return body;
@@ -48,10 +48,10 @@ public Expression AlphaRename(string prefix) {
     var var4var = new Dictionary<BoundVar, BoundVar>();
     var bvars = new List<BoundVar>();
     foreach (var bv in BoundVars) {
-      var newBv = new BoundVar(bv.tok, prefix + bv.Name, bv.Type);
+      var newBv = new BoundVar(bv.Tok, prefix + bv.Name, bv.Type);
       bvars.Add(newBv);
       var4var.Add(bv, newBv);
-      var ie = new IdentifierExpr(newBv.tok, newBv.Name);
+      var ie = new IdentifierExpr(newBv.Tok, newBv.Name);
       ie.Var = newBv;  // resolve here
       ie.Type = newBv.Type;  // resolve here
       substMap.Add(bv, ie);
@@ -60,7 +60,7 @@ public Expression AlphaRename(string prefix) {
     var range = Range == null ? null : s.Substitute(Range);
     var term = s.Substitute(Term);
     var attrs = s.SubstAttributes(Attributes);
-    var ex = new ExistsExpr(tok, Origin, bvars, range, term, attrs);
+    var ex = new ExistsExpr(Tok, Origin, bvars, range, term, attrs);
     ex.Type = Type.Bool;
     ex.Bounds = s.SubstituteBoundedPoolList(Bounds);
     return ex;

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

@@ -25,7 +25,7 @@ public override Expression LogicalBody(bool bypassSplitQuantifier = false) {
     if (Range == null) {
       return Term;
     }
-    var body = new BinaryExpr(Term.tok, BinaryExpr.Opcode.Imp, Range, Term);
+    var body = new BinaryExpr(Term.Tok, BinaryExpr.Opcode.Imp, Range, Term);
     body.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;
     body.Type = Term.Type;
     return body;

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

@@ -17,7 +17,7 @@ private Expression SplitQuantifierToExpression() {
     Contract.Requires(SplitQuantifier != null && SplitQuantifier.Any());
     Expression accumulator = SplitQuantifier[0];
     for (int tid = 1; tid < SplitQuantifier.Count; tid++) {
-      accumulator = new BinaryExpr(Term.tok, SplitResolvedOp, accumulator, SplitQuantifier[tid]);
+      accumulator = new BinaryExpr(Term.Tok, SplitResolvedOp, accumulator, SplitQuantifier[tid]);
     }
     return accumulator;
   }

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

@@ -36,7 +36,7 @@ public void Resolve(ModuleResolver resolver,
     var afterResolveErrorCount = resolver.reporter.ErrorCount;
     if (beforeResolveErrorCount == afterResolveErrorCount) {
       resolver.ResolveExpression(Body, resolutionContext);
-      resolver.ConstrainSubtypeRelation(resultType, Body.Type, Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", Body.Type, resultType);
+      resolver.ConstrainSubtypeRelation(resultType, Body.Type, Body.Tok, "type of case bodies do not agree (found {0}, previous types {1})", Body.Type, resultType);
     }
   }
 

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

@@ -21,7 +21,7 @@ public NestedMatchCaseStmt(IOrigin tok, ExtendedPattern pat, List<Statement> bod
     this.Attributes = attrs;
   }
 
-  private NestedMatchCaseStmt(Cloner cloner, NestedMatchCaseStmt original) : base(original.tok, original.Pat) {
+  private NestedMatchCaseStmt(Cloner cloner, NestedMatchCaseStmt original) : base(original.Tok, original.Pat) {
     this.Body = original.Body.Select(stmt => cloner.CloneStmt(stmt, false)).ToList();
     this.Attributes = cloner.CloneAttributes(original.Attributes);
   }

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

@@ -65,13 +65,13 @@ public void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext
       resolver.PartiallySolveTypeConstraints(true);
 
       if (Source.Type is TypeProxy) {
-        resolver.reporter.Error(MessageSource.Resolver, tok, "Could not resolve the type of the source of the match expression. Please provide additional typing annotations.");
+        resolver.reporter.Error(MessageSource.Resolver, Tok, "Could not resolve the type of the source of the match expression. Please provide additional typing annotations.");
         return;
       }
     }
 
     var errorCount = resolver.reporter.Count(ErrorLevel.Error);
-    var sourceType = resolver.PartiallyResolveTypeForMemberSelection(Source.tok, Source.Type).NormalizeExpand();
+    var sourceType = resolver.PartiallyResolveTypeForMemberSelection(Source.Tok, Source.Type).NormalizeExpand();
     if (resolver.reporter.Count(ErrorLevel.Error) != errorCount) {
       return;
     }

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

@@ -101,7 +101,7 @@ public void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext
     }
 
     var errorCount = resolver.Reporter.Count(ErrorLevel.Error);
-    var sourceType = resolver.PartiallyResolveTypeForMemberSelection(Source.tok, Source.Type).NormalizeExpand();
+    var sourceType = resolver.PartiallyResolveTypeForMemberSelection(Source.Tok, Source.Type).NormalizeExpand();
     CheckLinearNestedMatchStmt(sourceType, resolutionContext, resolver);
     if (resolver.Reporter.Count(ErrorLevel.Error) != errorCount) {
       return;

Source/DafnyCore/AST/Expressions/Conditional/Patterns/LitPattern.cs

@@ -39,11 +39,11 @@ public LiteralExpr OptimisticallyDesugaredLit {
         if (OrigLit is NegationExpression neg) {
           var lit = (LiteralExpr)neg.E;
           if (lit.Value is BaseTypes.BigDec d) {
-            optimisticallyDesugaredLit = new LiteralExpr(neg.tok, -d);
+            optimisticallyDesugaredLit = new LiteralExpr(neg.Tok, -d);
           } else {
             var n = (BigInteger)lit.Value;
-            var tok = new Token(neg.tok.line, neg.tok.col) {
-              Uri = neg.tok.Uri,
+            var tok = new Token(neg.Tok.line, neg.Tok.col) {
+              Uri = neg.Tok.Uri,
               val = "-0"
             };
             optimisticallyDesugaredLit = new LiteralExpr(tok, -n);
@@ -81,7 +81,7 @@ public override void Resolve(ModuleResolver resolver,
 
     var literal = OptimisticallyDesugaredLit;
     resolver.ResolveExpression(literal, resolutionContext);
-    resolver.AddAssignableConstraint(literal.tok, sourceType, literal.Type,
+    resolver.AddAssignableConstraint(literal.Tok, sourceType, literal.Type,
       "literal expression in case (of type '{1}') not assignable to match source type '{0}'");
   }
 }

Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs

@@ -61,7 +61,7 @@ public void FillIn(ModuleResolver resolver, Dictionary<DefaultValueExpression, W
         resolver.reporter.Error(MessageSource.Resolver, this,
           "default-valued expressions are cyclicly dependent; this is not allowed, since it would cause infinite expansion");
         // nevertheless, to avoid any issues in the resolver, fill in the .ResolvedExpression field with something
-        this.ResolvedExpression = Expression.CreateBoolLiteral(this.tok, false);
+        this.ResolvedExpression = Expression.CreateBoolLiteral(this.Tok, false);
       }
       return;
     }