feat: Various small improvements to Python code generation

[fabiomadge]

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

[robin-aws]

Still thinking through the changes necessary to support let expressions, but in the meantime here are a couple of comments.

[robin-aws]

This could just be set(self) couldn't it? It just has to be something compatible with whatever CreateForeachLoop emits (i.e. anything iterable).

[fabiomadge]

It doesn't really matter here, but I think it's the type dafny assumes.

[robin-aws]

UniqueElements is just something that needs to be called in the target language, it doesn't have to produce a "Dafny value" at this level of abstraction. Just set(self) will work because it will only be used to compile something like this:

var mySet := set x | x in mySeq

To something like this in Python:

mySet = _dafny.Set()
for x in mySeq.UniqueElements:  // <- produced by PythonCompiler.CreateForEachLoop
  mySet.add(x)

What you've got is correct too, since _dafny.Seq is also iterable, I'm just trying to save us an extra object creation. :)

[fabiomadge]

It will undoubtedly work for python(see it doesn’t matter here) and given that this is only used immediately in comprehensions, like you described, it doesn’t matter in general. That being said, I do like the cleaner interface of returning a sequence, but your overhead argument is compelling, so I’ll adopt it.

[robin-aws]

Thanks! It's purely an optimization, and normally I wouldn't prioritize it at this stage, but this is a really easy one. :)

[robin-aws]

frall - intentional to avoid name conflict or typo? :)

[fabiomadge]

It's what Java, C#, and JS call it, but I don't deeply care.

[robin-aws]

The testing coverage for this is implicitly in Hello.dfy, I assume, which only worked before because we were just emitting a base Python string?

[fabiomadge]

Yes, we weren't doing anything with the strings other than passing them around, so it was fine.

[robin-aws]

For the record this version is definitely incomplete, since any value of type seq<char> is a string according to Dafny, even if it isn't a literal. Here's a test case we should add for the next step:

method Main() {
  var manualString := ['H', 'e', 'l', 'l', 'o'];
  print manualString;  // Still prints "Hello" and not "['H', 'e', 'l', 'l', 'o']"
}

[fabiomadge]

Good point, I'll try to add it in this one.

[robin-aws]

Nah, let's leave it for the next step. We'll need a more general implementation of a type descriptor anyway (for dynamic type checks like is), better to do that properly in a separate PR.

[robin-aws]

Just noting for the record that as I'm better appreciating our solution so far for TargetLambdasRestrictedToExpressions, I definitely see more speed bumps down the road for edge cases we don't handle correctly, because we're not doing this "post hoc clean up" for every possible method call that might need it. I won't likely see an immediate alternative and don't want to block this proven progress, but I do want to revisit before we go too much further.

[fabiomadge]

Yes, those changes are unlikely to be comprehensive, but I was hesitant to introduce additional untested changes.

[robin-aws]

🚀

[fabiomadge]

Do compilers do April fools' day?

[robin-aws]

Oh if we're going to do that, we should do it in the verifier instead. :)

[robin-aws]

Approved on the condition that the next PR adds a beefy comment on TargetLambdasRestrictedToExpressions about how we're using wStmts and why we have to conditionally add return statements in the SinglePassCompiler superclass. :)