feat: Modules in the python backend #1871

fabiomadge · 2022-02-28T21:49:30Z

Adds support for modules, and increases the stinginess w.r.t. whitespace in the generated code.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

fabiomadge · 2022-02-28T23:03:33Z

Source/Dafny/Compilers/Compiler.cs

@@ -1194,6 +1196,8 @@ public enum ResolvedUnaryOp { BoolNot, BitwiseNot, Cardinality }
            var w = DeclareDatatype(dt, wr);
            if (w != null) {
              CompileClassMembers(program, dt, w);
+            } else if (this is not CppCompiler) {


The alternative is living with a \n when there's a tuple. I personally don't like either.

Could this be an attribute of each of the compilers that the main code checks to decide whether to add the \n?

This code is a little strange, we always add a \n in L1161 for every TopLevelDecl that's compiled. Sometimes we only find out later that we don't have to do anything. This leaves unsightly whitespace in the generated sources. Looking it is no fun.

The concrete problem here is a hack in the cpp compiler. They include the ClassMembers on the first pass, so they can't have the second one. To avoid that, they act like they didn't do anything.

Sounds like we can still define an attribute, even if it's a weird name like CompilesClassMembersOnTheFirstPass or whatever. :)

Referring to concrete subclasses here is just a recipe for weird hard-to-debug edge cases as we add more compilers.

Now, it's this one field we happen to overwrite in this one compiler.

cpitclaudel · 2022-02-28T23:09:18Z

Source/Dafny/Compilers/Compiler.cs

@@ -1238,8 +1242,10 @@ public enum ResolvedUnaryOp { BoolNot, BitwiseNot, Cardinality }
            }
          } else if (d is ValuetypeDecl) {
            // nop
+            wr.DeleteLast();


That's a bit scary: are we sure that we know which character this will be deleting?

Reasonably so, the test go trough after all. At least in this case it should be.

I agree this is very risky and makes the code an order of magnitude harder to reason about confidently. I'd define whatever additional Compiler attributes you need to specialize the behavior without doing this.

I hesitate to even mention it, but IF this was absolutely necessary, I would at least provide an argument to DeleteLast to specify WHAT you expect to be deleted, so at least you have a chance of catching bugs if the state is ever not what you thought it would be.

I think it's reasonably nice now.

robin-aws

Thanks for starting to tackle the confusing labelling on the BraceStyle enum!

robin-aws · 2022-03-01T22:58:59Z

Source/Dafny/Compilers/Compiler-python.cs

+          compiledName = IdProtect((string)idParam);
+          break;
+        default:
+          Contract.Assert(false); // unexpected ID


I'd prefer throwing an exception instead. Contract.Assert is turned off for release builds, and we don't the chance of a user hitting this case and failing in a weird way elsewhere because of the default "" value.

This is a very common pattern in our code base and all the other implementations of GetSpecialFieldInfo do it this way, but I can change it if you feel strongly about it. I'd argue that a user will notice it at the very latest when their generated code doesn't compile.

Okay, I'll let it go for now. I'll consider this something we should clean up when we address #1390 more generally.

robin-aws · 2022-03-01T23:03:57Z

Source/Dafny/ConcreteSyntax/ConcreteSyntaxTree.cs

@@ -7,10 +7,11 @@

 namespace Microsoft.Dafny {
  public enum BraceStyle {


Since you're already touching most of the references to this type, I think the time is right to fix the name and call it BlockStyle instead. That will resolve the weird redundancy in BraceStyle.Brace and just plain contradiction in BraceStyle.NewlineNoBrace (which would just become BlockStyle.Newline).

I think then Space would also be renamed to SpaceBrace?

robin-aws · 2022-03-01T23:12:23Z

Source/Dafny/Compilers/Compiler.cs

@@ -1194,6 +1196,8 @@ public enum ResolvedUnaryOp { BoolNot, BitwiseNot, Cardinality }
            var w = DeclareDatatype(dt, wr);
            if (w != null) {
              CompileClassMembers(program, dt, w);
+            } else if (this is not CppCompiler) {


Sounds like we can still define an attribute, even if it's a weird name like CompilesClassMembersOnTheFirstPass or whatever. :)

Referring to concrete subclasses here is just a recipe for weird hard-to-debug edge cases as we add more compilers.

robin-aws · 2022-03-01T23:15:27Z

Source/Dafny/Compilers/Compiler.cs

@@ -1238,8 +1242,10 @@ public enum ResolvedUnaryOp { BoolNot, BitwiseNot, Cardinality }
            }
          } else if (d is ValuetypeDecl) {
            // nop
+            wr.DeleteLast();


I agree this is very risky and makes the code an order of magnitude harder to reason about confidently. I'd define whatever additional Compiler attributes you need to specialize the behavior without doing this.

I hesitate to even mention it, but IF this was absolutely necessary, I would at least provide an argument to DeleteLast to specify WHAT you expect to be deleted, so at least you have a chance of catching bugs if the state is ever not what you thought it would be.

robin-aws · 2022-03-01T23:19:24Z

Source/Dafny/Compilers/Compiler-python.cs


-      var customReceiver = !forBodyInheritance && NeedsCustomReceiver(m);


Did all of this disappear because customReceiver is never true in our test cases so far?

Great, I'm definitely in favour of removing code with no testing coverage (assuming it's not easy to add a test instead).

robin-aws

Much better, thanks for the improvements! Just the one small tweak and then LGTM.

robin-aws · 2022-03-02T18:47:20Z

Source/Dafny/Compilers/Compiler-python.cs

+          compiledName = IdProtect((string)idParam);
+          break;
+        default:
+          Contract.Assert(false); // unexpected ID


Okay, I'll let it go for now. I'll consider this something we should clean up when we address #1390 more generally.

robin-aws · 2022-03-02T18:48:30Z

Source/Dafny/Compilers/Compiler.cs

    protected abstract ConcreteSyntaxTree CreateIterator(IteratorDecl iter, ConcreteSyntaxTree wr);
    /// <summary>
    /// Returns an IClassWriter that can be used to write additional members. If "dt" is already written
    /// in the DafnyRuntime.targetlanguage file, then returns "null".
    /// </summary>
    protected abstract IClassWriter/*?*/ DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxTree wr);
+    protected virtual bool DatatypeDeclarationAndMemberCompilationAreSeparate => true;


Much better name than my suggestion :)

