Go lang call same module member

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -2045,7 +2045,8 @@ protected override void EmitHalt(IToken tok, Expression/*?*/ messageExpr, Concre
       wr.Format($"throw new Dafny.HaltException({exceptionMessage});");
     }
 
-    protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
+    protected override ConcreteSyntaxTree EmitForStmt(StatementGenerationContext context, IToken tok,
+      IVariable loopIndex, bool goingUp, string endVarName, /*?*/
       List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
 
       wr.Write($"for ({TypeName(loopIndex.Type, wr, tok)} {loopIndex.GetOrCreateCompileName(currentIdGenerator)} = ");
@@ -2062,7 +2063,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
         bodyWr.WriteLine($"{loopIndex.GetOrCreateCompileName(currentIdGenerator)}--;");
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
-      TrStmtList(body, bodyWr);
+      TrStmtList(context, body, bodyWr);
 
       return startWr;
     }
@@ -3498,12 +3499,12 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete
       Coverage.EmitTearDown(wBody);
     }
 
-    protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr) {
+    protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr, StatementGenerationContext context) {
       var tryBlock = wr.NewBlock("try");
-      TrStmt(body, tryBlock);
+      TrStmt(context, body, tryBlock);
       var catchBlock = wr.NewBlock("catch (Dafny.HaltException e)");
       catchBlock.WriteLine($"var {haltMessageVarName} = Dafny.Sequence<{CharTypeName}>.{CharMethodQualifier}FromString(e.Message);");
-      TrStmt(recoveryBody, catchBlock);
+      TrStmt(context, recoveryBody, catchBlock);
     }
 
     protected void EmitCoverageReportInstrumentation(Program program, ConcreteSyntaxTree wr) {

Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs

@@ -1324,7 +1324,8 @@ protected override void EmitHalt(IToken tok, Expression messageExpr, ConcreteSyn
       wr.WriteLine(");");
     }
 
-    protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
+    protected override ConcreteSyntaxTree EmitForStmt(StatementGenerationContext context, IToken tok,
+      IVariable loopIndex, bool goingUp, string endVarName, /*?*/
       List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
       throw new UnsupportedFeatureException(tok, Feature.ForLoops, "for loops have not yet been implemented");
     }
@@ -2468,7 +2469,8 @@ protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBod
       throw new UnsupportedFeatureException(Token.NoToken, Feature.ExactBoundedPool);
     }
 
-    protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr) {
+    protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody,
+      ConcreteSyntaxTree wr, StatementGenerationContext context) {
       throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
     }
   }

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -482,8 +482,9 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name,
       return params_;
     }
 
-    protected override void TrDividedBlockStmt(Constructor m, DividedBlockStmt dividedBlockStmt, ConcreteSyntaxTree writer) {
-      TrStmtList(dividedBlockStmt.BodyInit, writer);
+    protected override void TrDividedBlockStmt(Constructor m, DividedBlockStmt dividedBlockStmt,
+      ConcreteSyntaxTree writer, StatementGenerationContext context) {
+      TrStmtList(context, dividedBlockStmt.BodyInit, writer);
       if (writer is BuilderSyntaxTree<StatementContainer> builder) {
         var membersToInitialize = ((TopLevelDeclWithMembers)m.EnclosingClass).Members.Where((md =>
           md is Field and not ConstantField { Rhs: { } }));
@@ -506,7 +507,7 @@ protected override void TrDividedBlockStmt(Constructor m, DividedBlockStmt divid
         throw new InvalidCastException("Divided block statement outside of a statement container");
       }
       // We need to indicate to Dafny that 
-      TrStmtList(dividedBlockStmt.BodyProper, writer);
+      TrStmtList(context, dividedBlockStmt.BodyProper, writer);
     }
 
     protected override bool InstanceConstAreStatic() {
@@ -1278,7 +1279,8 @@ protected override ConcreteSyntaxTree EmitBlock(ConcreteSyntaxTree wr) {
     }
 
     // Return a writer to write the start expression, which is lo if going up, and hi if going down
-    protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string endVarName,
+    protected override ConcreteSyntaxTree EmitForStmt(StatementGenerationContext context, IToken tok,
+      IVariable loopIndex, bool goingUp, string endVarName,
       List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
       if (GetStatementBuilder(wr, out var statementContainer)) {
         var indexName = loopIndex.CompileNameShadowable;
@@ -1292,7 +1294,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
             ));
           ConcreteSyntaxTree bodyWr = new BuilderSyntaxTree<StatementContainer>(foreachBuilder, this);
           bodyWr = EmitContinueLabel(labels, bodyWr);
-          TrStmtList(body, bodyWr);
+          TrStmtList(context, body, bodyWr);
           return new BuilderSyntaxTree<ExprContainer>(startBuilder, this);
         } else {
           var loHiBuilder = ((ExprContainer)foreachBuilder).BinOp("int_range", (DAST.Expression lo, DAST.Expression hi) =>
@@ -1304,7 +1306,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
              ));
           ConcreteSyntaxTree bodyWr = new BuilderSyntaxTree<StatementContainer>(foreachBuilder, this);
           bodyWr = EmitContinueLabel(labels, bodyWr);
-          TrStmtList(body, bodyWr);
+          TrStmtList(context, body, bodyWr);
           BuilderSyntaxTree<ExprContainer> toReturn;
           if (goingUp) {
             toReturn = WrBuffer(out var loBuf);
@@ -3226,8 +3228,9 @@ protected override void OrganizeModules(Program program, out List<ModuleDefiniti
         String.Compare(a.FullDafnyName, b.FullDafnyName, StringComparison.Ordinal));
     }
 
-    protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr) {
-      TrStmt(body, wr);
+    protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody,
+      ConcreteSyntaxTree wr, StatementGenerationContext context) {
+      TrStmt(context, body, wr);
     }
 
     protected override ConcreteSyntaxTree GetNullClassConcreteSyntaxTree() {
@@ -3244,8 +3247,9 @@ protected override void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultT
       TrExprOpt(match.Flattened, resultType, wr, wStmts, inLetExprBody, accumulatorVar, continuation);
     }
 
-    protected override void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {
-      TrStmt(match.Flattened, writer);
+    protected override void EmitNestedMatchStmt(StatementGenerationContext context, NestedMatchStmt match,
+      ConcreteSyntaxTree writer) {
+      TrStmt(context, match.Flattened, writer);
     }
   }
 }

