Rename some things that are not lexical tokens, from Token to Origin (#…

…5956)

This PR extract some refactorings from
#5931 to make that PR easier to
review.

### Description
- Rename some things that are not lexical tokens, from Token to Origin.
In particular, `Microsoft.Dafny.IToken` is now
`Microsoft.Dafny.IOrigin`. Same renaming is done for classes that
inherit from `IToken`, except `Token` and `RangeToken`
- Extract two classes into separate files, `IOrigin` and `OriginWrapper`
- Note: there are same locations where lexical tokens are handled,
particularly in the parser and the formatter, where the name `IOrigin`
does not make sense. That is addressed by this PR:
#5957

### How has this been tested?
Pure refactoring, covered by existing tests

<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/DafnyCore.Test/ClonerTest.cs

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

Source/DafnyCore.Test/NodeTests.cs

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

Source/DafnyCore/AST/Attributes.cs

@@ -681,10 +681,10 @@ public static IEnumerable<Attributes> AsEnumerable(this Attributes attr) {
 
 // {:..} Attributes parsed are built using this class
 public class UserSuppliedAttributes : Attributes {
-  public readonly IToken OpenBrace;
-  public readonly IToken CloseBrace;
+  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(IToken tok, IToken openBrace, IToken closeBrace, List<Expression> args, Attributes prev)
+  public UserSuppliedAttributes(IOrigin tok, IOrigin openBrace, IOrigin closeBrace, List<Expression> args, Attributes prev)
     : base(tok.val, args, prev) {
     Contract.Requires(tok != null);
     Contract.Requires(openBrace != null);
@@ -699,10 +699,10 @@ public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, L
 // @-Attributes parsed are built using this class
 public class UserSuppliedAtAttribute : Attributes {
   public static readonly string AtName = "@";
-  public readonly IToken AtSign;
+  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(IToken tok, Expression arg, Attributes prev)
+  public UserSuppliedAtAttribute(IOrigin tok, Expression arg, Attributes prev)
     : base(AtName, new List<Expression>() { arg }, prev) {
     Contract.Requires(tok != null);
     this.tok = tok;

Source/DafnyCore/AST/Cloner.cs

@@ -603,7 +603,7 @@ public virtual RangeToken Range(RangeToken range) {
       return new RangeToken(Tok(range.StartToken), Tok(range.EndToken));
     }
 
-    public virtual IToken Tok(IToken tok) {
+    public virtual IOrigin Tok(IOrigin tok) {
       Contract.Requires(tok != null);
       return tok;
     }

Source/DafnyCore/AST/DafnyInterface.dfy

@@ -1,18 +1,18 @@
 include "System.dfy"
 
-// Interface with existing Dafny code (IToken)
+// Interface with existing Dafny code (IOrigin)
 @Compile(false)
 @Options("-functionSyntax:4")
 module {:extern "Microsoft.Dafny"} MicrosoftDafny {
   import opened System
 
   @Compile(false)
-  trait {:extern "IToken"} IToken {
+  trait {:extern "IOrigin"} IOrigin {
     var val: CsString
     var LeadingTrivia: CsString
     var TrailingTrivia: CsString
-    var Next: IToken?
-    ghost var allTokens: seq<IToken>
+    var Next: IOrigin?
+    ghost var allTokens: seq<IOrigin>
 
     ghost predicate Valid() reads this, allTokens decreases |allTokens| {
       && |allTokens| > 0 && allTokens[0] == this
@@ -34,7 +34,7 @@ module {:extern "Microsoft.Dafny"} MicrosoftDafny {
         this.Next.AlltokenSpec(i - 1);
       }
     }
-    lemma TokenNextIsIPlus1(middle: IToken, i: int)
+    lemma TokenNextIsIPlus1(middle: IOrigin, i: int)
       requires Valid()
       requires 0 <= i < |allTokens|
       requires allTokens[i] == middle
@@ -47,7 +47,7 @@ module {:extern "Microsoft.Dafny"} MicrosoftDafny {
       }
     }
 
-    lemma TokenNextIsNullImpliesLastToken(middle: IToken, i: int)
+    lemma TokenNextIsNullImpliesLastToken(middle: IOrigin, i: int)
       requires middle.Valid() && this.Valid()
       requires 0 <= i < |allTokens|
       requires middle == allTokens[i]

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

@@ -14,7 +14,7 @@ public ActualBindings(List<ActualBinding> argumentBindings) {
 
   public ActualBindings(Cloner cloner, ActualBindings original) {
     ArgumentBindings = original.ArgumentBindings.Select(actualBinding => new ActualBinding(
-      actualBinding.FormalParameterName == null ? null : cloner.Tok((IToken)actualBinding.FormalParameterName),
+      actualBinding.FormalParameterName == null ? null : cloner.Tok((IOrigin)actualBinding.FormalParameterName),
       cloner.CloneExpr(actualBinding.Actual))).ToList();
     if (cloner.CloneResolvedFields) {
       arguments = original.Arguments?.Select(cloner.CloneExpr).ToList();
@@ -44,15 +44,15 @@ public void AcceptArgumentExpressionsAsExactParameterList(List<Expression> args
 }
 
 public class ActualBinding : TokenNode {
-  public readonly IToken /*?*/ FormalParameterName;
+  public readonly IOrigin /*?*/ FormalParameterName;
   public readonly Expression Actual;
   public readonly bool IsGhost;
 
   public override IEnumerable<INode> Children => new List<Node> { Actual }.Where(x => x != null);
 
   public override IEnumerable<INode> PreResolveChildren => Children;
 
-  public ActualBinding(IToken /*?*/ formalParameterName, Expression actual, bool isGhost = false) {
+  public ActualBinding(IOrigin /*?*/ formalParameterName, Expression actual, bool isGhost = false) {
     Contract.Requires(actual != null);
     FormalParameterName = formalParameterName;
     Actual = actual;

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

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

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

@@ -8,8 +8,8 @@ namespace Microsoft.Dafny;
 /// An ApplySuffix desugars into either an ApplyExpr or a FunctionCallExpr
 /// </summary>
 public class ApplySuffix : SuffixExpr, ICloneable<ApplySuffix>, ICanFormat {
-  public readonly IToken/*?*/ AtTok;
-  public readonly IToken CloseParen;
+  public readonly IOrigin/*?*/ AtTok;
+  public readonly IOrigin 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
@@ -35,7 +35,7 @@ public ApplySuffix(Cloner cloner, ApplySuffix original) :
     Bindings = new ActualBindings(cloner, original.Bindings);
   }
 
-  public ApplySuffix(IToken tok, IToken/*?*/ atLabel, Expression lhs, List<ActualBinding> args, IToken closeParen)
+  public ApplySuffix(IOrigin tok, IOrigin/*?*/ atLabel, Expression lhs, List<ActualBinding> args, IOrigin closeParen)
     : base(tok, lhs) {
     Contract.Requires(tok != null);
     Contract.Requires(lhs != null);
@@ -66,7 +66,7 @@ public override IEnumerable<Expression> PreResolveSubExpressions {
   /// <param name="name">The name of the target function or method.</param>
   /// <param name="args">The arguments to apply the function or method to.</param>
   /// <returns></returns>
-  public static Expression MakeRawApplySuffix(IToken tok, string name, List<Expression> args) {
+  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);

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

@@ -32,7 +32,7 @@ public ExprDotName(Cloner cloner, ExprDotName original) : base(cloner, original)
     OptTypeArguments = original.OptTypeArguments?.ConvertAll(cloner.CloneType);
   }
 
-  public ExprDotName(IToken tok, Expression obj, string suffixName, List<Type> optTypeArguments)
+  public ExprDotName(IOrigin tok, Expression obj, string suffixName, List<Type> optTypeArguments)
     : base(tok, obj) {
     Contract.Requires(tok != null);
     Contract.Requires(obj != null);

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

@@ -7,8 +7,8 @@ namespace Microsoft.Dafny;
 public class FunctionCallExpr : Expression, IHasReferences, ICloneable<FunctionCallExpr> {
   public string Name;
   public readonly Expression Receiver;
-  public readonly IToken OpenParen;  // can be null if Args.Count == 0
-  public readonly IToken CloseParen;
+  public readonly IOrigin OpenParen;  // can be null if Args.Count == 0
+  public readonly IOrigin 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(IToken tok, string fn, Expression receiver, IToken openParen, IToken closeParen, [Captured] List<ActualBinding> args, Label/*?*/ atLabel = null)
+  public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, IOrigin 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(IToken tok, string fn, Expression receiver, IToken openP
     Contract.Ensures(type == null);
   }
 
-  public FunctionCallExpr(IToken tok, string fn, Expression receiver, IToken openParen, IToken closeParen, [Captured] ActualBindings bindings, Label/*?*/ atLabel = null)
+  public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, IOrigin closeParen, [Captured] ActualBindings bindings, Label/*?*/ atLabel = null)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(fn != null);
@@ -106,7 +106,7 @@ public FunctionCallExpr(IToken tok, string fn, Expression receiver, IToken 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(IToken tok, string fn, Expression receiver, IToken openParen, IToken closeParen, [Captured] List<Expression> args,
+  public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, IOrigin closeParen, [Captured] List<Expression> args,
     Label /*?*/ atLabel = null)
     : this(tok, fn, receiver, openParen, closeParen, args.ConvertAll(e => new ActualBinding(null, e)), atLabel) {
     Bindings.AcceptArgumentExpressionsAsExactParameterList();
@@ -148,5 +148,5 @@ public IEnumerable<IHasNavigationToken> GetReferences() {
     return Enumerable.Repeat(Function, 1);
   }
 
-  public IToken NavigationToken => tok;
+  public IOrigin NavigationToken => tok;
 }

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

@@ -214,7 +214,7 @@ public MemberSelectExpr(Cloner cloner, MemberSelectExpr original) : base(cloner,
     }
   }
 
-  public MemberSelectExpr(IToken tok, Expression obj, string memberName)
+  public MemberSelectExpr(IOrigin tok, Expression obj, string memberName)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(obj != null);
@@ -226,7 +226,7 @@ public MemberSelectExpr(IToken tok, Expression obj, string memberName)
   /// <summary>
   /// Returns a resolved MemberSelectExpr for a field.
   /// </summary>
-  public MemberSelectExpr(IToken tok, Expression obj, Field field)
+  public MemberSelectExpr(IOrigin tok, Expression obj, Field field)
     : this(tok, obj, field.Name) {
     Contract.Requires(tok != null);
     Contract.Requires(obj != null);
@@ -297,5 +297,5 @@ public IEnumerable<IHasNavigationToken> GetReferences() {
     return new[] { Member };
   }
 
-  public IToken NavigationToken => tok;
+  public IOrigin NavigationToken => tok;
 }

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

@@ -19,7 +19,7 @@ public MultiSelectExpr(Cloner cloner, MultiSelectExpr original) : base(cloner, o
     Array = cloner.CloneExpr(original.Array);
   }
 
-  public MultiSelectExpr(IToken tok, Expression array, List<Expression> indices)
+  public MultiSelectExpr(IOrigin tok, Expression array, List<Expression> indices)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(array != null);

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

@@ -7,7 +7,7 @@ namespace Microsoft.Dafny;
 public class NameSegment : ConcreteSyntaxExpression, ICloneable<NameSegment>, ICanFormat {
   public readonly string Name;
   public readonly List<Type> OptTypeArguments;
-  public NameSegment(IToken tok, string name, List<Type> optTypeArguments)
+  public NameSegment(IOrigin tok, string name, List<Type> optTypeArguments)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(name != null);

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

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

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

@@ -21,7 +21,7 @@ public class StaticReceiverExpr : LiteralExpr, ICloneable<StaticReceiverExpr> {
   /// </summary>
   public Expression ContainerExpression;
 
-  public StaticReceiverExpr(IToken tok, Type t, bool isImplicit)
+  public StaticReceiverExpr(IOrigin tok, Type t, bool isImplicit)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(t != null);
@@ -38,7 +38,7 @@ public StaticReceiverExpr(Cloner cloner, StaticReceiverExpr original) : base(clo
   /// Constructs a resolved LiteralExpr representing the fictitious static-receiver literal whose type is
   /// "cl" parameterized by the type arguments of "cl" itself.
   /// </summary>
-  public StaticReceiverExpr(IToken tok, TopLevelDeclWithMembers cl, bool isImplicit, Expression lhs = null)
+  public StaticReceiverExpr(IOrigin tok, TopLevelDeclWithMembers cl, bool isImplicit, Expression lhs = null)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(cl != null);
@@ -62,7 +62,7 @@ public StaticReceiverExpr(IToken tok, TopLevelDeclWithMembers cl, bool isImplici
   ///   a trait that in turn extends trait "W(g(Y))".  If "t" denotes type "C(G)" and "cl" denotes "W",
   ///   then type of the StaticReceiverExpr will be "T(g(f(G)))".
   /// </summary>
-  public StaticReceiverExpr(IToken tok, UserDefinedType t, TopLevelDeclWithMembers cl, bool isImplicit, Expression lhs = null)
+  public StaticReceiverExpr(IOrigin tok, UserDefinedType t, TopLevelDeclWithMembers cl, bool isImplicit, Expression lhs = null)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(t.ResolvedClass != null);

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

@@ -42,7 +42,7 @@ protected SuffixExpr(Cloner cloner, SuffixExpr original) : base(cloner, original
     Lhs = cloner.CloneExpr(original.Lhs);
   }
 
-  public SuffixExpr(IToken tok, Expression lhs)
+  public SuffixExpr(IOrigin tok, Expression lhs)
     : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(lhs != null);

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

@@ -6,7 +6,7 @@ public class ThisExpr : Expression, ICloneable<ThisExpr> {
   public ThisExpr(Cloner cloner, ThisExpr original) : base(cloner, original) {
   }
 
-  public ThisExpr(IToken tok)
+  public ThisExpr(IOrigin tok)
     : base(tok) {
     Contract.Requires(tok != null);
   }
@@ -46,8 +46,8 @@ public class ImplicitThisExpr : ThisExpr, ICloneable<ImplicitThisExpr> {
   public ImplicitThisExpr(Cloner cloner, ImplicitThisExpr original) : base(cloner, original) {
   }
 
-  public ImplicitThisExpr(IToken tok)
-    : base(new AutoGeneratedToken(tok)) {
+  public ImplicitThisExpr(IOrigin tok)
+    : base(new AutoGeneratedOrigin(tok)) {
     Contract.Requires(tok != null);
   }
 
@@ -70,7 +70,7 @@ public class ImplicitThisExpr_ConstructorCall : ImplicitThisExpr, ICloneable<Imp
   public ImplicitThisExpr_ConstructorCall(Cloner cloner, ImplicitThisExpr_ConstructorCall original) : base(cloner, original) {
   }
 
-  public ImplicitThisExpr_ConstructorCall(IToken tok)
+  public ImplicitThisExpr_ConstructorCall(IOrigin tok)
     : base(tok) {
     Contract.Requires(tok != null);
   }

Source/DafnyCore/AST/Expressions/AttributedExpression.cs

@@ -47,10 +47,10 @@ public AttributedExpression(Expression e, AssertLabel/*?*/ label, Attributes att
     this.tok = e.Tok;
   }
 
-  public void AddCustomizedErrorMessage(IToken tok, string s) {
+  public void AddCustomizedErrorMessage(IOrigin tok, string s) {
     var args = new List<Expression>() { new StringLiteralExpr(tok, s, true) };
-    IToken openBrace = tok;
-    IToken closeBrace = new Token(tok.line, tok.col + 7 + s.Length + 1); // where 7 = length(":error ")
+    IOrigin openBrace = tok;
+    IOrigin closeBrace = new Token(tok.line, tok.col + 7 + s.Length + 1); // where 7 = length(":error ")
     this.Attributes = new UserSuppliedAttributes(tok, openBrace, closeBrace, args, this.Attributes);
   }
 

Source/DafnyCore/AST/Expressions/AutoGeneratedExpression.cs

@@ -11,7 +11,7 @@ namespace Microsoft.Dafny;
 /// </summary>
 // TODO replace this with AutoGeneratedToken.
 public class AutoGeneratedExpression : ParensExpression, ICloneable<AutoGeneratedExpression> {
-  public AutoGeneratedExpression(IToken tok, Expression e)
+  public AutoGeneratedExpression(IOrigin tok, Expression e)
     : base(tok, e) {
     Contract.Requires(tok != null);
     Contract.Requires(e != null);
@@ -28,7 +28,7 @@ public AutoGeneratedExpression(Cloner cloner, AutoGeneratedExpression original)
   /// This maker method takes a resolved expression "e" and wraps a resolved AutoGeneratedExpression
   /// around it.
   /// </summary>
-  public static AutoGeneratedExpression Create(Expression e, IToken token = null) {
+  public static AutoGeneratedExpression Create(Expression e, IOrigin token = null) {
     Contract.Requires(e != null);
     var a = new AutoGeneratedExpression(token ?? e.tok, e);
     a.type = e.Type;

Source/DafnyCore/AST/Expressions/Collections/DisplayExpression.cs

@@ -14,7 +14,7 @@ protected DisplayExpression(Cloner cloner, DisplayExpression original) : base(cl
     Elements = original.Elements.ConvertAll(cloner.CloneExpr);
   }
 
-  public DisplayExpression(IToken tok, List<Expression> elements)
+  public DisplayExpression(IOrigin tok, List<Expression> elements)
     : base(tok) {
     Contract.Requires(cce.NonNullElements(elements));
     Elements = elements;