feat: Populate runtimes with all built-in declarations

.github/workflows/msbuild.yml

@@ -53,7 +53,7 @@ jobs:
       run: dotnet build Source/Dafny.sln
     - name: Check whitespace and style
       working-directory: dafny
-      run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs
+      run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyRuntime/DafnyRuntimeSystemModule.cs
     - name: Create NuGet package (just to make sure it works)
       run: dotnet pack --no-build dafny/Source/Dafny.sln
     - name: Check uniformity of integration tests that exercise backends

.github/workflows/runtime-tests.yml

@@ -38,18 +38,27 @@ jobs:
           cd ./Source/DafnyCore
           make test
           make check-format
+      - name: Test DafnyRuntime (C#)
+        run: |
+          cd ./Source/DafnyRuntime
+          make all
       - name: Test DafnyRuntimeDafny
         run: |
           cd ./Source/DafnyRuntime/DafnyRuntimeDafny
-          make test
-          make check-format
+          make all
       - name: Test DafnyRuntimeGo
         run: |
           cd ./Source/DafnyRuntime/DafnyRuntimeGo
-          make test
-      # This isn't strictly necessary since the Java runtime has to be built into a jar,
-      # which also runs the tests.
-      # But I prefer the simplicity of testing every testable runtime in this workflow
+          make all
       - name: Test DafnyRuntimeJava
-        run: ./Source/DafnyRuntime/DafnyRuntimeJava/gradlew -p ./Source/DafnyRuntime/DafnyRuntimeJava test
-
+        run: |
+          cd ./Source/DafnyRuntime/DafnyRuntimeJava
+          make all
+      - name: Test DafnyRuntimePython
+        run: |
+          cd ./Source/DafnyRuntime/DafnyRuntimePython
+          make all
+      - name: Test DafnyRuntimeJs
+        run: |
+          cd ./Source/DafnyRuntime/DafnyRuntimeJs
+          make all

Source/DafnyCore/AST/ShouldCompileOrVerify.cs

@@ -13,7 +13,10 @@ public static bool ShouldCompile(this ModuleDefinition module, CompilationData p
     }
 
     if (module.FullName == "_System") {
-      return true;
+      return program.Options.SystemModuleTranslationMode != CommonOptionBag.SystemModuleMode.Omit;
+    }
+    if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.Populate) {
+      return false;
     }
 
     if (module is DefaultModuleDefinition) {

Source/DafnyCore/AST/SystemModuleManager.cs

@@ -415,7 +415,7 @@ public TupleTypeDecl TupleType(IToken tok, int dims, bool allowCreationOfNewType
         nonGhostTupleTypeDecl = TupleType(tok, nonGhostDims, allowCreationOfNewType);
       }
 
-      tt = new TupleTypeDecl(argumentGhostness, SystemModule, nonGhostTupleTypeDecl, DontCompile());
+      tt = new TupleTypeDecl(argumentGhostness, SystemModule, nonGhostTupleTypeDecl, null);
       if (tt.NonGhostDims > MaxNonGhostTupleSizeUsed) {
         MaxNonGhostTupleSizeToken = tok;
         MaxNonGhostTupleSizeUsed = tt.NonGhostDims;
@@ -490,6 +490,39 @@ public void ResolveValueTypeDecls(ProgramResolver programResolver) {
       }
     }
   }