Source/DafnyCore/Backends/GoLang/GoBackend.cs → Source/DafnyCore/Backends/GoLang/GoLangBackend.cs

@@ -11,7 +11,7 @@
 
 namespace Microsoft.Dafny;
 
-public class GoBackend : ExecutableBackend {
+public class GoLangBackend : ExecutableBackend {
 
   public override IReadOnlySet<string> SupportedExtensions => new HashSet<string> { ".go" };
 
@@ -39,7 +39,7 @@ public override string TargetBaseDir(string dafnyProgramName) {
   };
   public override IEnumerable<Option<string>> SupportedOptions => new List<Option<string>> { GoModuleNameCliOption };
 
-  static GoBackend() {
+  static GoLangBackend() {
     OptionRegistry.RegisterOption(GoModuleNameCliOption, OptionScope.Translation);
   }
 
@@ -49,7 +49,7 @@ protected override SinglePassCodeGenerator CreateCodeGenerator() {
     if (GoModuleMode) {
       GoModuleName = goModuleName;
     }
-    return new GoCodeGenerator(Options, Reporter);
+    return new GoLangCodeGenerator(Options, Reporter);
   }
 
   public override async Task<bool> OnPostGenerate(string dafnyProgramName, string targetDirectory, TextWriter outputWriter) {
@@ -237,6 +237,6 @@ private static string FindPackageName(string externFilename) {
 
   private static readonly Regex PackageLine = new Regex(@"^\s*package\s+([a-zA-Z0-9_]+)\s*$");
 
-  public GoBackend(DafnyOptions options) : base(options) {
+  public GoLangBackend(DafnyOptions options) : base(options) {
   }
 }

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs → Source/DafnyCore/Backends/GoLang/GoLangCodeGenerator.cs

@@ -18,7 +18,7 @@
 using static Microsoft.Dafny.ConcreteSyntaxTreeUtils;
 
 namespace Microsoft.Dafny.Compilers {
-  class GoCodeGenerator : SinglePassCodeGenerator {
+  class GoLangCodeGenerator : SinglePassCodeGenerator {
     protected override void EmitStaticExternMethodQualifier(string qual, ConcreteSyntaxTree wr) {
       if (qual != null) {
         qual = ImportPrefix + qual;
@@ -31,8 +31,8 @@ protected override void EmitStaticExternMethodQualifier(string qual, ConcreteSyn
 
     private bool GoModuleMode;
     private string GoModuleName;
-    public GoCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
-      var goModuleName = Options.Get(GoBackend.GoModuleNameCliOption);
+    public GoLangCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
+      var goModuleName = Options.Get(GoLangBackend.GoModuleNameCliOption);
       GoModuleMode = goModuleName != null;
       if (GoModuleMode) {
         GoModuleName = goModuleName.ToString();
@@ -166,8 +166,8 @@ ConcreteSyntaxTree CreateDescribedSection(string desc, ConcreteSyntaxTree wr, pa
     }
 
     protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) {
-      var wr = ((GoCodeGenerator.ClassWriter)cw).ConcreteMethodWriter;
-      return wr.NewNamedBlock("func (_this * {0}) Main({1} _dafny.Sequence)", FormatCompanionTypeName(((GoCodeGenerator.ClassWriter)cw).ClassName), argsParameterName);
+      var wr = ((GoLangCodeGenerator.ClassWriter)cw).ConcreteMethodWriter;
+      return wr.NewNamedBlock("func (_this * {0}) Main({1} _dafny.Sequence)", FormatCompanionTypeName(((GoLangCodeGenerator.ClassWriter)cw).ClassName), argsParameterName);
     }
 
     private Import CreateImport(string moduleName, ModuleDefinition externModule,
@@ -256,7 +256,7 @@ protected override void DependOnModule(Program program, ModuleDefinition module,
           var translatedRecord = program.Compilation.AlreadyTranslatedRecord;
           translatedRecord.OptionsByModule.TryGetValue(module.FullDafnyName, out var moduleOptions);
           object moduleName = null;
-          moduleOptions?.TryGetValue(GoBackend.GoModuleNameCliOption.Name, out moduleName);
+          moduleOptions?.TryGetValue(GoLangBackend.GoModuleNameCliOption.Name, out moduleName);
 
           goModuleName = moduleName is string name ? moduleName + "/" : "";
           if (String.IsNullOrEmpty(goModuleName)) {
@@ -338,7 +338,7 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
     }
 
     // TODO Consider splitting this into two functions; most things seem to be passing includeRtd: false, includeEquals: false and includeString: true.
-    private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, string name, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, List<Type>/*?*/ superClasses, IToken tok, ConcreteSyntaxTree wr, bool includeRtd, bool includeEquals, bool includeString) {
+    private GoLangCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, string name, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, List<Type>/*?*/ superClasses, IToken tok, ConcreteSyntaxTree wr, bool includeRtd, bool includeEquals, bool includeString) {
       // See docs/Compilation/ReferenceTypes.md for a description of how instance members of classes and traits are compiled into Go.
       //
       // func New_Class_(Type0 _dafny.TypeDescriptor, Type1 _dafny.TypeDescriptor) *Class {
@@ -1229,15 +1229,15 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name,
       }
     }
     protected class ClassWriter : IClassWriter {
-      public readonly GoCodeGenerator CodeGenerator;
+      public readonly GoLangCodeGenerator CodeGenerator;
       public readonly TopLevelDecl ClassContext;
       public readonly bool IsClass;
       public readonly string ClassName;
       public readonly bool IsExtern;
       public readonly ConcreteSyntaxTree/*?*/ AbstractMethodWriter, ConcreteMethodWriter, InstanceFieldWriter, InstanceFieldInitWriter, TraitInitWriter, StaticFieldWriter, StaticFieldInitWriter;
       public bool AnyInstanceFields { get; private set; } = false;
 
-      public ClassWriter(GoCodeGenerator codeGenerator, TopLevelDecl classContext, bool isClass, string className, bool isExtern, ConcreteSyntaxTree abstractMethodWriter, ConcreteSyntaxTree concreteMethodWriter,
+      public ClassWriter(GoLangCodeGenerator codeGenerator, TopLevelDecl classContext, bool isClass, string className, bool isExtern, ConcreteSyntaxTree abstractMethodWriter, ConcreteSyntaxTree concreteMethodWriter,
         ConcreteSyntaxTree/*?*/ instanceFieldWriter, ConcreteSyntaxTree/*?*/ instanceFieldInitWriter, ConcreteSyntaxTree/*?*/ traitInitWriter,
         ConcreteSyntaxTree staticFieldWriter, ConcreteSyntaxTree staticFieldInitWriter) {
         Contract.Requires(codeGenerator != null);
@@ -1579,7 +1579,7 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToke
     protected override bool SupportsStaticsInGenericClasses => false;
     protected override bool TraitRepeatsInheritedDeclarations => true;
 
-    private void FinishClass(GoCodeGenerator.ClassWriter cw) {
+    private void FinishClass(GoLangCodeGenerator.ClassWriter cw) {
       // Go gets weird about zero-length structs.  In particular, it likes to
       // make all pointers to a zero-length struct the same.  Irritatingly, this
       // forces us to waste space here.
@@ -2102,7 +2102,8 @@ protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree gua
       return wBody;
     }
 
-    protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
+    protected override ConcreteSyntaxTree EmitForStmt(StatementGenerationContext context, IToken tok,
+      IVariable loopIndex, bool goingUp, string endVarName, /*?*/
       List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
 
       wr.Write($"for {loopIndex.GetOrCreateCompileName(currentIdGenerator)} := ");
@@ -2139,7 +2140,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
         }
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
-      TrStmtList(body, bodyWr);
+      TrStmtList(context, body, bodyWr);
 
       return startWr;
     }
@@ -4085,15 +4086,16 @@ protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBod
       TrParenExpr("_dafny.SingleValue", e, wr, inLetExprBody, wStmts);
     }
 
-    protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr) {
+    protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody,
+      ConcreteSyntaxTree wr, StatementGenerationContext context) {
       var funcBlock = wr.NewBlock("func()", close: BlockStyle.Brace);
       var deferBlock = funcBlock.NewBlock("defer func()", close: BlockStyle.Brace);
       var ifRecoverBlock = deferBlock.NewBlock("if r := recover(); r != nil");
       var stringMaker = UnicodeCharEnabled ? "UnicodeSeqOfUtf8Bytes" : "SeqOfString";
       ifRecoverBlock.WriteLine($"var {haltMessageVarName} = {HelperModulePrefix}{stringMaker}(r.(string))");
-      TrStmt(recoveryBody, ifRecoverBlock);
+      TrStmt(context, recoveryBody, ifRecoverBlock);
       funcBlock.WriteLine("()");
-      TrStmt(body, funcBlock);
+      TrStmt(context, body, funcBlock);
       wr.WriteLine("()");
     }
   }

Source/DafnyCore/Backends/InternalBackendsPluginConfiguration.cs

@@ -9,7 +9,7 @@ public override IExecutableBackend[] GetCompilers(DafnyOptions options) {
     return new IExecutableBackend[] {
       new CsharpBackend(options),
       new JavaScriptBackend(options),
-      new GoBackend(options),
+      new GoLangBackend(options),
       new JavaBackend(options),
       new PythonBackend(options),
       new CppBackend(options),

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -3858,7 +3858,8 @@ protected override ConcreteSyntaxTree CreateForLoop(string indexVar, Action<Conc
       return wr.NewNamedBlock($"for (java.math.BigInteger {indexVar} = {start}; {indexVar}.compareTo({bound}) < 0; {indexVar} = {indexVar}.add(java.math.BigInteger.ONE))");
     }
 
-    protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
+    protected override ConcreteSyntaxTree EmitForStmt(StatementGenerationContext context, IToken tok,
+      IVariable loopIndex, bool goingUp, string endVarName, /*?*/
       List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
 
       var nativeType = AsNativeType(loopIndex.Type);
@@ -3901,7 +3902,7 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
         }
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
-      TrStmtList(body, bodyWr);
+      TrStmtList(context, body, bodyWr);
 
       return startWr;
     }
@@ -4386,12 +4387,13 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete
       throw new UnsupportedFeatureException(iter.tok, Feature.Iterators);
     }
 
-    protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr) {
+    protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody,
+      ConcreteSyntaxTree wr, StatementGenerationContext context) {
       var tryBlock = wr.NewBlock("try");
-      TrStmt(body, tryBlock);
+      TrStmt(context, body, tryBlock);
       var catchBlock = wr.NewBlock("catch (dafny.DafnyHaltException e)");
       catchBlock.WriteLine($"dafny.DafnySequence<Character> {haltMessageVarName} = dafny.DafnySequence.asString(e.getMessage());");
-      TrStmt(recoveryBody, catchBlock);
+      TrStmt(context, recoveryBody, catchBlock);
     }
 
     protected override void EmitNestedMatchExpr(NestedMatchExpr match, bool inLetExprBody, ConcreteSyntaxTree output,
@@ -4412,11 +4414,12 @@ protected override void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultT
       }
     }
 
-    protected override void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {
+    protected override void EmitNestedMatchStmt(StatementGenerationContext context, NestedMatchStmt match,
+      ConcreteSyntaxTree writer) {
       if (match.Cases.Count == 0) {
-        base.EmitNestedMatchStmt(match, writer);
+        base.EmitNestedMatchStmt(context, match, writer);
       } else {
-        TrStmt(match.Flattened, writer);
+        TrStmt(context, match.Flattened, writer);
       }
     }
   }