feat: Populate runtimes with all built-in declarations #4658
Conversation
robin-aws
changed the title
| } | ||
|
|
||
| protected void CheckSystemModulePopulatedToCommonLimits(SystemModuleManager systemModuleManager) { | ||
| systemModuleManager.CheckHasAllTupleNonGhostDimsUpTo(20); |
There was a problem hiding this comment.
Let's make sure the numbers in CheckCommonSytemModuleLimits match those in CheckSystemModulePopulatedToCommonLimits
Source/TestDafny/MultiBackendTest.cs
Outdated
| if (compiler.TargetId == "cs") { | ||
| // C# is a bit unusual in that the runtime behaves a little differently | ||
| // depending on whether it is included as source or referenced as DafnyRuntime.dll | ||
| // (because of "#ifdef ISDAFNYRUNTIMELIB" directives). |
There was a problem hiding this comment.
I didn't get what these directives are for. Could you add documentation on that somewhere close to the C# runtime or compiler?
|
This is looking amazing already ! Awesome work |
| @@ -49,6 +49,9 @@ private TupleTypeDecl(ModuleDefinition systemModule, List<TypeParameter> typeArg | |||
| } | |||
| } | |||
| this.EqualitySupport = argumentGhostness.Contains(true) ? ES.Never : ES.ConsultTypeArguments; | |||
|
|
|||
| // TODO: Correct? | |||
| } | ||
| } | ||
|
|
||
| // The declarations below would normally be omitted if we aren't compiling the system module, |
There was a problem hiding this comment.
Seems like these declarations could be not-internal and only as part of the system module
There was a problem hiding this comment.
I tried that, but realized FuncExtensions in particular is tricky because they are extension methods on the System.Func family of delegates, and extension methods only ever apply within the current assembly. Given that I didn't bother spending the time moving the Array helper functions either. I'm adding a comment about this here though.
There was a problem hiding this comment.
extension methods only ever apply within the current assembly
I don't get what you mean. You can use extensions methods defined in a library for sure.
| @@ -269,7 +267,7 @@ private enum JavaNativeType { Byte, Short, Int, Long } | |||
| var wStmts = wr.Fork(); | |||
| var wrVarInit = wr; | |||
| wrVarInit.Write($"java.util.ArrayList<{DafnyTupleClass(L)}<{tupleTypeArgs}>> {ingredients} = "); | |||
| AddTupleToSet(L); | |||
| // TODO: Assert that Tuple(L) exists in the _System module | |||
| @@ -370,7 +373,8 @@ private enum JavaNativeType { Byte, Short, Int, Long } | |||
| 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; | |||
| // return wr; | |||
There was a problem hiding this comment.
Please remove the comment
| @@ -1840,6 +1836,12 @@ protected class ClassWriter : IClassWriter { | |||
| } | |||
|
|
|||
| protected override IClassWriter/*?*/ DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxTree wr) { | |||
| if (dt is TupleTypeDecl tupleTypeDecl) { | |||
| // CreateTuple() produces somewhat different code | |||
There was a problem hiding this comment.
I don't get the comment. What produces different code than what?
| public enum SystemModuleMode { | ||
| Include, | ||
| Omit, | ||
| // TODO: better name? OmitOthers? |
There was a problem hiding this comment.
The rule of these names seems to be to describe the effect, not the reason behind it (populate), so OmitAllOtherModules or OnlyIncludeSystem[Module] match well.
|
Left a few minor comments. Feel free to merge first and address them as a follow-up |
Description
Fixes #511
Generalizes the approach used in #2284 to pre-generate all built-in declarations into the various runtimes:
--system-moduleoption to control how the system module is treated when translating:systemModulePopulator.dfyfile, previously namedtuplesForDafnyRuntime.dfy. The output is now present in each runtime in a separate file/source location, and checked for consistency in CI just as other Dafny-generated committed source is.DafnyPipelineto support more than one file better (as Go already was).TODOs:
internalfrom C# helper code (and tests to confirm it works)How has this been tested?
Mostly existing tests, but also added an internal version of
--include-runtimefordafny run, so that%testDafnyForEachCompilercan include testing on C# when using the separateDafnyRuntime.dlllibrary, as that behaves significantly different in this case.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.