+
+  public void CheckHasAllTupleNonGhostDimsUpTo(int max) {
+    var allNeededDims = Enumerable.Range(0, max + 1).ToHashSet();
+    var allDeclaredDims = tupleTypeDecls.Keys
+        .Select(argumentGhostness => argumentGhostness.Count(ghost => !ghost))
+        .Distinct()
+        .ToHashSet();
+    if (!allDeclaredDims.SetEquals(allNeededDims)) {
+      throw new ArgumentException(@$"Not all tuple types declared between 0 and {max}!
+needed: {allNeededDims.Comma()}
+declared: {allDeclaredDims.Comma()}");
+    }
+  }
+
+  public void CheckHasAllArrayDimsUpTo(int max) {
+    var allNeededDims = Enumerable.Range(1, max).ToHashSet();
+    var allDeclaredDims = arrayTypeDecls.Keys.ToHashSet();
+    if (!allDeclaredDims.SetEquals(allNeededDims)) {
+      throw new ArgumentException(@$"Not all array types declared between 1 and {max}!
+needed: {allNeededDims.Comma()}
+declared: {allDeclaredDims.Comma()}");
+    }
+  }
+
+  public void CheckHasAllArrowAritiesUpTo(int max) {
+    var allNeededArities = Enumerable.Range(0, max + 1).ToHashSet();
+    var allDeclaredArities = ArrowTypeDecls.Keys.ToHashSet();
+    if (!allDeclaredArities.SetEquals(allNeededArities)) {
+      throw new ArgumentException(@$"Not all arrow types declared between 0 and {max}
+needed: {allNeededArities.Comma()}
+declared: {allDeclaredArities.Comma()}");
+    }
+  }
 }
 
 enum ValuetypeVariety {

Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs

@@ -49,6 +49,9 @@ private TupleTypeDecl(ModuleDefinition systemModule, List<TypeParameter> typeArg
       }
     }
     this.EqualitySupport = argumentGhostness.Contains(true) ? ES.Never : ES.ConsultTypeArguments;
+
+    // TODO: Correct?
+    ParentTypeInformation = new InheritanceInformationClass();
   }
   private static List<TypeParameter> CreateCovariantTypeParameters(int dims) {
     Contract.Requires(0 <= dims);

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -24,7 +24,9 @@ public class CsharpCompiler : SinglePassCompiler {
 
     public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
       Feature.SubsetTypeTests,
-      Feature.TuplesWiderThan20
+      Feature.TuplesWiderThan20,
+      Feature.ArraysWithMoreThan16Dims,
+      Feature.ArrowsWithMoreThan16Arguments
     };
 
     public CsharpCompiler(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
@@ -71,17 +73,26 @@ 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) {
+        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) {
+        wr.WriteLine("#endif");
+      }
       Synthesize = ProgramHasMethodsWithAttr(program, "synthesize");
       if (Synthesize) {
         CsharpSynthesizer.EmitImports(wr);
       }
-      EmitDafnySourceAttribute(program, wr);
+
+      if (program.Options.SystemModuleTranslationMode != CommonOptionBag.SystemModuleMode.Populate) {
+        EmitDafnySourceAttribute(program, wr);
+      }
 
       if (Options.IncludeRuntime) {
-        ReadRuntimeSystem(program, "DafnyRuntime.cs", wr);
+        EmitRuntimeSource("DafnyRuntimeCsharp", wr, false);
       }
 
     }
@@ -119,8 +130,25 @@ void EmitDafnySourceAttribute(Program program, ConcreteSyntaxTree wr) {
     }
 
     protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager, ConcreteSyntaxTree wr) {
-      if (systemModuleManager.MaxNonGhostTupleSizeUsed > 20) {
-        UnsupportedFeatureError(systemModuleManager.MaxNonGhostTupleSizeToken, Feature.TuplesWiderThan20);
+      switch (Options.SystemModuleTranslationMode) {
+        case CommonOptionBag.SystemModuleMode.Omit: {
+            CheckCommonSytemModuleLimits(systemModuleManager);
+            break;
+          }
+        case CommonOptionBag.SystemModuleMode.Populate: {
+            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.
+      // 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) {
+        wr.WriteLine("#if ISDAFNYRUNTIMELIB");
       }
 
       var dafnyNamespace = CreateModule("Dafny", false, false, null, wr);
@@ -129,6 +157,10 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
         CsharpSynthesizer.EmitMultiMatcher(dafnyNamespace);
       }
       EmitFuncExtensions(systemModuleManager, wr);
+
+      if (Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.Populate) {
+        wr.WriteLine("#endif");
+      }
     }
 
     // Generates casts for functions of those arities present in the program, like:

Source/DafnyCore/Compilers/CSharp/Synthesizer-Csharp.cs

@@ -317,7 +317,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, ForallExpr forallExpr,
   /// </summary>
   internal static void EmitMultiMatcher(ConcreteSyntaxTree dafnyNamespace) {
     const string multiMatcher = @"
-    class MultiMatcher {
+    internal class MultiMatcher {
 
       private readonly Func<object[], bool> predicate;
       private readonly int argumentCount;

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -55,7 +55,8 @@ public CppCompiler(DafnyOptions options, ErrorReporter reporter, ReadOnlyCollect
       Feature.RunAllTests,
       Feature.MethodSynthesis,
       Feature.UnicodeChars,
-      Feature.ConvertingValuesToStrings
+      Feature.ConvertingValuesToStrings,
+      Feature.BuiltinsInRuntime
     };
 
     private List<DatatypeDecl> datatypeDecls = new();
@@ -118,10 +119,8 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       this.classDeclsWr = headerFileWr.Fork();
       this.hashWr = headerFileWr.Fork();
 
-      var rt = wr.NewFile("DafnyRuntime.h");
-
       if (Options.IncludeRuntime) {
-        ReadRuntimeSystem(program, "DafnyRuntime.h", rt);
+        EmitRuntimeSource("DafnyRuntimeCpp", wr);
       }
 
     }

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

@@ -66,16 +66,10 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       EmitImports(wr, out RootImportWriter, out RootImportDummyWriter);
 
       if (Options.IncludeRuntime) {
-        var rt = wr.NewFile("dafny/dafny.go");
-        ReadRuntimeSystem(program, "DafnyRuntime.go", rt);
-        rt = wr.NewFile("dafny/dafnyFromDafny.go");
-        ReadRuntimeSystem(program, "DafnyRuntimeFromDafny.go", rt);
+        EmitRuntimeSource("DafnyRuntimeGo", wr);
       }
     }
 
-    protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager, ConcreteSyntaxTree wr) {
-    }
-
     private string DafnyTypeDescriptor => $"{HelperModulePrefix}TypeDescriptor";
 
     // The implementation of seq<T> is now in DafnyRuntimeDafny/src/dafnyRuntime.dfy.