Syncing RDE Work #4745
Syncing RDE Work #4745
Conversation
…zation in dafny compiler
| @@ -2,15 +2,209 @@ module {:extern "ResolvedDesugaredExecutableDafnyPlugin"} ResolvedDesugaredExecu | |||
| import opened DAST | |||
| import PrettyPrinter | |||
| import UnsupportedFeature | |||
| import DAM | |||
|
|
|||
| class COMP { | |||
There was a problem hiding this comment.
Class COMP only has static members. Remove the class altogether and instead declare the members as module-level members.
There was a problem hiding this comment.
Thanks, I think that should be fine as long as Compiler-dafny.cs does not depend on the fact that COMP is a class by way of its translation to C# in GeneratedFromDafny.cs.
| case Break(lab) => { | ||
| match lab | ||
| case Some(lab) => | ||
| st := DAM.Throw(DAM.Var(lab), DAM.Skip()); | ||
| case None => UnsupportedFeature.Throw(); st := DAM.Skip(); | ||
| } |
There was a problem hiding this comment.
Instead of putting { ... } around the entire match lab ... statement, put the { ... } around the list of cases, like this:
match lab {
case Some(lab) =>
...
case None => ...
}| type Field = string | ||
|
|
||
| datatype Pos = | ||
| Unit |
There was a problem hiding this comment.
Add a prefix | to make all the alternatives look the same.
| } | ||
|
|
||
| // S |- stack <= start- <= end- | ||
| predicate CheckStack(s: StoreTyping, start: Neg, stack: Stack, end: Neg) { |
There was a problem hiding this comment.
The name CheckStack sounds operational, using the verb "check". Wouldn't it be more appropriate to think of a predicate is using an adjective, like ValidStack?
For that matter, it is also possible to rename the predicate just Valid and declare it as a member of the StoreTyping type.
There was a problem hiding this comment.
+1 for grouping checking/synthesis functions into each type definition
The terminology Check/Synth is a reference to the two modes of bidirectional typing (checking against a type vs. synthesis of a type).
Description
Pretty printing RDE Dafny backend + Dafny Abstract Machine.
How has this been tested?
Pretty printing tested on "Hello, World".
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.