Too many nested parentheses syntax error in Python

Dafny version

4.1.0

Code to produce this issue

method Main() {
    var c := 1;
    print(c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c
          + c + c + c + c + c + c + c), "\n";
}

Command to run and resulting output

% dafny run -t:py src/Scratch.dfy                          

Dafny program verifier finished with 0 verified, 0 errors
Traceback (most recent call last):
  File "/Users/salkeldr/Documents/GitHub/libraries/src/Scratch-py/Scratch.py", line 7, in <module>
    import module_
  File "/Users/salkeldr/Documents/GitHub/libraries/src/Scratch-py/module_.py", line 23
    _dafny.print(_dafny.string_of((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((d_0_c_) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)) + (d_0_c_)))
                                                                                                                                                                                                                                        ^
SyntaxError: too many nested parentheses

What happened?

See above

What type of operating system are you experiencing the problem on?

Mac

Based on above, it doesn't seem particularly possible to fix this issue with the current model of compiling. The current compilers enforce expression trees by liberal use of parentheses, which makes the generated code robust to things like operator precedence differences between languages, but also seems to create a gargantuan number of parentheses in the generated code.

Unless I'm mistaken, given that Python apparently just has a depth limit for brackets/parentheses, it would seem a redesign of, at least, the Python compiler would be necessary. After some noodling, a much-easier-said-than-done solution would be to use the fact that Python provides the ast module or the existence of LibCST to, instead, translate the Dafny AST/CST to the Python equivalent, then use existing means to generate the Python code from the resulting syntax tree.

My mentioned course of action would be a fairly large undertaking, but I think it might be a good way towards a more robust Dafny -> Python compiler (perhaps illuminating opportunities for other languages) and improving the adoption potential of Dafny into larger Python projects. For a shorter-term workaround, I think it might be better to raise an error during the compilation process rather than letting the invalid code to be generated. Thoughts?

dafny-lang / dafny