robin-aws · 2022-03-02T18:48:58Z

Source/Dafny/ConcreteSyntax/ConcreteSyntaxTree.cs

@@ -114,6 +115,12 @@ public T Append<T>(T node)
      return this;
    }

+    public void DeleteLast() {


Very glad we don't need this any more. Now let's remove the method so no one is tempted by the dark side in the future. :)

robin-aws · 2022-03-02T18:49:16Z

Source/Dafny/ConcreteSyntax/ConcreteSyntaxTree.cs

-  public enum BraceStyle {
+  public enum BlockStyle {
    Nothing,
-    Space,
    Newline,
-    NewlineNoBrace
+    Brace,
+    SpaceBrace,
+    NewlineBrace
  }


SO much better, thank you!

improve module support

f4c5136

fabiomadge requested a review from robin-aws February 28, 2022 21:49

fabiomadge added 3 commits February 28, 2022 22:52

Merge branch 'master' into python_modules

c6e78ab

add test

27d3650

work around to some shady bahavior in the cpp compiler

53470ac

fabiomadge commented Feb 28, 2022

View reviewed changes

cpitclaudel reviewed Feb 28, 2022

View reviewed changes

robin-aws requested changes Mar 1, 2022

View reviewed changes

fabiomadge added 3 commits March 2, 2022 14:16

review

b73e7b1

new names

6bf70a5

Merge branch 'master' into python_modules

ac0beee

fabiomadge requested a review from robin-aws March 2, 2022 13:30

fabiomadge added 2 commits March 2, 2022 14:54

fix those names

c9d5254

Merge branch 'master' into python_modules

4a30621

robin-aws requested changes Mar 2, 2022

View reviewed changes

delete deleteLast

3f2d8d7

robin-aws approved these changes Mar 2, 2022

View reviewed changes

fabiomadge enabled auto-merge (squash) March 2, 2022 19:01

fabiomadge added 2 commits March 2, 2022 20:35

Merge branch 'master' into python_modules

4c35497

Merge branch 'master' into python_modules

9a287b6

fabiomadge merged commit af985e8 into dafny-lang:master Mar 3, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Modules in the python backend #1871

feat: Modules in the python backend #1871

fabiomadge commented Feb 28, 2022 •

edited

Loading

fabiomadge Feb 28, 2022

cpitclaudel Feb 28, 2022

fabiomadge Feb 28, 2022

robin-aws Mar 1, 2022

fabiomadge Mar 2, 2022

cpitclaudel Feb 28, 2022

fabiomadge Feb 28, 2022

robin-aws Mar 1, 2022

fabiomadge Mar 2, 2022

robin-aws left a comment

robin-aws Mar 1, 2022

fabiomadge Mar 2, 2022

robin-aws Mar 2, 2022

robin-aws Mar 1, 2022

robin-aws Mar 1, 2022

robin-aws Mar 1, 2022

robin-aws Mar 1, 2022

fabiomadge Mar 1, 2022

robin-aws Mar 2, 2022

robin-aws left a comment

robin-aws Mar 2, 2022

robin-aws Mar 2, 2022

robin-aws Mar 2, 2022

robin-aws Mar 2, 2022

		@@ -7,10 +7,11 @@

		namespace Microsoft.Dafny {
		public enum BraceStyle {


		var customReceiver = !forBodyInheritance && NeedsCustomReceiver(m);

feat: Modules in the python backend #1871

feat: Modules in the python backend #1871

Conversation

fabiomadge commented Feb 28, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fabiomadge commented Feb 28, 2022 •

edited

Loading