Revert "Remove IncludeToken as prep for caching parsing (#3858)" (#3981)

This reverts commit eb45d23.

Author: fabiomadge

Source/DafnyCore.Test/DooFileTest.cs

@@ -29,14 +29,12 @@ public void UnknownManifestEntries() {
   }
 
   private static Program ParseProgram(string dafnyProgramText, DafnyOptions options) {
-    const string fullFilePath = "untitled:foo";
-    var rootUri = new Uri(fullFilePath);
-    var outerModule = new DefaultModuleDefinition(new List<Uri> { rootUri });
-    var module = new LiteralModuleDecl(outerModule, null);
+    var module = new LiteralModuleDecl(new DefaultModuleDefinition(), null);
+    const string fullFilePath = "foo";
     Microsoft.Dafny.Type.ResetScopes();
     var builtIns = new BuiltIns(options);
-    var errorReporter = new ConsoleErrorReporter(options, outerModule);
-    var parseResult = Parser.Parse(dafnyProgramText, rootUri, module, builtIns, errorReporter);
+    var errorReporter = new ConsoleErrorReporter(options);
+    var parseResult = Parser.Parse(dafnyProgramText, fullFilePath, "foo", module, builtIns, errorReporter);
     Assert.Equal(0, parseResult);
     return new Program(fullFilePath, module, builtIns, errorReporter);
   }

Source/DafnyCore/AST/Cloner.cs

@@ -31,8 +31,8 @@ public Cloner(bool cloneResolvedFields = false) {
 
     public virtual ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) {
       ModuleDefinition nw;
-      if (m is DefaultModuleDefinition defaultModuleDefinition) {
-        nw = new DefaultModuleDefinition(defaultModuleDefinition.RootUris);
+      if (m is DefaultModuleDefinition) {
+        nw = new DefaultModuleDefinition();
       } else {
         nw = new ModuleDefinition(Range(m.RangeToken), name, m.PrefixIds, m.IsAbstract, m.IsFacade,
           m.RefinementQId, m.EnclosingModule, CloneAttributes(m.Attributes),

Source/DafnyCore/AST/DafnyAst.cs

@@ -39,8 +39,6 @@ void ObjectInvariant() {
       Contract.Invariant(DefaultModule != null);
     }
 
-    public List<Include> Includes => DefaultModuleDef.Includes;
-
     public readonly string FullName;
     [FilledInDuringResolution] public Dictionary<ModuleDefinition, ModuleSignature> ModuleSigs;
     // Resolution essentially flattens the module hierarchy, for
@@ -50,7 +48,7 @@ void ObjectInvariant() {
 
     public Method MainMethod; // Method to be used as main if compiled
     public readonly LiteralModuleDecl DefaultModule;
-    public readonly DefaultModuleDefinition DefaultModuleDef;
+    public readonly ModuleDefinition DefaultModuleDef;
     public readonly BuiltIns BuiltIns;
     public DafnyOptions Options => Reporter.Options;
     public ErrorReporter Reporter { get; set; }
@@ -102,7 +100,7 @@ public IToken GetFirstTopLevelToken() {
 
       var firstToken = DefaultModule.RootToken.Next;
       // We skip all included files
-      while (firstToken is { Next: { } } && firstToken.Next.Filepath != DefaultModule.RootToken.Filepath) {
+      while (firstToken is { Next: { } } && firstToken.Next.Filename != DefaultModule.RootToken.Filename) {
         firstToken = firstToken.Next;
       }
 
@@ -123,13 +121,13 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
   }
 
   public class Include : TokenNode, IComparable {
-    public Uri IncluderFilename { get; }
+    public string IncluderFilename { get; }
     public string IncludedFilename { get; }
     public string CanonicalPath { get; }
     public bool CompileIncludedCode { get; }
     public bool ErrorReported;
 
-    public Include(IToken tok, Uri includer, string theFilename, bool compileIncludedCode) {
+    public Include(IToken tok, string includer, string theFilename, bool compileIncludedCode) {
       this.tok = tok;
       this.IncluderFilename = includer;
       this.IncludedFilename = theFilename;

Source/DafnyCore/AST/Expressions/LitPattern.cs

@@ -43,7 +43,7 @@ public LiteralExpr OptimisticallyDesugaredLit {
           } else {
             var n = (BigInteger)lit.Value;
             var tok = new Token(neg.tok.line, neg.tok.col) {
-              Uri = neg.tok.Uri,
+              Filename = neg.tok.Filename,
               val = "-0"
             };
             optimisticallyDesugaredLit = new LiteralExpr(tok, -n);

Source/DafnyCore/AST/Grammar/IndentationFormatter.cs

@@ -1,5 +1,4 @@
-using System;
-using System.Collections.Concurrent;
+using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.Linq;
 using System.Text.RegularExpressions;
@@ -24,7 +23,7 @@ public IndentationFormatter(TokenNewIndentCollector formatter) {
   /// by immediately processing all nodes and assigning indentations to most structural tokens 
   /// </summary>
   public static IndentationFormatter ForProgram(Program program, bool reduceBlockiness = true) {
-    var tokenNewIndentCollector = new TokenNewIndentCollector(program) {
+    var tokenNewIndentCollector = new TokenNewIndentCollector {
       ReduceBlockiness = reduceBlockiness
     };
     foreach (var child in program.DefaultModuleDef.PreResolveChildren) {

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -972,9 +972,9 @@ private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes,
       return false;
     }
 
-    private bool PrintModeSkipGeneral(IToken tok, string fileBeingPrinted) {
+    private bool PrintModeSkipGeneral(Bpl.IToken tok, string fileBeingPrinted) {
       return (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhost)
-             && tok.Uri != null && fileBeingPrinted != null && tok.Uri.LocalPath != fileBeingPrinted;
+             && tok.filename != null && fileBeingPrinted != null && Path.GetFullPath(tok.filename) != fileBeingPrinted;
     }
 
     public void PrintMethod(Method method, int indent, bool printSignatureOnly) {

Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs

@@ -50,8 +50,6 @@ namespace Microsoft.Dafny;
  * ```
  */
 public class TokenNewIndentCollector : TopDownVisitor<int> {
-  private readonly Program program;
-
   /* If true, the indentation will be
    * var name := method(
    *   x,
@@ -83,8 +81,8 @@ private Indentations PosToIndentations(int pos) {
   public int binOpIndent = -1;
   public int binOpArgIndent = -1;
 
-  internal TokenNewIndentCollector(Program program) {
-    this.program = program;
+
+  internal TokenNewIndentCollector() {
     preResolve = true;
   }
 
@@ -231,7 +229,7 @@ public static bool IsFollowedByNewline(IToken token) {
   // 'inline' is the hypothetical indentation of this token if it was on its own line
   // 'below' is the hypothetical indentation of a comment after that token, and of the next token if it does not have a set indentation
   public void SetIndentations(IToken token, int above = -1, int inline = -1, int below = -1) {
-    if (token.WasIncluded(program) || (token.line == 0 && token.col == 0)) {
+    if (token is IncludeToken || (token.line == 0 && token.col == 0)) {
       // Just ignore this token.
       return;
     }
@@ -401,7 +399,7 @@ public void SetStatementIndentation(Statement statement) {
   }
 
   public void SetDeclIndentation(TopLevelDecl topLevelDecl, int indent) {
-    if (topLevelDecl.tok.WasIncluded(program)) {
+    if (topLevelDecl.tok is IncludeToken) {
       return;
     }
 
@@ -422,7 +420,7 @@ public void SetDeclIndentation(TopLevelDecl topLevelDecl, int indent) {
 
       var initialMemberIndent = declWithMembers.tok.line == 0 ? indent : indent2;
       foreach (var member in declWithMembers.PreResolveChildren) {
-        if (member.Tok.WasIncluded(program)) {
+        if (member.Tok is IncludeToken) {
           continue;
         }
 

Source/DafnyCore/AST/IncludeHandler.cs

@@ -2,7 +2,6 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
-using System.IO;
 using System.Text;
 
 namespace Microsoft.Dafny;
@@ -18,14 +17,12 @@ public interface IToken : Microsoft.Boogie.IToken {
   string val { get; set; }
   bool IsValid { get; }*/
   string Boogie.IToken.filename {
-    get => Uri == null ? null : Path.GetFileName(Uri.LocalPath);
-    set => throw new NotSupportedException();
+    get => Filename;
+    set => Filename = value;
   }
 
-  public string ActualFilename => Uri.LocalPath;
-  string Filepath => Uri.LocalPath;
-
-  Uri Uri { get; set; }
+  public string ActualFilename { get; }
+  string Filename { get; set; }
 
   /// <summary>
   /// TrailingTrivia contains everything after the token,
@@ -73,9 +70,8 @@ public Token(int linenum, int colnum) {
 
   public int kind { get; set; } // Used by coco, so we can't rename it to Kind
 
-  public string ActualFilename => Filepath;
-  public string Filepath => Uri?.LocalPath;
-  public Uri Uri { get; set; }
+  public string ActualFilename => Filename;
+  public string Filename { get; set; }
 
   public int pos { get; set; } // Used by coco, so we can't rename it to Pos
 
@@ -108,7 +104,7 @@ public IToken WithVal(string newVal) {
       line = line,
       Prev = Prev,
       Next = Next,
-      Uri = Uri,
+      Filename = Filename,
       kind = kind,
       val = newVal
     };
@@ -119,7 +115,7 @@ public override int GetHashCode() {
   }
 
   public override string ToString() {
-    return $"'{val}': {Path.GetFileName(Filepath)}@{pos} - @{line}:{col}";
+    return $"{Filename}@{pos} - @{line}:{col}";
   }
 }
 
@@ -140,11 +136,9 @@ public virtual int col {
 
   public string ActualFilename => WrappedToken.ActualFilename;
 
-  public virtual string Filepath => WrappedToken.Filepath;
-
-  public Uri Uri {
-    get => WrappedToken.Uri;
-    set => WrappedToken.Uri = value;
+  public virtual string Filename {
+    get { return WrappedToken.Filename; }
+    set { WrappedToken.filename = value; }
   }
 
   public bool IsValid {
@@ -186,32 +180,6 @@ public virtual IToken Prev {
 }
 
 public static class TokenExtensions {
-
-  public static string TokenToString(this Boogie.IToken tok, DafnyOptions options) {
-    if (tok is IToken dafnyToken) {
-      return dafnyToken.TokenToString(options);
-    }
-
-    return $"{tok.filename}({tok.line},{tok.col - 1})";
-  }
-
-  public static string TokenToString(this IToken tok, DafnyOptions options) {
-    if (tok.Uri == null) {
-      return $"({tok.line},{tok.col - 1})";
-    }
-
-    var currentDirectory = Directory.GetCurrentDirectory();
-    string filename = tok.Uri.Scheme switch {
-      "stdin" => "<stdin>",
-      "transcript" => Path.GetFileName(tok.Filepath),
-      _ => options.UseBaseNameForFileName
-        ? Path.GetFileName(tok.Filepath)
-        : (tok.Filepath.StartsWith(currentDirectory) ? Path.GetRelativePath(currentDirectory, tok.Filepath) : tok.Filepath)
-    };
-
-    return $"{filename}({tok.line},{tok.col - 1})";
-  }
-
   public static RangeToken ToRange(this IToken token) {
     if (token is BoogieRangeToken boogieRangeToken) {
       return new RangeToken(boogieRangeToken.StartToken, boogieRangeToken.EndToken);
@@ -333,6 +301,54 @@ public override IToken WithVal(string newVal) {
   }
 }
 
+/// <summary>
+/// An IncludeToken is a wrapper that indicates that the function/method was
+/// declared in a file that was included. Any proof obligations from such an
+/// included file are to be ignored.
+/// </summary>
+public class IncludeToken : TokenWrapper {
+  public Include Include;
+  public IncludeToken(Include include, IToken wrappedToken)
+    : base(wrappedToken) {
+    Contract.Requires(wrappedToken != null);
+    this.Include = include;
+  }
+
+  public override string val {
+    get { return WrappedToken.val; }
+    set { WrappedToken.val = value; }
+  }
+
+  public override int pos {
+    get { return WrappedToken.pos; }
+    set { WrappedToken.pos = value; }
+  }
+
+  public override int line {
+    get { return WrappedToken.line; }
+    set { WrappedToken.line = value; }
+  }
+
+  public override int col {
+    get { return WrappedToken.col; }
+    set { WrappedToken.col = value; }
+  }
+
+  public override IToken Prev {
+    get { return WrappedToken.Prev; }
+    set { WrappedToken.Prev = value; }
+  }
+
+  public override IToken Next {
+    get { return WrappedToken.Next; }
+    set { WrappedToken.Next = value; }
+  }
+
+  public override IToken WithVal(string newVal) {
+    return new IncludeToken(Include, WrappedToken.WithVal(newVal));
+  }
+}
+
 /// <summary>
 /// A token wrapper used to produce better type checking errors
 /// for quantified variables. See QuantifierVar.ExtractSingleRange()

Source/DafnyCore/AST/Tokens.cs

@@ -1159,14 +1159,14 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
 }
 
 public class DefaultModuleDefinition : ModuleDefinition {
-
-  public IList<Uri> RootUris { get; }
-  public DefaultModuleDefinition(IList<Uri> rootUris)
+  public DefaultModuleDefinition()
     : base(RangeToken.NoToken, new Name("_module"), new List<IToken>(), false, false, null, null, null, true, true, true) {
-    RootUris = rootUris;
   }
-
-  public override bool IsDefaultModule => true;
+  public override bool IsDefaultModule {
+    get {
+      return true;
+    }
+  }
 }
 
 public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType {