Dafny IR contains singleton tuples when compiling pair with ghost

[dnezam]

Dafny version

4.7.0

Code to produce this issue

method Main() {
  print ("ab", ghost "ab"), "\n";
}

Command to run and resulting output

[Module (Name "_module") [] F
       (SOME
          [ModuleItem_Class
             (Class (Name "__default") (Ident (Name "_module")) [] [] []
                [ClassItem_Method
                   (Method T T F F NONE (Name "Main") [] []
                      [Print
                         (Expression_Tuple [Literal (StringLiteral "ab" F)]);
                       Print (Literal (StringLiteral "\\n" F)); EarlyReturn]
                      [] (SOME []))] [])])]

What happened?

After updating to the changes on the feat-rust-externs-subsets-eta-names-tests branch #5613 the Dafny IR seems to contain 1 tuples, even though it did not in the past (around https://github.com/dnezam/dafny/tree/141053d202b4619b742927d4ae646b62b5864218)

Since singleton tuples are not supported by Dafny (nor CakeML), and weren't generated before, I would have assumed that this does not occur.

Additionally, even if these should be implemented as Tuples, this would create inconsistencies when trying to print (ab vs (ab)).

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

Linux

[MikaelMayer]

Thanks for reporting. Please note that the Dafny IR is in development, not stable and is heavily subject to change.

[MikaelMayer]

I need to say as well that, despite my comment above, I don't expect any overhaul change in the near future as we almost have everything needed for the Dafny-to-Rust compiler so far. Perhaps we will add a few types there and there.

Originally, the Dafny AST was meant to be printed back to Dafny. However, in the current architecture, it resembles more an IR as you are saying than an AST, as it contains some low-level routines such as collection initializers and builders.

How much are these 1-tuple impacting you? I want to see how I can mitigate possible refactoring of that AST in the future.

[dnezam]

Thanks for the reply!

1-tuples wouldn't be difficult to deal with, since CakeML support them AFAIK. The only "issue" that I can currently think of is that printing them might be a bit inconsistent (dafny run would print it as x, while the current CakeML compiler would print it as (x)), but that wouldn't be difficult to deal with.

TL;DR: I don't think 1-tuples impact the CakeML compiler too much; once it is decided how to print them/whether to generate them it should be straightforward to deal with it on our side.