feat: Add returns, ifs, and blocks to the python compiler

[fabiomadge]

(Also fixes the retry logic added a short while back in #1835)

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

[fabiomadge]

# Dafny program 3_Calls-As.dfy compiled into Python
from typing import Callable

class _dafny:
    def print(value):
        if type(value) == bool:
            print("true" if value else "false", end="")
        else:
            print(value, end="")

class _System:
  class nat:
    def Default():
      return int(0)

class _module:
  class _default:
    def A0(x, y):
      return

    def A1(x, y):
      a: int = int(0)
      a = a
      return a

    def A2(x, y):
      a: int = int(0)
      b: bool = False
      _rhs0: int = a
      _rhs1: bool = b
      a = _rhs0
      b = _rhs1
      return a, b

    def A3(x, y):
      a: int = int(0)
      b: bool = False
      c: int = int(0)
      _39_u: int = int(0)
      if (x) == (3):
        _39_u = c
      elif (x) == (4):
        _39_u = (c) + (0)
      elif True:
        _39_u = ((c) + (0)) + (0)
      _39_u = (1) * (_39_u)
      if True:
        _40_y: int
        _40_y = 65
        _39_u = (0) + (_39_u)
      _rhs2: int = a
      _rhs3: bool = b
      _rhs4: int = _39_u
      a = _rhs2
      b = _rhs3
      c = _rhs4
      return a, b, c

    def Main():
      _41_a: int = int(0)
      _42_b: int = int(0)
      _43_c: bool = False
      _44_d: int = int(0)
      _45_e: bool = False
      _46_f: int = int(0)
      _module._default.A0(2, False)
      _out0: int
      _out0 = _module._default.A1(2, False)
      _41_a = _out0
      _out1: int
      _out2: bool
      _out1, _out2 = _module._default.A2(2, False)
      _42_b = _out1
      _43_c = _out2
      _out3: int
      _out4: bool
      _out5: int
      _out3, _out4, _out5 = _module._default.A3(2, False)
      _44_d = _out3
      _45_e = _out4
      _46_f = _out5
      _dafny.print(_41_a)
      _dafny.print(" ")
      _dafny.print(_42_b)
      _dafny.print(" ")
      _dafny.print(_43_c)
      _dafny.print(" ")
      _dafny.print(_44_d)
      _dafny.print(" ")
      _dafny.print(_45_e)
      _dafny.print(" ")
      _dafny.print(_46_f)
      _dafny.print("\n")


_module._default.Main()

Admittedly not generated on this branch, but the result should be close.

[MikaelMayer]

Great, the python compiler is taking shape !

[MikaelMayer]

Good catch !

[MikaelMayer]

Not necessarily this PR, but next time could you consider moving this to a switch expression that returns a nullable string, and if the string returned is null, it calls the default case? It might simplify all these case and breaks.

[fabiomadge]

That would be nice for the moment, but I have every reason to expect that well will need to set one of the other out variables (L618-L625) eventually.

[fabiomadge]

I'll keep it in mind for when we get closer to a stable version of this method.