Introduce code generator name

Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs

@@ -6,12 +6,12 @@
 public class BenchmarkingCompilerInstrumenter : CompilerInstrumenter {
   public BenchmarkingCompilerInstrumenter(ErrorReporter reporter) : base(reporter) { }
 
-  public override void Instrument(IExecutableBackend backend, SinglePassCompiler compiler, Program program) {
-    if (compiler is JavaCompiler javaCompiler) {
+  public override void Instrument(IExecutableBackend backend, SinglePassCodeGenerator codeGenerator, Program program) {
+    if (codeGenerator is JavaCodeGenerator javaCompiler) {
       javaCompiler.AddInstrumenter(new JavaBenchmarkCompilationInstrumenter(Reporter));
     } else {
       Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, program.GetStartOfFirstFileToken(),
-        $"The benchmarking plugin does not support this compilation target: {compiler} (--target:{backend.TargetId})");
+        $"The benchmarking plugin does not support this compilation target: {codeGenerator} (--target:{backend.TargetId})");
     }
   }
 }

Source/DafnyCore/AST/Members/Method.cs

@@ -192,7 +192,7 @@ public bool AllowsNontermination {
 
   public override string GetCompileName(DafnyOptions options) {
     var nm = base.GetCompileName(options);
-    if (nm == Dafny.Compilers.SinglePassCompiler.DefaultNameMain && IsStatic && !IsEntryPoint) {
+    if (nm == Dafny.Compilers.SinglePassCodeGenerator.DefaultNameMain && IsStatic && !IsEntryPoint) {
       // for a static method that is named "Main" but is not a legal "Main" method,
       // change its name.
       nm = EnclosingClass.Name + "_" + nm;

Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs → Source/DafnyCore/Backends/CSharp/CsharpBackend.cs

@@ -12,8 +12,8 @@ namespace Microsoft.Dafny.Compilers;
 
 public class CsharpBackend : ExecutableBackend {
 
-  protected override SinglePassCompiler CreateCompiler() {
-    return new CsharpCompiler(Options, Reporter);
+  protected override SinglePassCodeGenerator CreateCodeGenerator() {
+    return new CsharpCodeGenerator(Options, Reporter);
   }
 
   public override IReadOnlySet<string> SupportedExtensions => new HashSet<string> { ".cs", ".dll" };
@@ -160,7 +160,7 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
   }
 
   public override void PopulateCoverageReport(CoverageReport coverageReport) {
-    compiler.Coverage.PopulateCoverageReport(coverageReport);
+    codeGenerator.Coverage.PopulateCoverageReport(coverageReport);
   }
 
   public CsharpBackend(DafnyOptions options) : base(options) {

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs → Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -19,7 +19,7 @@
 using static Microsoft.Dafny.ConcreteSyntaxTreeUtils;
 
 namespace Microsoft.Dafny.Compilers {
-  public class CsharpCompiler : SinglePassCompiler {
+  public class CsharpCodeGenerator : SinglePassCodeGenerator {
     protected bool Synthesize = false;
 
     public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
@@ -29,7 +29,7 @@ public class CsharpCompiler : SinglePassCompiler {
       Feature.ArrowsWithMoreThan16Arguments
     };
 
-    public CsharpCompiler(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
+    public CsharpCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
     }
 
     const string DafnyISet = "Dafny.ISet";
@@ -1377,25 +1377,25 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name,
     }
 
     protected class ClassWriter : IClassWriter {
-      public readonly CsharpCompiler Compiler;
+      public readonly CsharpCodeGenerator CodeGenerator;
       public readonly ConcreteSyntaxTree InstanceMemberWriter;
       public readonly ConcreteSyntaxTree StaticMemberWriter;
       public readonly ConcreteSyntaxTree CtorBodyWriter;
       private readonly CsharpSynthesizer csharpSynthesizer;
 
-      public ClassWriter(CsharpCompiler compiler, ConcreteSyntaxTree instanceMemberWriter, ConcreteSyntaxTree/*?*/ ctorBodyWriter, ConcreteSyntaxTree/*?*/ staticMemberWriter = null) {
-        Contract.Requires(compiler != null);
+      public ClassWriter(CsharpCodeGenerator codeGenerator, ConcreteSyntaxTree instanceMemberWriter, ConcreteSyntaxTree/*?*/ ctorBodyWriter, ConcreteSyntaxTree/*?*/ staticMemberWriter = null) {
+        Contract.Requires(codeGenerator != null);
         Contract.Requires(instanceMemberWriter != null);
-        this.Compiler = compiler;
+        this.CodeGenerator = codeGenerator;
         this.InstanceMemberWriter = instanceMemberWriter;
         this.CtorBodyWriter = ctorBodyWriter;
         this.StaticMemberWriter = staticMemberWriter ?? instanceMemberWriter;
-        this.csharpSynthesizer = new CsharpSynthesizer(Compiler, ErrorWriter());
+        this.csharpSynthesizer = new CsharpSynthesizer(CodeGenerator, ErrorWriter());
       }
 
       public ConcreteSyntaxTree Writer(bool isStatic, bool createBody, MemberDecl/*?*/ member) {
         if (createBody) {
-          if (isStatic || (member?.EnclosingClass is TraitDecl && Compiler.NeedsCustomReceiver(member))) {
+          if (isStatic || (member?.EnclosingClass is TraitDecl && CodeGenerator.NeedsCustomReceiver(member))) {
             return StaticMemberWriter;
           }
         }
@@ -1404,7 +1404,7 @@ public ConcreteSyntaxTree Writer(bool isStatic, bool createBody, MemberDecl/*?*/
       }
 
       public ConcreteSyntaxTree /*?*/ CreateMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) {
-        return Compiler.CreateMethod(m, typeArgs, createBody, Writer(m.IsStatic, createBody, m), forBodyInheritance, lookasideBody);
+        return CodeGenerator.CreateMethod(m, typeArgs, createBody, Writer(m.IsStatic, createBody, m), forBodyInheritance, lookasideBody);
       }
 
       public ConcreteSyntaxTree SynthesizeMethod(Method method, List<TypeArgumentInstantiation> typeArgs, bool createBody, bool forBodyInheritance,
@@ -1413,20 +1413,20 @@ public ConcreteSyntaxTree SynthesizeMethod(Method method, List<TypeArgumentInsta
       }
 
       public ConcreteSyntaxTree /*?*/ CreateFunction(string name, List<TypeArgumentInstantiation> typeArgs, List<Formal> formals, Type resultType, IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) {
-        return Compiler.CreateFunction(name, typeArgs, formals, resultType, tok, isStatic, createBody, member, Writer(isStatic, createBody, member), forBodyInheritance, lookasideBody);
+        return CodeGenerator.CreateFunction(name, typeArgs, formals, resultType, tok, isStatic, createBody, member, Writer(isStatic, createBody, member), forBodyInheritance, lookasideBody);
       }
 
       public ConcreteSyntaxTree /*?*/ CreateGetter(string name, TopLevelDecl enclosingDecl, Type resultType, IToken tok, bool isStatic, bool isConst, bool createBody, MemberDecl /*?*/ member, bool forBodyInheritance) {
-        return Compiler.CreateGetter(name, resultType, tok, isStatic, createBody, Writer(isStatic, createBody, member));
+        return CodeGenerator.CreateGetter(name, resultType, tok, isStatic, createBody, Writer(isStatic, createBody, member));
       }
 
       public ConcreteSyntaxTree /*?*/ CreateGetterSetter(string name, Type resultType, IToken tok, bool createBody, MemberDecl /*?*/ member, out ConcreteSyntaxTree setterWriter, bool forBodyInheritance) {
-        return Compiler.CreateGetterSetter(name, resultType, tok, createBody, out setterWriter, Writer(false, createBody, member));
+        return CodeGenerator.CreateGetterSetter(name, resultType, tok, createBody, out setterWriter, Writer(false, createBody, member));
       }
 
       public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, bool isConst, Type type, IToken tok, string rhs, Field field) {
-        var typeName = Compiler.TypeName(type, this.StaticMemberWriter, tok);
-        Compiler.DeclareField(name, true, isStatic, isConst, typeName, rhs, this);
+        var typeName = CodeGenerator.TypeName(type, this.StaticMemberWriter, tok);
+        CodeGenerator.DeclareField(name, true, isStatic, isConst, typeName, rhs, this);
       }
 
       public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) {

Source/DafnyCore/Compilers/CSharp/Synthesizer-Csharp.cs → Source/DafnyCore/Backends/CSharp/CsharpSynthesizer.cs

@@ -28,17 +28,17 @@ namespace Microsoft.Dafny.Compilers;
 /// </summary>
 public class CsharpSynthesizer {
 
-  private readonly CsharpCompiler compiler;
+  private readonly CsharpCodeGenerator codeGenerator;
   private readonly ConcreteSyntaxTree ErrorWriter;
   // maps identifiers to the names of the corresponding mock:
   private Dictionary<IVariable, string> objectToMockName = new();
   // associates a bound variable with the lambda passed to argument matcher
   private Dictionary<IVariable, string> bounds = new();
   private Method lastSynthesizedMethod = null;
-  private DafnyOptions Options => compiler.Options;
+  private DafnyOptions Options => codeGenerator.Options;
 
-  public CsharpSynthesizer(CsharpCompiler compiler, ConcreteSyntaxTree errorWriter) {
-    this.compiler = compiler;
+  public CsharpSynthesizer(CsharpCodeGenerator codeGenerator, ConcreteSyntaxTree errorWriter) {
+    this.codeGenerator = codeGenerator;
     ErrorWriter = errorWriter;
   }
 
@@ -69,19 +69,19 @@ public CsharpSynthesizer(CsharpCompiler compiler, ConcreteSyntaxTree errorWriter
   /// }
   /// </summary>
   public ConcreteSyntaxTree SynthesizeMethod(Method method,
-    List<SinglePassCompiler.TypeArgumentInstantiation> typeArgs, bool createBody,
+    List<SinglePassCodeGenerator.TypeArgumentInstantiation> typeArgs, bool createBody,
     ConcreteSyntaxTree wr, bool forBodyInheritance, bool lookasideBody) {
 
     lastSynthesizedMethod = method;
     // The following few lines are identical to those in Compiler.CreateMethod:
     var customReceiver = createBody &&
                          !forBodyInheritance &&
-                         compiler.NeedsCustomReceiver(method);
-    var keywords = compiler.Keywords(true, true);
-    var returnType = compiler.GetTargetReturnTypeReplacement(method, wr);
-    var typeParameters = compiler.TypeParameters(SinglePassCompiler.TypeArgumentInstantiation.
-      ToFormals(compiler.ForTypeParameters(typeArgs, method, lookasideBody)));
-    var parameters = compiler
+                         codeGenerator.NeedsCustomReceiver(method);
+    var keywords = codeGenerator.Keywords(true, true);
+    var returnType = codeGenerator.GetTargetReturnTypeReplacement(method, wr);
+    var typeParameters = codeGenerator.TypeParameters(SinglePassCodeGenerator.TypeArgumentInstantiation.
+      ToFormals(codeGenerator.ForTypeParameters(typeArgs, method, lookasideBody)));
+    var parameters = codeGenerator
       .GetMethodParameters(method, typeArgs, lookasideBody, customReceiver, returnType);
 
     // Out parameters cannot be used inside lambda expressions in Csharp
@@ -90,19 +90,19 @@ public ConcreteSyntaxTree SynthesizeMethod(Method method,
     // The solution is to rename the out parameters.
     var parameterString = parameters.ToString();
     var objectToReturnName = method.Outs.ToDictionary(o => o,
-      o => compiler.idGenerator.FreshId(o.CompileName + "Return"));
+      o => codeGenerator.idGenerator.FreshId(o.CompileName + "Return"));
     foreach (var (obj, returnName) in objectToReturnName) {
       parameterString = Regex.Replace(parameterString,
         $"(^|[^a-zA-Z0-9_]){obj.CompileName}([^a-zA-Z0-9_]|$)",
         "$1" + returnName + "$2");
     }
-    wr.FormatLine($"{keywords}{returnType} {compiler.PublicIdProtect(method.GetCompileName(Options))}{typeParameters}({parameterString}) {{");
+    wr.FormatLine($"{keywords}{returnType} {codeGenerator.PublicIdProtect(method.GetCompileName(Options))}{typeParameters}({parameterString}) {{");
 
     // Initialize the mocks
     objectToMockName = method.Outs.ToDictionary(o => (IVariable)o,
-      o => compiler.idGenerator.FreshId(o.CompileName + "Mock"));
+      o => codeGenerator.idGenerator.FreshId(o.CompileName + "Mock"));
     foreach (var (obj, mockName) in objectToMockName) {
-      var typeName = compiler.TypeName(obj.Type, wr, obj.Tok);
+      var typeName = codeGenerator.TypeName(obj.Type, wr, obj.Tok);
       // Mocking a trait works only so long as no trait member is accessed
       if ((method.Outs.First().Type is UserDefinedType userDefinedType) &&
           userDefinedType.IsTraitType) {
@@ -151,7 +151,7 @@ private Tuple<IVariable, string> GetBound(Expression exp) {
   private void SynthesizeExpression(ConcreteSyntaxTree wr, Expression expr, ConcreteSyntaxTree wStmts) {
     switch (expr) {
       case LiteralExpr literalExpr:
-        wr.Append(compiler.Expr(literalExpr, false, wStmts));
+        wr.Append(codeGenerator.Expr(literalExpr, false, wStmts));
         break;
       case ApplySuffix applySuffix:
         SynthesizeExpression(wr, applySuffix, wStmts);
@@ -179,15 +179,15 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, ApplySuffix applySuffix
     var methodName = method.GetCompileName(Options);
 
     if (((Function)method).Ens.Count != 0) {
-      compiler.Reporter.Warning(MessageSource.Compiler,
-        CompilerErrors.ErrorId.c_possibly_unsatisfied_postconditions, lastSynthesizedMethod.tok,
+      codeGenerator.Reporter.Warning(MessageSource.Compiler,
+          GeneratorErrors.ErrorId.c_possibly_unsatisfied_postconditions, lastSynthesizedMethod.tok,
         "Post-conditions on function {0} might " +
         "be unsatisfied when synthesizing code " +
         "for method {1}",
         methodName, lastSynthesizedMethod.Name);
     }
 
-    var tmpId = compiler.idGenerator.FreshId("tmp");
+    var tmpId = codeGenerator.idGenerator.FreshId("tmp");
     wr.Format($"{objectToMockName[receiver]}.Setup({tmpId} => {tmpId}.{methodName}(");
 
     // The remaining part of the method uses Moq's argument matching to
@@ -199,7 +199,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, ApplySuffix applySuffix
       if (bound != null) { // if true, arg is a bound variable
         wr.Write(bound.Item2);
       } else {
-        wr.Append(compiler.Expr(arg, false, wStmts));
+        wr.Append(codeGenerator.Expr(arg, false, wStmts));
       }
       if (i != applySuffix.Args.Count - 1) {
         wr.Write(", ");
@@ -224,13 +224,13 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, BinaryExpr binaryExpr,
       var obj = ((IdentifierExpr)exprDotName.Lhs.Resolved).Var;
       var field = ((MemberSelectExpr)exprDotName.Resolved).Member;
       var fieldName = field.GetCompileName(Options);
-      compiler.Reporter.Warning(MessageSource.Compiler,
-        CompilerErrors.ErrorId.c_stubbing_fields_not_recommended, lastSynthesizedMethod.tok,
+      codeGenerator.Reporter.Warning(MessageSource.Compiler,
+        GeneratorErrors.ErrorId.c_stubbing_fields_not_recommended, lastSynthesizedMethod.tok,
         "Stubbing fields is not recommended (field {0} of object {1} inside method {2})",
         fieldName, obj.Name, lastSynthesizedMethod.Name);
-      var tmpId = compiler.idGenerator.FreshId("tmp");
+      var tmpId = codeGenerator.idGenerator.FreshId("tmp");
       wr.Format($"{objectToMockName[obj]}.SetupGet({tmpId} => {tmpId}.@{fieldName}).Returns( ");
-      wr.Append(compiler.Expr(binaryExpr.E1, false, wStmts));
+      wr.Append(codeGenerator.Expr(binaryExpr.E1, false, wStmts));
       wr.WriteLine(");");
       return;
     }
@@ -242,7 +242,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, BinaryExpr binaryExpr,
     wr.Write("(");
     for (int i = 0; i < applySuffix.Args.Count; i++) {
       var arg = applySuffix.Args[i];
-      var typeName = compiler.TypeName(arg.Type, wr, arg.tok);
+      var typeName = codeGenerator.TypeName(arg.Type, wr, arg.tok);
       var bound = GetBound(arg);
       if (bound != null) {
         wr.Format($"{typeName} {bound.Item1.CompileName}");
@@ -256,7 +256,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, BinaryExpr binaryExpr,
       }
     }
     wr.Write(")=>");
-    wr.Append(compiler.Expr(binaryExpr.E1, false, wStmts));
+    wr.Append(codeGenerator.Expr(binaryExpr.E1, false, wStmts));
     wr.WriteLine(");");
   }
 
@@ -268,12 +268,12 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, ForallExpr forallExpr,
 
     // a MultiMatcher is created to convert an antecedent of the implication
     // following the forall statement to argument matching calls in Moq
-    var matcherName = compiler.idGenerator.FreshId("matcher");
+    var matcherName = codeGenerator.idGenerator.FreshId("matcher");
 
-    var tmpId = compiler.idGenerator.FreshId("tmp");
+    var tmpId = codeGenerator.idGenerator.FreshId("tmp");
     for (int i = 0; i < forallExpr.BoundVars.Count; i++) {
       var boundVar = forallExpr.BoundVars[i];
-      var varType = compiler.TypeName(boundVar.Type, wr, boundVar.tok);
+      var varType = codeGenerator.TypeName(boundVar.Type, wr, boundVar.tok);
       bounds[boundVar] = $"It.Is<{varType}>(x => {matcherName}.Match(x))";
       declarations.Add($"var {boundVar.CompileName} = ({varType}) {tmpId}[{i}];");
     }
@@ -286,7 +286,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, ForallExpr forallExpr,
     switch (binaryExpr.Op) {
       case BinaryExpr.Opcode.Imp:
         wr.Write("\treturn ");
-        wr.Append(compiler.Expr(binaryExpr.E0, false, wStmts));
+        wr.Append(codeGenerator.Expr(binaryExpr.E0, false, wStmts));
         wr.WriteLine(";");
         binaryExpr = (BinaryExpr)binaryExpr.E1.Resolved;
         break;