PR feedback, release note

dafny-lang · Nov 1, 2023 · 761cbf8 · 761cbf8
1 parent ab8c23b
commit 761cbf8
Show file tree

Hide file tree

Showing 11 changed files with 28 additions and 19 deletions.
diff --git a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs
@@ -15,7 +15,7 @@ public static bool ShouldCompile(this ModuleDefinition module, CompilationData p
     if (module.FullName == "_System") {
       return program.Options.SystemModuleTranslationMode != CommonOptionBag.SystemModuleMode.Omit;
     }
-    if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.Populate) {
+    if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
       return false;
     }
 

diff --git a/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs
@@ -50,7 +50,7 @@ private TupleTypeDecl(ModuleDefinition systemModule, List<TypeParameter> typeArg
     }
     this.EqualitySupport = argumentGhostness.Contains(true) ? ES.Never : ES.ConsultTypeArguments;
 
-    // TODO: Correct?
+    // Resolve parent type information - not currently possible for tuples to have any parent traits
     ParentTypeInformation = new InheritanceInformationClass();
   }
   private static List<TypeParameter> CreateCovariantTypeParameters(int dims) {

diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
@@ -73,21 +73,21 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       wr.WriteLine("// Optionally, you may want to include compiler switches like");
       wr.WriteLine("//     /debug /nowarn:162,164,168,183,219,436,1717,1718");
       wr.WriteLine();
-      if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.Populate) {
+      if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
         wr.WriteLine("#if ISDAFNYRUNTIMELIB");
       }
       wr.WriteLine("using System;");
       wr.WriteLine("using System.Numerics;");
       wr.WriteLine("using System.Collections;");
-      if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.Populate) {
+      if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
         wr.WriteLine("#endif");
       }
       Synthesize = ProgramHasMethodsWithAttr(program, "synthesize");
       if (Synthesize) {
         CsharpSynthesizer.EmitImports(wr);
       }
 
-      if (program.Options.SystemModuleTranslationMode != CommonOptionBag.SystemModuleMode.Populate) {
+      if (program.Options.SystemModuleTranslationMode != CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
         EmitDafnySourceAttribute(program, wr);
       }
 
@@ -135,19 +135,22 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
             CheckCommonSytemModuleLimits(systemModuleManager);
             break;
           }
-        case CommonOptionBag.SystemModuleMode.Populate: {
+        case CommonOptionBag.SystemModuleMode.OmitAllOtherModules: {
             CheckSystemModulePopulatedToCommonLimits(systemModuleManager);
             break;
           }
       }
 
       // The declarations below would normally be omitted if we aren't compiling the system module,
       // but they are all marked as "internal", so they have to be included in each separately-compiled assembly.
+      // In particular, FuncExtensions contain extension methods for the System.Func<> family of delegates,
+      // and extension methods always only apply within the current assembly.
+      //
       // Instead we just make sure to guard them with "#if ISDAFNYRUNTIMELIB" when compiling the system module,
       // so they don't become duplicates when --include-runtime is used.
       // See comment at the top of DafnyRuntime.cs.
 
-      if (Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.Populate) {
+      if (Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
         wr.WriteLine("#if ISDAFNYRUNTIMELIB");
       }
 
@@ -158,7 +161,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
       }
       EmitFuncExtensions(systemModuleManager, wr);
 
-      if (Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.Populate) {
+      if (Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
         wr.WriteLine("#endif");
       }
     }

diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
@@ -267,7 +267,7 @@ protected override ConcreteSyntaxTree EmitIngredients(ConcreteSyntaxTree wr, str
       var wStmts = wr.Fork();
       var wrVarInit = wr;
       wrVarInit.Write($"java.util.ArrayList<{DafnyTupleClass(L)}<{tupleTypeArgs}>> {ingredients} = ");
-      // TODO: Assert that Tuple(L) exists in the _System module
+      Contract.Assert(L <= MaxTupleNonGhostDims);
       EmitEmptyTupleList(tupleTypeArgs, wrVarInit);
       var wrOuter = wr;
       wr = CompileGuardedLoops(s.BoundVars, s.Bounds, s.Range, wr);
@@ -316,7 +316,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
             CheckCommonSytemModuleLimits(systemModuleManager);
             return;
           }
