Pure parse function

Source/DafnyCore.Test/DooFileTest.cs

@@ -31,9 +31,8 @@ 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 }, false);
     Microsoft.Dafny.Type.ResetScopes();
-    var errorReporter = new ConsoleErrorReporter(options, outerModule);
+    var errorReporter = new ConsoleErrorReporter(options);
     var program = ParseUtils.Parse(dafnyProgramText, rootUri, errorReporter);
     Assert.Equal(0, errorReporter.ErrorCount);
     return program;

Source/DafnyCore/AST/BuiltIns.cs

@@ -67,32 +67,42 @@ public static Attributes AxiomAttribute() {
   public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) {
     Contract.Requires(1 <= dims);
     Contract.Requires(arg != null);
-    return ArrayType(Token.NoToken, dims, new List<Type>() { arg }, allowCreationOfNewClass);
+    var (result, mod) = ArrayType(Token.NoToken, dims, new List<Type> { arg }, allowCreationOfNewClass);
+    mod(this);
+    return result;
   }
-  public UserDefinedType ArrayType(IToken tok, int dims, List<Type> optTypeArgs, bool allowCreationOfNewClass, bool useClassNameType = false) {
+
+  public static (UserDefinedType type, Action<BuiltIns> ModifyBuiltins) ArrayType(IToken tok, int dims, List<Type> optTypeArgs, bool allowCreationOfNewClass, bool useClassNameType = false) {
     Contract.Requires(tok != null);
     Contract.Requires(1 <= dims);
     Contract.Requires(optTypeArgs == null || optTypeArgs.Count > 0);  // ideally, it is 1, but more will generate an error later, and null means it will be filled in automatically
     Contract.Ensures(Contract.Result<UserDefinedType>() != null);
 
     var arrayName = ArrayClassName(dims);
     if (useClassNameType) {
-      arrayName = arrayName + "?";
+      arrayName += "?";
     }
-    if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {
-      ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule, DontCompile());
+
+    void ModifyBuiltins(BuiltIns builtIns) {
+      if (!allowCreationOfNewClass || builtIns.arrayTypeDecls.ContainsKey(dims)) {
+        return;
+      }
+
+      ArrayClassDecl arrayClass = new ArrayClassDecl(dims, builtIns.SystemModule, builtIns.DontCompile());
       for (int d = 0; d < dims; d++) {
         string name = dims == 1 ? "Length" : "Length" + d;
         Field len = new SpecialField(RangeToken.NoToken, name, SpecialField.ID.ArrayLength, dims == 1 ? null : (object)d, false, false, false, Type.Int, null);
-        len.EnclosingClass = arrayClass;  // resolve here
+        len.EnclosingClass = arrayClass; // resolve here
         arrayClass.Members.Add(len);
       }
-      arrayTypeDecls.Add(dims, arrayClass);
-      SystemModule.SourceDecls.Add(arrayClass);
-      CreateArrowTypeDecl(dims);  // also create an arrow type with this arity, since it may be used in an initializing expression for the array
+
+      builtIns.arrayTypeDecls.Add(dims, arrayClass);
+      builtIns.SystemModule.SourceDecls.Add(arrayClass);
+      builtIns.CreateArrowTypeDecl(dims); // also create an arrow type with this arity, since it may be used in an initializing expression for the array
     }
-    UserDefinedType udt = new UserDefinedType(tok, arrayName, optTypeArgs);
-    return udt;
+
+    var udt = new UserDefinedType(tok, arrayName, optTypeArgs);
+    return (udt, ModifyBuiltins);
   }
 
   public static string ArrayClassName(int dims) {

Source/DafnyCore/AST/DafnyAst.cs

@@ -110,7 +110,7 @@ public string Name {
     /// Get the first token that is in the same file as the DefaultModule.RootToken.FileName
     /// (skips included tokens)
     public IToken GetFirstTopLevelToken() {
-      var rootToken = DefaultModule.RangeToken.StartToken;
+      var rootToken = DefaultModuleDef.RangeToken.StartToken;
       if (rootToken.Next == null) {
         return null;
       }
@@ -137,32 +137,6 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
     }
   }
 
-  public class Include : TokenNode, IComparable {
-    public Uri IncluderFilename { get; }
-    public Uri IncludedFilename { get; }
-    public string CanonicalPath { get; }
-    public bool ErrorReported;
-
-    public Include(IToken tok, Uri includer, Uri theFilename) {
-      this.tok = tok;
-      this.IncluderFilename = includer;
-      this.IncludedFilename = theFilename;
-      this.CanonicalPath = DafnyFile.Canonicalize(theFilename.LocalPath).LocalPath;
-      this.ErrorReported = false;
-    }
-
-    public int CompareTo(object obj) {
-      if (obj is Include include) {
-        return CanonicalPath.CompareTo(include.CanonicalPath);
-      } else {
-        throw new NotImplementedException();
-      }
-    }
-
-    public override IEnumerable<Node> Children => Enumerable.Empty<Node>();
-    public override IEnumerable<Node> PreResolveChildren => Enumerable.Empty<Node>();
-  }
-
   /// <summary>
   /// An expression introducting bound variables
   /// </summary>