Merge branch 'master' into non-reference-traits

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

@@ -22,7 +22,7 @@ public ThisExpr(MemberDecl m)
     Contract.Requires(m.tok != null);
     Contract.Requires(m.EnclosingClass != null);
     Contract.Requires(!m.IsStatic);
-    Type = Resolver.GetReceiverType(m.tok, m);
+    Type = ModuleResolver.GetReceiverType(m.tok, m);
   }
 
   /// <summary>
@@ -34,7 +34,7 @@ public ThisExpr(TopLevelDeclWithMembers cl)
     : base(cl.tok) {
     Contract.Requires(cl != null);
     Contract.Requires(cl.tok != null);
-    Type = Resolver.GetThisType(cl.tok, cl);
+    Type = ModuleResolver.GetThisType(cl.tok, cl);
   }
 
   public ThisExpr Clone(Cloner cloner) {

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

@@ -12,7 +12,7 @@ public NestedMatchCase(IToken tok, ExtendedPattern pat) {
     this.Pat = pat;
   }
 
-  public void CheckLinearNestedMatchCase(Type type, ResolutionContext resolutionContext, Resolver resolver) {
+  public void CheckLinearNestedMatchCase(Type type, ResolutionContext resolutionContext, ModuleResolver resolver) {
     Pat.CheckLinearExtendedPattern(type, resolutionContext, resolver);
   }
 }

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

@@ -21,7 +21,7 @@ public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Att
 
   public override IEnumerable<Node> PreResolveChildren => Children;
 
-  public void Resolve(Resolver resolver,
+  public void Resolve(ModuleResolver resolver,
     ResolutionContext resolutionContext,
     Type resultType,
     Type sourceType) {

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

@@ -33,7 +33,7 @@ public NestedMatchCaseStmt Clone(Cloner cloner) {
   public override IEnumerable<Node> PreResolveChildren => Children;
 
   public void Resolve(
-    Resolver resolver,
+    ModuleResolver resolver,
     ResolutionContext resolutionContext,
     Dictionary<TypeParameter, Type> subst,
     Type sourceType) {

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

@@ -52,7 +52,7 @@ public override IEnumerable<Expression> SubExpressions {
 
   public override IEnumerable<Node> Children => new[] { Source }.Concat<Node>(Cases);
 
-  public void Resolve(Resolver resolver, ResolutionContext resolutionContext) {
+  public void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext) {
 
     resolver.ResolveExpression(Source, resolutionContext);
 

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

@@ -78,7 +78,7 @@ public NestedMatchStmt(RangeToken rangeToken, Expression source, [Captured] List
   /// 2 - desugaring it into a decision tree of MatchStmt and IfStmt (for constant matching)
   /// 3 - resolving the generated (sub)statement.
   /// </summary>
-  public override void Resolve(Resolver resolver, ResolutionContext resolutionContext) {
+  public override void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext) {
     resolver.ResolveExpression(Source, resolutionContext);
 
     if (Source.Type is TypeProxy) {
@@ -111,7 +111,7 @@ public override void Resolve(Resolver resolver, ResolutionContext resolutionCont
     }
   }
 
-  public void CheckLinearNestedMatchStmt(Type dtd, ResolutionContext resolutionContext, Resolver resolver) {
+  public void CheckLinearNestedMatchStmt(Type dtd, ResolutionContext resolutionContext, ModuleResolver resolver) {
     foreach (NestedMatchCaseStmt mc in this.Cases) {
       resolver.scope.PushMarker();
       resolver.ResolveAttributes(mc, resolutionContext);

Source/DafnyCore/AST/Expressions/Conditional/Patterns/DisjunctivePattern.cs

@@ -24,7 +24,7 @@ public override IEnumerable<Expression> SubExpressions {
     }
   }
 
-  public override void Resolve(Resolver resolver, ResolutionContext resolutionContext,
+  public override void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext,
     Type sourceType, bool isGhost, bool inStatementContext,
     bool inPattern, bool inDisjunctivePattern) {
 

Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs

@@ -29,7 +29,7 @@ public virtual IEnumerable<Expression> SubExpressions {
     }
   }
 
-  public abstract void Resolve(Resolver resolver, ResolutionContext resolutionContext,
+  public abstract void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext,
     Type sourceType, bool isGhost, bool inStatementContext,
     bool inPattern, bool inDisjunctivePattern);
 
@@ -44,7 +44,7 @@ public abstract void Resolve(Resolver resolver, ResolutionContext resolutionCont
   *  3 - An IdPattern at datatype type representing a constructor of type
   *  4 - An IdPattern at datatype type with no arguments representing a bound variable
   */
-  public void CheckLinearExtendedPattern(Type type, ResolutionContext resolutionContext, Resolver resolver) {
+  public void CheckLinearExtendedPattern(Type type, ResolutionContext resolutionContext, ModuleResolver resolver) {
     if (type == null) {
       return;
     }

Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs

@@ -86,7 +86,7 @@ public override IEnumerable<Expression> SubExpressions {
     }
   }
 
-  public override void Resolve(Resolver resolver, ResolutionContext resolutionContext,
+  public override void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext,
     Type sourceType, bool isGhost, bool inStatementContext,
     bool inPattern, bool inDisjunctivePattern) {
 
@@ -136,7 +136,7 @@ public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
 
   public IToken NameToken => Tok;
 
-  public void CheckLinearVarPattern(Type type, ResolutionContext resolutionContext, Resolver resolver) {
+  public void CheckLinearVarPattern(Type type, ResolutionContext resolutionContext, ModuleResolver resolver) {
     if (Arguments != null) {
       if (Id == SystemModuleManager.TupleTypeCtorName(1)) {
         resolver.reporter.Error(MessageSource.Resolver, this.Tok, "parentheses are not allowed around a pattern");

Source/DafnyCore/AST/Expressions/Conditional/Patterns/LitPattern.cs

@@ -74,7 +74,7 @@ public override IEnumerable<Expression> SubExpressions {
     }
   }
 
-  public override void Resolve(Resolver resolver,
+  public override void Resolve(ModuleResolver resolver,
     ResolutionContext resolutionContext,
     Type sourceType, bool isGhost, bool inStatementContext,
     bool inPattern, bool inDisjunctivePattern) {

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -727,9 +727,9 @@ public static Expression WrapResolvedCall(FunctionCallExpr call, SystemModuleMan
     // Wrap the resolved call in the usual unresolved structure, in case the expression is cloned and re-resolved.
     var receiverType = (UserDefinedType)call.Receiver.Type.NormalizeExpand();
     var subst = TypeParameter.SubstitutionMap(receiverType.ResolvedClass.TypeArgs, receiverType.TypeArgs);
-    subst = Resolver.AddParentTypeParameterSubstitutions(subst, receiverType);
+    subst = ModuleResolver.AddParentTypeParameterSubstitutions(subst, receiverType);
     var exprDotName = new ExprDotName(call.tok, call.Receiver, call.Function.Name, call.TypeApplication_JustFunction) {
-      Type = Resolver.SelectAppropriateArrowTypeForFunction(call.Function, subst, systemModuleManager)
+      Type = ModuleResolver.SelectAppropriateArrowTypeForFunction(call.Function, subst, systemModuleManager)
     };
 
     subst = TypeParameter.SubstitutionMap(call.Function.TypeArgs, call.TypeApplication_JustFunction);

Source/DafnyCore/AST/Members/Function.cs

@@ -359,7 +359,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
   /// <summary>
   /// Assumes type parameters have already been pushed
   /// </summary>
-  public void Resolve(Resolver resolver) {
+  public void Resolve(ModuleResolver resolver) {
     Contract.Requires(this != null);
     Contract.Requires(resolver.AllTypeConstraints.Count == 0);
     Contract.Ensures(resolver.AllTypeConstraints.Count == 0);

Source/DafnyCore/AST/Members/Method.cs

@@ -219,7 +219,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
   /// <summary>
   /// Assumes type parameters have already been pushed
   /// </summary>
-  public void Resolve(Resolver resolver) {
+  public void Resolve(ModuleResolver resolver) {
     Contract.Requires(this != null);
     Contract.Requires(resolver.AllTypeConstraints.Count == 0);
     Contract.Ensures(resolver.AllTypeConstraints.Count == 0);

Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs

@@ -90,7 +90,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     return true;
   }
 
-  public ModuleSignature Resolve(Resolver resolver, CompilationData compilation) {
+  public ModuleSignature Resolve(ModuleResolver resolver, CompilationData compilation) {
     // The declaration is a literal module, so it has members and such that we need
     // to resolve. First we do refinement transformation. Then we construct the signature
     // of the module. This is the public, externally visible signature. Then we add in

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -380,7 +380,7 @@ public ModuleDefinition Clone(Cloner cloner) {
   /// resolved, a caller has to check for both a change in error count and a "false"
   /// return value.
   /// </summary>
-  public bool Resolve(ModuleSignature sig, Resolver resolver, bool isAnExport = false) {
+  public bool Resolve(ModuleSignature sig, ModuleResolver resolver, bool isAnExport = false) {
     Contract.Requires(resolver.AllTypeConstraints.Count == 0);
     Contract.Ensures(resolver.AllTypeConstraints.Count == 0);
 
@@ -421,9 +421,9 @@ public bool Resolve(ModuleSignature sig, Resolver resolver, bool isAnExport = fa
     }
 
     var oldModuleInfo = resolver.moduleInfo;
-    resolver.moduleInfo = Resolver.MergeSignature(sig, resolver.ProgramResolver.SystemModuleManager.systemNameInfo);
+    resolver.moduleInfo = ModuleResolver.MergeSignature(sig, resolver.ProgramResolver.SystemModuleManager.systemNameInfo);
     Type.PushScope(resolver.moduleInfo.VisibilityScope);
-    Resolver.ResolveOpenedImports(resolver.moduleInfo, this, resolver.Reporter, resolver); // opened imports do not persist
+    ModuleResolver.ResolveOpenedImports(resolver.moduleInfo, this, resolver.Reporter, resolver); // opened imports do not persist
     var datatypeDependencies = new Graph<IndDatatypeDecl>();
     var codatatypeDependencies = new Graph<CoDatatypeDecl>();
     var allDeclarations = AllDeclarationsAndNonNullTypeDecls(TopLevelDecls).ToList();
@@ -541,7 +541,7 @@ private static PrefixNameModule ShortenPrefix(PrefixNameModule prefixNameModule)
     return prefixNameModule with { Parts = rest };
   }
 
-  public ModuleSignature RegisterTopLevelDecls(Resolver resolver, bool useImports) {
+  public ModuleSignature RegisterTopLevelDecls(ModuleResolver resolver, bool useImports) {
     Contract.Requires(this != null);
     var sig = new ModuleSignature();
     sig.ModuleDef = this;

Source/DafnyCore/AST/Modules/ScopeCloner.cs

@@ -54,7 +54,7 @@ public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Modul
         vismap.Add(def, new VisibilityScope());
       }
 
-      sigmap[def] = Resolver.MergeSignature(sigmap[def], import.Signature);
+      sigmap[def] = ModuleResolver.MergeSignature(sigmap[def], import.Signature);
       sigmap[def].ModuleDef = def;
       declmap[def].Add((AliasModuleDecl)top);
       if (VisibleInScope(import)) {

Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs

@@ -110,7 +110,7 @@ public override IEnumerable<Expression> PreResolveSubExpressions {
   /// and saves the result into s.ResolvedStatements.
   /// This is also known as the "elephant operator"
   /// </summary>
-  public override void Resolve(Resolver resolver, ResolutionContext resolutionContext) {
+  public override void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext) {
     base.Resolve(resolver, resolutionContext);
     // TODO Do I have any responsibilities regarding the use of resolutionContext? Is it mutable?
 
@@ -246,7 +246,7 @@ public override void Resolve(Resolver resolver, ResolutionContext resolutionCont
   /// <param name="resolver"></param>
   /// <param name="enclosingMethod"></param>
   private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract, Type firstType,
-    Resolver resolver, Method enclosingMethod) {
+    ModuleResolver resolver, Method enclosingMethod) {
 
     var temp = resolver.FreshTempVarName("valueOrError", enclosingMethod);
     var lhss = new List<LocalVariable>() { new LocalVariable(RangeToken, temp, new InferredTypeProxy(), false) };

Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs

@@ -73,7 +73,7 @@ public override IEnumerable<Expression> NonSpecificationSubExpressions {
     }
   }
 
-  public override void Resolve(Resolver resolver, ResolutionContext resolutionContext) {
+  public override void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext) {
     Contract.Requires(this != null);
     Contract.Requires(resolutionContext != null);
 

Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs

@@ -27,7 +27,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     return formatter.SetIndentUpdateStmt(this, indentBefore, false);
   }
 
-  public override void Resolve(Resolver resolver, ResolutionContext context) {
+  public override void Resolve(ModuleResolver resolver, ResolutionContext context) {
     foreach (var lhs in Lhss) {
       var ec = resolver.Reporter.Count(ErrorLevel.Error);
       resolver.ResolveExpression(lhs, context);

Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs

@@ -81,7 +81,7 @@ public override IEnumerable<Expression> PreResolveSubExpressions {
   /// errorCountBeforeCheckingLhs is passed in so that this method can determined if any resolution errors were found during
   /// LHS or RHS checking, because only if no errors were found is update.ResolvedStmt changed.
   /// </summary>
-  public override void Resolve(Resolver resolver, ResolutionContext resolutionContext) {
+  public override void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext) {
     Contract.Requires(this != null);
     Contract.Requires(resolutionContext != null);
 
@@ -90,7 +90,7 @@ public override void Resolve(Resolver resolver, ResolutionContext resolutionCont
     base.Resolve(resolver, resolutionContext);
 
     IToken firstEffectfulRhs = null;
-    Resolver.MethodCallInformation methodCallInfo = null;
+    ModuleResolver.MethodCallInformation methodCallInfo = null;
     ResolvedStatements = new();
     foreach (var rhs in Rhss) {
       bool isEffectful;

Source/DafnyCore/AST/Statements/Statement.cs

@@ -28,7 +28,7 @@ void ObjectInvariant() {
 
   [FilledInDuringResolution] public bool IsGhost { get; set; }
 
-  public virtual void Resolve(Resolver resolver, ResolutionContext resolutionContext) {
+  public virtual void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext) {
     resolver.ResolveAttributes(this, resolutionContext);
   }
 

Source/DafnyCore/AST/SystemModuleManager.cs

@@ -464,7 +464,7 @@ public ValuetypeDecl AsValuetypeDecl(Type t) {
   }
 
   public void ResolveValueTypeDecls(ProgramResolver programResolver) {
-    var moduleResolver = new Resolver(programResolver);
+    var moduleResolver = new ModuleResolver(programResolver);
     moduleResolver.moduleInfo = systemNameInfo;
     foreach (var valueTypeDecl in valuetypeDecls) {
       foreach (var member in valueTypeDecl.Members) {

Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs

@@ -186,7 +186,7 @@ public override bool SetIndent(int indentBefore, TokenNewIndentCollector formatt
   /// <summary>
   /// Assumes the specification of the iterator itself has been successfully resolved.
   /// </summary>
-  public void CreateIteratorMethodSpecs(Resolver resolver) {
+  public void CreateIteratorMethodSpecs(ModuleResolver resolver) {
     Contract.Requires(this != null);
 
     var tok = new AutoGeneratedToken(Tok);
@@ -319,7 +319,7 @@ public void CreateIteratorMethodSpecs(Resolver resolver) {
     Member_MoveNext.Decreases.Attributes = Decreases.Attributes;
   }
 
-  public void Resolve(Resolver resolver) {
+  public void Resolve(ModuleResolver resolver) {
     // register the names of the implicit members
     var members = new Dictionary<string, MemberDecl>();
     resolver.AddClassMembers(this, members);

Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs

@@ -173,7 +173,7 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
     return Members.SelectMany(m => m.Assumptions(this));
   }
 
-  public void RegisterMembers(Resolver resolver, Dictionary<string, MemberDecl> members) {
+  public void RegisterMembers(ModuleResolver resolver, Dictionary<string, MemberDecl> members) {
     Contract.Requires(this != null);
     Contract.Requires(members != null);
 
@@ -248,7 +248,7 @@ public void RegisterMembers(Resolver resolver, Dictionary<string, MemberDecl> me
           extraMember.InheritVisibility(m, false);
           members.Add(extraName.Value, extraMember);
         } else if (m is Function f && f.ByMethodBody != null) {
-          Resolver.RegisterByMethod(f, this);
+          ModuleResolver.RegisterByMethod(f, this);
         }
       } else if (m is Constructor && !((Constructor)m).HasName) {
         resolver.reporter.Error(MessageSource.Resolver, m, "More than one anonymous constructor");

Source/DafnyCore/AST/Types/Types.cs

@@ -1891,7 +1891,7 @@ public BitvectorType(DafnyOptions options, int width)
     : base() {
     Contract.Requires(0 <= width);
     Width = width;
-    foreach (var nativeType in Resolver.NativeTypes) {
+    foreach (var nativeType in ModuleResolver.NativeTypes) {
       if (options.Backend.SupportedNativeTypes.Contains(nativeType.Name) && width <= nativeType.Bitwidth) {
         NativeType = nativeType;
         break;
@@ -2533,7 +2533,7 @@ public override string TypeName(DafnyOptions options, ModuleDefinition context,
       // Unfortunately, ResolveClass may be null, so Name is all we have.  Reverse-engineer the string name.
       IEnumerable<bool> argumentGhostness = SystemModuleManager.ArgumentGhostnessFromString(Name, TypeArgs.Count);
       return "(" + Util.Comma(System.Linq.Enumerable.Zip(TypeArgs, argumentGhostness),
-        (ty_u) => Resolver.GhostPrefix(ty_u.Item2) + ty_u.Item1.TypeName(options, context, parseAble)) + ")";
+        (ty_u) => ModuleResolver.GhostPrefix(ty_u.Item2) + ty_u.Item1.TypeName(options, context, parseAble)) + ")";
     } else if (ArrowType.IsPartialArrowTypeName(Name)) {
       return ArrowType.PrettyArrowTypeName(options, ArrowType.PARTIAL_ARROW, TypeArgs, null, context, parseAble);
     } else if (ArrowType.IsTotalArrowTypeName(Name)) {

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -3544,7 +3544,7 @@ protected ConcreteSyntaxTree CompileGuardedLoops(List<BoundVar> bvs, List<Compre
       ConcreteSyntaxTree guardWriter = new ConcreteSyntaxTree();
       var wStmts = guardWriter.Fork();
       wr = EmitIf(out guardWriter, false, wr);
-      foreach (var bvConstraints in bvs.Select(bv => Resolver.GetImpliedTypeConstraint(bv, bv.Type))) {
+      foreach (var bvConstraints in bvs.Select(bv => ModuleResolver.GetImpliedTypeConstraint(bv, bv.Type))) {
         TrParenExpr(bvConstraints, guardWriter, false, wStmts);
         guardWriter.Write($" {Conj} ");
       }

Source/DafnyCore/DafnyOptions.cs

@@ -41,7 +41,7 @@ public class DafnyOptions : Bpl.CommandLineOptions {
 
     public IList<Uri> CliRootSourceUris = new List<Uri>();
 
-    public ProjectFile ProjectFile { get; set; }
+    public DafnyProject DafnyProject { get; set; }
     public Command CurrentCommand { get; set; }
 
 

Source/DafnyCore/DooFile.cs

@@ -137,7 +137,7 @@ public bool Validate(string filePath, DafnyOptions options, Command currentComma
 
       object libraryValue = null;
       if (Manifest.Options.TryGetValue(option.Name, out var manifestValue)) {
-        if (!ProjectFile.TryGetValueFromToml(Console.Out, null,
+        if (!DafnyProject.TryGetValueFromToml(Console.Out, null,
               option.Name, option.ValueType, manifestValue, out libraryValue)) {
           return false;
         }