-        case CommonOptionBag.SystemModuleMode.Populate: {
+        case CommonOptionBag.SystemModuleMode.OmitAllOtherModules: {
             CheckSystemModulePopulatedToCommonLimits(systemModuleManager);
             break;
           }
@@ -373,7 +373,6 @@ private void EmitImport(Import import, ConcreteSyntaxTree importWriter) {
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string /*?*/ libraryName, ConcreteSyntaxTree wr) {
       if (isDefault) {
         // Fold the default module into the main module
-        // return wr;
         moduleName = "_System";
       }
       var pkgName = libraryName ?? IdProtect(moduleName);
@@ -1837,7 +1836,12 @@ protected override ConcreteSyntaxTree EmitSign(Type type, ConcreteSyntaxTree wr)
 
     protected override IClassWriter/*?*/ DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxTree wr) {
       if (dt is TupleTypeDecl tupleTypeDecl) {
-        // CreateTuple() produces somewhat different code
+        // CreateTuple() produces quite different code than this method would
+        // by treating a tuple declaration as just a special case of a datatype.
+        // Compare to the C# compiler which just compiles tuples like datatypes
+        // with a bit of special handling for the name.
+        // This could be changed to match at some point, but it would break
+        // code that relies on the current runtime representation of tuples in Java.
         CreateTuple(tupleTypeDecl.Dims, wr);
         return null;
       }

diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -239,8 +239,8 @@ May slow down verification slightly.
   public enum SystemModuleMode {
     Include,
     Omit,
-    // TODO: better name? OmitOthers?
-    Populate
+    // Used to pre-compile the System module into the runtimes
+    OmitAllOtherModules
   }
 
   public static readonly Option<SystemModuleMode> SystemModule = new("--system-module", () => SystemModuleMode.Omit,

diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/Makefile b/Source/DafnyRuntime/DafnyRuntimeGo/Makefile
@@ -11,7 +11,7 @@ test:
 	cd dafny &&	GO111MODULE=auto go test
 
 build-system-module:
-	$(DAFNY) translate go --no-verify --use-basename-for-filename --system-module:Populate ../systemModulePopulator.dfy --output:../obj/systemModulePopulator
+	$(DAFNY) translate go --no-verify --use-basename-for-filename --system-module:OmitAllOtherModules ../systemModulePopulator.dfy --output:../obj/systemModulePopulator
 
 check-system-module: build-system-module
 	diff $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET)

diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/Makefile b/Source/DafnyRuntime/DafnyRuntimeJava/Makefile
@@ -15,7 +15,7 @@ test:
 
 # TODO: Add --optimize-erasable-datatype-wrapper:false elsewhere too
 build-system-module:
-	$(DAFNY) translate java --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false --system-module:Populate ../systemModulePopulator.dfy --output:../obj/systemModulePopulator
+	$(DAFNY) translate java --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false --system-module:OmitAllOtherModules ../systemModulePopulator.dfy --output:../obj/systemModulePopulator
 
 check-system-module: build-system-module
 	diff $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET)

diff --git a/Source/DafnyRuntime/DafnyRuntimeJs/Makefile b/Source/DafnyRuntime/DafnyRuntimeJs/Makefile
@@ -8,7 +8,7 @@ GENERATED_SYSTEM_MODULE_TARGET=DafnyRuntimeSystemModule.js
 all: check-system-module
 
 build-system-module:
-	$(DAFNY) translate js --no-verify --use-basename-for-filename --system-module:Populate ../systemModulePopulator.dfy --output:../obj/systemModulePopulator
+	$(DAFNY) translate js --no-verify --use-basename-for-filename --system-module:OmitAllOtherModules ../systemModulePopulator.dfy --output:../obj/systemModulePopulator
 
 check-system-module: build-system-module
 	diff $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET)

diff --git a/Source/DafnyRuntime/DafnyRuntimePython/Makefile b/Source/DafnyRuntime/DafnyRuntimePython/Makefile
@@ -8,7 +8,7 @@ GENERATED_SYSTEM_MODULE_TARGET=System_.py
 all: check-system-module
 
 build-system-module:
-	$(DAFNY) translate py --no-verify --use-basename-for-filename --system-module:Populate ../systemModulePopulator.dfy --output:../obj/systemModulePopulator
+	$(DAFNY) translate py --no-verify --use-basename-for-filename --system-module:OmitAllOtherModules ../systemModulePopulator.dfy --output:../obj/systemModulePopulator
 
 check-system-module: build-system-module
 	diff $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET)

diff --git a/Source/DafnyRuntime/Makefile b/Source/DafnyRuntime/Makefile
@@ -8,7 +8,7 @@ GENERATED_SYSTEM_MODULE_TARGET=DafnyRuntimeSystemModule.cs
 all: check-system-module
 
 build-system-module:
-	$(DAFNY) translate cs --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false --system-module:Populate systemModulePopulator.dfy --output:obj/systemModulePopulator
+	$(DAFNY) translate cs --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false --system-module:OmitAllOtherModules systemModulePopulator.dfy --output:obj/systemModulePopulator
 
 check-system-module: build-system-module
 	diff $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET)

diff --git a/docs/dev/news/4658.feat b/docs/dev/news/4658.feat
@@ -0,0 +1,2 @@
+Built-in types such as the `nat` subset type, tuples, arrows, and arrays are now pre-compiled into each backend's runtime library,
+instead of emitted on every call to `dafny translate`, to avoid potential duplicate definitions when translating components separately.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		Built-in types such as the `nat` subset type, tuples, arrows, and arrays are now pre-compiled into each backend's runtime library,
		instead of emitted on every call to `dafny translate`, to avoid potential duplicate definitions when translating components separately.