Remove IncludeToken as prep for caching parsing (#3858)

Currently a file that's included is parsed differently. Its tokens are
wrapped in an `IncludeToken`, that includes a reference to the including
file.

To allow reusing parsed files in a cache, how the file is parsed should
be independent of what triggered it to be parsed. To achieve that, this
PR removes `IncludeToken`. To enable still determining whether a
particular token was part of an include or not, tokens now store a `Uri`
that uniquely identifies the document that token came from. The Uris of
the root documents are stored in `DefaultModuleDefinition`, which is
just below `Program`. Any token with a Uri that is not part of the root
set is considered to be included.

<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>

Author: keyboardDrummer

Source/DafnyCore.Test/DooFileTest.cs

@@ -29,12 +29,14 @@ public void UnknownManifestEntries() {
   }
 
   private static Program ParseProgram(string dafnyProgramText, DafnyOptions options) {
-    var module = new LiteralModuleDecl(new DefaultModuleDefinition(), null);
-    const string fullFilePath = "foo";
+    const string fullFilePath = "untitled:foo";
+    var rootUri = new Uri(fullFilePath);
+    var outerModule = new DefaultModuleDefinition(new List<Uri> { rootUri });
+    var module = new LiteralModuleDecl(outerModule, null);
     Microsoft.Dafny.Type.ResetScopes();
     var builtIns = new BuiltIns(options);
-    var errorReporter = new ConsoleErrorReporter(options);
-    var parseResult = Parser.Parse(dafnyProgramText, fullFilePath, "foo", module, builtIns, errorReporter);
+    var errorReporter = new ConsoleErrorReporter(options, outerModule);
+    var parseResult = Parser.Parse(dafnyProgramText, rootUri, 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) {
-        nw = new DefaultModuleDefinition();
+      if (m is DefaultModuleDefinition defaultModuleDefinition) {
+        nw = new DefaultModuleDefinition(defaultModuleDefinition.RootUris);
       } 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,6 +39,8 @@ 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
@@ -48,7 +50,7 @@ void ObjectInvariant() {
 
     public Method MainMethod; // Method to be used as main if compiled
     public readonly ModuleDecl DefaultModule;
-    public readonly ModuleDefinition DefaultModuleDef;
+    public readonly DefaultModuleDefinition DefaultModuleDef;
     public readonly BuiltIns BuiltIns;
     public DafnyOptions Options => Reporter.Options;
     public ErrorReporter Reporter { get; set; }
@@ -101,7 +103,7 @@ public IToken GetFirstTopLevelToken() {
 
       var firstToken = DefaultModule.RootToken.Next;
       // We skip all included files
-      while (firstToken is { Next: { } } && firstToken.Next.Filename != DefaultModule.RootToken.Filename) {
+      while (firstToken is { Next: { } } && firstToken.Next.Filepath != DefaultModule.RootToken.Filepath) {
         firstToken = firstToken.Next;
       }
 
@@ -122,13 +124,13 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
   }
 
   public class Include : TokenNode, IComparable {
-    public string IncluderFilename { get; }
+    public Uri IncluderFilename { get; }
     public string IncludedFilename { get; }
     public string CanonicalPath { get; }
     public bool CompileIncludedCode { get; }
     public bool ErrorReported;
 
-    public Include(IToken tok, string includer, string theFilename, bool compileIncludedCode) {
+    public Include(IToken tok, Uri 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) {
-              Filename = neg.tok.Filename,
+              Uri = neg.tok.Uri,
               val = "-0"
             };
             optimisticallyDesugaredLit = new LiteralExpr(tok, -n);

Source/DafnyCore/AST/Grammar/IndentationFormatter.cs

@@ -1,4 +1,5 @@
-using System.Collections.Concurrent;
+using System;
+using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.Linq;
 using System.Text.RegularExpressions;
@@ -23,7 +24,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 {
+    var tokenNewIndentCollector = new TokenNewIndentCollector(program) {
       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(Bpl.IToken tok, string fileBeingPrinted) {
+    private bool PrintModeSkipGeneral(IToken tok, string fileBeingPrinted) {
       return (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhost)
-             && tok.filename != null && fileBeingPrinted != null && Path.GetFullPath(tok.filename) != fileBeingPrinted;
+             && tok.Uri != null && fileBeingPrinted != null && tok.Uri.LocalPath != fileBeingPrinted;
     }
 
     public void PrintMethod(Method method, int indent, bool printSignatureOnly) {

Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs

@@ -50,6 +50,8 @@ namespace Microsoft.Dafny;
  * ```
  */
 public class TokenNewIndentCollector : TopDownVisitor<int> {
+  private readonly Program program;
+
   /* If true, the indentation will be
    * var name := method(
    *   x,
@@ -81,8 +83,8 @@ private Indentations PosToIndentations(int pos) {
   public int binOpIndent = -1;
   public int binOpArgIndent = -1;
 
-
-  internal TokenNewIndentCollector() {
+  internal TokenNewIndentCollector(Program program) {
+    this.program = program;
     preResolve = true;
   }
 
@@ -229,7 +231,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 is IncludeToken || (token.line == 0 && token.col == 0)) {
+    if (token.WasIncluded(program) || (token.line == 0 && token.col == 0)) {
       // Just ignore this token.
       return;
     }
@@ -399,7 +401,7 @@ public void SetStatementIndentation(Statement statement) {
   }
 
   public void SetDeclIndentation(TopLevelDecl topLevelDecl, int indent) {
-    if (topLevelDecl.tok is IncludeToken) {
+    if (topLevelDecl.tok.WasIncluded(program)) {
       return;
     }
 
@@ -420,7 +422,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 is IncludeToken) {
+        if (member.Tok.WasIncluded(program)) {
           continue;
         }
 

Source/DafnyCore/AST/IncludeHandler.cs

@@ -0,0 +1,28 @@
+using System;
+using System.IO;
+using System.Linq;
+
+namespace Microsoft.Dafny; 
+
+public static class IncludeHandler {
+  public static bool WasIncluded(this IToken token, DefaultModuleDefinition outerModule) {
+    if (token is RefinementToken) {
+      return false;
+    }
+
+    if (token == Token.NoToken) {
+      return false;
+    }
+
+    var files = outerModule.RootUris;
+    if (files.Contains(token.Uri)) {
+      return false;
+    }
+
+    return true;
+  }
+
+  public static bool WasIncluded(this IToken token, Program program) {
+    return token.WasIncluded(program.DefaultModuleDef);
+  }
+}

Source/DafnyCore/AST/Tokens.cs

@@ -2,6 +2,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.IO;
 using System.Text;
 
 namespace Microsoft.Dafny;
@@ -17,12 +18,14 @@ public interface IToken : Microsoft.Boogie.IToken {
   string val { get; set; }
   bool IsValid { get; }*/
   string Boogie.IToken.filename {
-    get => Filename;
-    set => Filename = value;
+    get => Uri == null ? null : Path.GetFileName(Uri.LocalPath);
+    set => throw new NotSupportedException();
   }
 
-  public string ActualFilename { get; }
-  string Filename { get; set; }
+  public string ActualFilename => Uri.LocalPath;
+  string Filepath => Uri.LocalPath;
+
+  Uri Uri { get; set; }
 
   /// <summary>
   /// TrailingTrivia contains everything after the token,
@@ -70,8 +73,9 @@ 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 => Filename;
-  public string Filename { get; set; }
+  public string ActualFilename => Filepath;
+  public string Filepath => Uri?.LocalPath;
+  public Uri Uri { get; set; }
 
   public int pos { get; set; } // Used by coco, so we can't rename it to Pos
 
@@ -104,7 +108,7 @@ public IToken WithVal(string newVal) {
       line = line,
       Prev = Prev,
       Next = Next,
-      Filename = Filename,
+      Uri = Uri,
       kind = kind,
       val = newVal
     };
@@ -115,7 +119,7 @@ public override int GetHashCode() {
   }
 
   public override string ToString() {
-    return $"{Filename}@{pos} - @{line}:{col}";
+    return $"'{val}': {Path.GetFileName(Filepath)}@{pos} - @{line}:{col}";
   }
 }
 
@@ -136,9 +140,11 @@ public virtual int col {
 
   public string ActualFilename => WrappedToken.ActualFilename;
 
-  public virtual string Filename {
-    get { return WrappedToken.Filename; }
-    set { WrappedToken.filename = value; }
+  public virtual string Filepath => WrappedToken.Filepath;
+
+  public Uri Uri {
+    get => WrappedToken.Uri;
+    set => WrappedToken.Uri = value;
   }
 
   public bool IsValid {
@@ -180,6 +186,32 @@ 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);
@@ -301,54 +333,6 @@ 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/TopLevelDeclarations.cs

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