Merge branch 'master' into support-enforce-determinism-with-standard-…

…libraries

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

@@ -65,7 +65,7 @@ public override IEnumerable<Expression> TerminalExpressions {
   public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     var lineThen = 0;
     var colThen = 0;
-    IOrigin thenToken = null;
+    Token thenToken = null;
     foreach (var token in OwnedTokens) {
       switch (token.val) {
         case "if": {

Source/DafnyCore/AST/Grammar/IndentationFormatter.cs

@@ -229,7 +229,7 @@ public string GetNewTrivia(Token token, bool trailingTrivia) {
     });
   }
 
-  private string ReIndentMultilineComment(IOrigin token, string capturedComment, int currentIndent,
+  private string ReIndentMultilineComment(Token token, string capturedComment, int currentIndent,
     string indentationBefore, bool precededByNewline, out bool previousMatchWasSingleLineCommentToAlign) {
     var doubleStar = capturedComment.StartsWith("/**") && !capturedComment.StartsWith("/***");
 

Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs

@@ -485,7 +485,7 @@ bool IsGenericInstantiation(bool inExpressionContext) {
   // Indeed 'name' could be the last expression of an ensures clause, and the attribute
   // could belong to the next method declaration otherwise.
   bool IsAtCall() {
-    IOrigin pt = la;
+    Token pt = la;
     if (pt.val != "@") {
       return false;
     }

Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs

@@ -122,7 +122,7 @@ protected override bool VisitOneStmt(Statement stmt, ref int unusedIndent) {
     }
 
     // Best heuristic for new elements is to indent them using the method's formatting
-    SetMethodLikeIndent(stmt.Origin, stmt.OwnedTokens, indentBefore);
+    SetMethodLikeIndent(stmt.StartToken, stmt.OwnedTokens, indentBefore);
     SetIndentations(stmt.EndToken, -1, -1, indentBefore);
 
     return true;
@@ -141,23 +141,23 @@ public static bool FirstTokenOnLineIs(Token token, Func<Token, bool> predicate)
   // Given a token, finds the indentation that was expected before it.
   // Used for frame expressions to initially copy the indentation of "reads", "requires", etc.
 
-  public int GetIndentAbove(IOrigin token) {
+  public int GetIndentAbove(Token token) {
     if (PosToIndentations(token.pos).Above is var aboveIndentation and not -1) {
       return aboveIndentation;
     }
 
     return GetIndentBelowOrInlineOrAbove(token.Prev);
   }
 
-  public int GetIndentInlineOrAbove(IOrigin token) {
+  public int GetIndentInlineOrAbove(Token token) {
     if (PosToIndentations(token.pos).Inline is var indentation and not -1) {
       return indentation;
     }
 
     return GetIndentAbove(token);
   }
 
-  public int GetIndentBelowOrInlineOrAbove(IOrigin token) {
+  public int GetIndentBelowOrInlineOrAbove(Token token) {
     if (token == null || token == Token.NoToken) {
       return 0;
     }
@@ -173,7 +173,7 @@ public int GetIndentBelowOrInlineOrAbove(IOrigin token) {
   // Get the precise column this token will be at after reformatting.
   // Requires all tokens before to have been formatted.
 
-  public int GetNewTokenVisualIndent(IOrigin token, int defaultIndent) {
+  public int GetNewTokenVisualIndent(Token token, int defaultIndent) {
     var previousTrivia = token.Prev != null ? token.Prev.TrailingTrivia : "";
     previousTrivia += token.LeadingTrivia;
     var lastNL = previousTrivia.LastIndexOf('\n');
@@ -206,7 +206,7 @@ public int GetNewTokenVisualIndent(IOrigin token, int defaultIndent) {
     return token.col - 1;
   }
 
-  private static int GetTrailingSpace(IOrigin token) {
+  private static int GetTrailingSpace(Token token) {
     var c = 0;
     while (c < token.TrailingTrivia.Length && token.TrailingTrivia[c] == ' ') {
       c++;
@@ -217,15 +217,15 @@ private static int GetTrailingSpace(IOrigin token) {
 
   // Given a token such as `var ` immediately followed by another token
   // returns the indent so that everything after it is aligned with the first token.
-  public int GetRightAlignIndentAfter(IOrigin token, int indentFallback) {
+  public int GetRightAlignIndentAfter(Token token, int indentFallback) {
     var trailingSpace = GetTrailingSpace(token);
     return GetNewTokenVisualIndent(token, indentFallback) + token.val.Length + trailingSpace;
   }
 
   private static readonly Regex FollowedByNewlineRegex = new Regex("^[ \t]*([\r\n]|//)");
   private readonly Uri fileToFormat;
 
-  public static bool IsFollowedByNewline(IOrigin token) {
+  public static bool IsFollowedByNewline(Token token) {
     return FollowedByNewlineRegex.IsMatch(token.TrailingTrivia);
   }
 
@@ -253,7 +253,7 @@ public void SetIndentations(IOrigin token, int above = -1, int inline = -1, int
 
   // functions, methods, predicates, iterators, can all be formatted using this method.
   // See FormatterWorksForMethodsInModule in Formatter.cs to see how methods are formatted.
-  public void SetMethodLikeIndent(IOrigin startToken, IEnumerable<IOrigin> ownedTokens, int indent) {
+  public void SetMethodLikeIndent(Token startToken, IEnumerable<Token> ownedTokens, int indent) {
     var indent2 = indent + SpaceTab;
     if (startToken.val != "{") {
       SetIndentations(startToken, indent, indent, indent2);
@@ -322,7 +322,7 @@ public void SetMethodLikeIndent(IOrigin startToken, IEnumerable<IOrigin> ownedTo
     }
   }
 
-  public void SetTypeLikeIndentation(int indent, IEnumerable<IOrigin> tokens) {
+  public void SetTypeLikeIndentation(int indent, IEnumerable<Token> tokens) {
     var commaIndent = indent + SpaceTab;
     var rightIndent = indent + SpaceTab;
     foreach (var token in tokens) {
@@ -579,7 +579,7 @@ public void SetIndentBody(Statement body, int indent) {
     Visit(body, indent);
   }
 
-  public bool SetIndentPrintRevealStmt(int indent, IEnumerable<IOrigin> ownedTokens) {
+  public bool SetIndentPrintRevealStmt(int indent, IEnumerable<Token> ownedTokens) {
     var commaIndent = indent + SpaceTab;
     var innerIndent = indent + SpaceTab;
     var afterSemicolonIndent = indent;
@@ -724,7 +724,7 @@ public void VisitAlternatives(List<GuardedAlternative> alternatives, int indent)
     }
   }
 
-  public bool SetIndentParensExpression(int indent, IEnumerable<IOrigin> ownedTokens) {
+  public bool SetIndentParensExpression(int indent, IEnumerable<Token> ownedTokens) {
     var itemIndent = indent + SpaceTab;
     var commaIndent = indent;
 
@@ -763,14 +763,14 @@ public bool SetIndentParensExpression(int indent, IEnumerable<IOrigin> ownedToke
     return true;
   }
 
-  public bool SetIndentCases(int indent, IEnumerable<IOrigin> ownedTokens, Action indentInside) {
+  public bool SetIndentCases(int indent, IEnumerable<Token> ownedTokens, Action indentInside) {
     var caseIndent = indent;
     var afterArrowIndent = indent + SpaceTab;
     var decreasesElemIndent = indent + SpaceTab + SpaceTab;
     var commaIndent = decreasesElemIndent;
     // Need to ensure that the "case" is at least left aligned with the match/if/while keyword
     IOrigin decisionToken = null;
-    var allTokens = ownedTokens as IOrigin[] ?? ownedTokens.ToArray();
+    var allTokens = ownedTokens as Token[] ?? ownedTokens.ToArray();
     foreach (var token in allTokens) {
       if (SetIndentLabelTokens(token, indent)) {
         continue;
@@ -856,7 +856,7 @@ public bool SetIndentCases(int indent, IEnumerable<IOrigin> ownedTokens, Action
     return false;
   }
 
-  public bool SetIndentVarDeclStmt(int indent, IEnumerable<IOrigin> ownedTokens, bool noLHS, bool isLetExpr) {
+  public bool SetIndentVarDeclStmt(int indent, IEnumerable<Token> ownedTokens, bool noLHS, bool isLetExpr) {
     var rightIndent = indent + SpaceTab;
     var commaIndent = indent + SpaceTab;
     var afterSemicolonIndent = indent;
@@ -926,7 +926,7 @@ public bool SetIndentVarDeclStmt(int indent, IEnumerable<IOrigin> ownedTokens, b
     return true;
   }
 
-  public bool SetIndentLabelTokens(IOrigin token, int indent) {
+  public bool SetIndentLabelTokens(Token token, int indent) {
     if (token.val == "label") {
       SetOpeningIndentedRegion(token, indent);
     } else if (token.val == ":" && token.Prev.Prev.val == "label") {
@@ -938,7 +938,7 @@ public bool SetIndentLabelTokens(IOrigin token, int indent) {
     return true;
   }
 
-  public void SetIndentLikeLoop(IEnumerable<IOrigin> ownedTokens, Statement body, int indent) {
+  public void SetIndentLikeLoop(IEnumerable<Token> ownedTokens, Statement body, int indent) {
     var decreasesElemIndent = indent + SpaceTab;
     var commaIndent = indent + SpaceTab;
     var first = true;
@@ -1120,7 +1120,7 @@ public void SetKeywordWithoutSurroundingIndentation(IOrigin token, int indent) {
   ///                ^rightIndent
   ///           ^commaIndent
   /// 
-  public void SetAlign(int indent, IOrigin token, out int rightIndent, out int commaIndent) {
+  public void SetAlign(int indent, Token token, out int rightIndent, out int commaIndent) {
     SetIndentations(token, indent, indent);
     rightIndent = GetRightAlignIndentAfter(token, indent);
     commaIndent = GetNewTokenVisualIndent(token, indent) + token.val.Length - 1;
@@ -1136,7 +1136,7 @@ public void SetAlign(int indent, IOrigin token, out int rightIndent, out int com
   ///        ^ rightIndent
   /// else Z
   /// 
-  public void SetAlignOpen(IOrigin token, int indent) {
+  public void SetAlignOpen(Token token, int indent) {
     var rightIndent = GetRightAlignIndentAfter(token, indent);
     SetIndentations(token, indent, indent, rightIndent);
   }

Source/DafnyCore/AST/IOrigin.cs

@@ -3,7 +3,7 @@
 
 namespace Microsoft.Dafny;
 
-public interface IOrigin : Microsoft.Boogie.IToken {
+public interface IOrigin : Boogie.IToken {
 
   bool IsInherited(ModuleDefinition m);
 
@@ -18,6 +18,7 @@ public interface IOrigin : Microsoft.Boogie.IToken {
   int line { get; set; }
   string val { get; set; }
   bool IsValid { get; }*/
+
   string Boogie.IToken.filename {
     get => Uri == null ? null : Path.GetFileName(Uri.LocalPath);
     set => throw new NotSupportedException();
@@ -34,27 +35,5 @@ Token Center {
     get;
   }
 
-  /// <summary>
-  /// TrailingTrivia contains everything after the token,
-  /// until and including two newlines between which there is no commment
-  /// All the remaining trivia is for the LeadingTrivia of the next token
-  ///
-  /// ```
-  /// const /*for const*/ x /*for x*/ := /* for := */ 1/* for 1 */
-  /// // for 1 again
-  /// // for 1 again
-  ///
-  /// // Two newlines, now all the trivia is for var y
-  /// // this line as well.
-  /// var y := 2
-  /// ```
-  /// </summary>
-  string TrailingTrivia { get; set; }
-  string LeadingTrivia { get; set; }
-  Token Next { get; set; } // The next token
-  Token Prev { get; set; } // The previous token
-
-  public IOrigin WithVal(string val);  // create a new token by setting the given val.
-
   bool IsCopy { get; }
 }

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -102,7 +102,7 @@ public bool InferredDecreases {
   public bool AllowsAllocation => CwInner.AllowsAllocation;
 
   public bool SingleFileToken => CwInner.SingleFileToken;
-  public IEnumerable<IOrigin> OwnedTokens => CwInner.OwnedTokens;
+  public IEnumerable<Token> OwnedTokens => CwInner.OwnedTokens;
   public IOrigin Origin => CwInner.Origin;
   public IOrigin NavigationToken => CwInner.NavigationToken;
   public SymbolKind? Kind => CwInner.Kind;

Source/DafnyCore/AST/Members/Method.cs

@@ -387,7 +387,7 @@ public override void Resolve(ModuleResolver resolver) {
       return triviaFound;
     }
 
-    IOrigin? lastClosingParenthesis = null;
+    Token? lastClosingParenthesis = null;
     foreach (var token in OwnedTokens) {
       if (token.val == ")") {
         lastClosingParenthesis = token;

Source/DafnyCore/AST/Modules/ExportSignature.cs

@@ -28,23 +28,20 @@ public ExportSignature(IOrigin prefixTok, string prefix, IOrigin idOrigin, strin
     ClassId = prefix;
     Id = id;
     Opaque = opaque;
-    OwnedTokensCache = new List<IOrigin>() { Origin, prefixTok };
   }
 
   public ExportSignature(IOrigin idOrigin, string id, bool opaque) : base(idOrigin) {
     Contract.Requires(idOrigin != null);
     Contract.Requires(id != null);
     Id = id;
     Opaque = opaque;
-    OwnedTokensCache = new List<IOrigin>() { Origin };
   }
 
   public ExportSignature(Cloner cloner, ExportSignature original) : base(cloner, original) {
     Id = original.Id;
     Opaque = original.Opaque;
     ClassId = original.ClassId;
     ClassIdTok = cloner.Origin(original.ClassIdTok);
-    OwnedTokensCache = new List<IOrigin>() { Origin };
   }
 
   public override string ToString() {

Source/DafnyCore/AST/OriginWrapper.cs

@@ -11,7 +11,6 @@ protected OriginWrapper(IOrigin wrappedToken) {
     WrappedToken = wrappedToken;
   }
 
-  public abstract IOrigin WithVal(string newVal);
   public virtual bool IsCopy => WrappedToken.IsCopy;
 
   public virtual int col {
@@ -58,22 +57,6 @@ public virtual string val {
     get { return WrappedToken.val; }
     set { WrappedToken.val = value; }
   }
-  public virtual string LeadingTrivia {
-    get { return WrappedToken.LeadingTrivia; }
-    set { throw new NotSupportedException(); }
-  }
-  public virtual string TrailingTrivia {
-    get { return WrappedToken.TrailingTrivia; }
-    set { throw new NotSupportedException(); }
-  }
-  public virtual Token Next {
-    get { return WrappedToken.Next; }
-    set { throw new NotSupportedException(); }
-  }
-  public virtual Token Prev {
-    get { return WrappedToken.Prev; }
-    set { throw new NotSupportedException(); }
-  }
 
   public int CompareTo(IOrigin other) {
     return WrappedToken.CompareTo(other);

Source/DafnyCore/AST/Statements/Methods/CallStmt.cs

@@ -4,73 +4,6 @@
 
 namespace Microsoft.Dafny;
 
-/// <summary>
-/// This class temporarily exists to retain old behavior
-/// When it comes to where errors are reported.
-///
-/// For function calls, the following location is used to report precondition failures:
-/// 
-/// someFunction(x, y);
-/// ^           ^
-/// old     future
-///
-/// For assertions, when the condition does not hold
-/// assert P(x)
-/// ^       ^
-/// future  old
-/// </summary>
-class OverrideCenter : OriginWrapper {
-  public OverrideCenter(IOrigin wrappedToken, Token newCenter) : base(wrappedToken) {
-    this.Center = newCenter;
-  }
-
-  public override Token Center { get; }
-
-  public override IOrigin WithVal(string newVal) {
-    throw new System.NotImplementedException();
-  }
-
-  public override int col {
-    get => Center.col;
-    set => throw new System.NotImplementedException();
-  }
-
-  public override int line {
-    get => Center.line;
-    set => throw new System.NotImplementedException();
-  }
-
-  public override int pos {
-    get => Center.pos;
-    set => throw new System.NotImplementedException();
-  }
-
-  public override string val {
-    get => Center.val;
-    set => throw new System.NotImplementedException();
-  }
-
-  public override string LeadingTrivia {
-    get => Center.LeadingTrivia;
-    set => throw new System.NotImplementedException();
-  }
-
-  public override string TrailingTrivia {
-    get => Center.TrailingTrivia;
-    set => throw new System.NotImplementedException();
-  }
-
-  public override Token Next {
-    get => Center.Next;
-    set => throw new System.NotImplementedException();
-  }
-
-  public override Token Prev {
-    get => Center.Prev;
-    set => throw new System.NotImplementedException();
-  }
-}
-
 /// <summary>
 /// A CallStmt is always resolved.  It is typically produced as a resolved counterpart of the syntactic AST note ApplySuffix.
 /// </summary>