Do not flatten matches for C#

[keyboardDrummer]

Description

Do not flatten matches for C#. Such flattening can cause the generated code size to be the square of the input code size. Removing the flattening leads to a huge decrease in the size of the generated C# code inside the Dafny codebase. It goes from ~14K lines to ~7K.

The compilation of nested matches is done as follows:

datatype TX = X(x1arg: TY, x2arg: TY)
datatype TY = Y(yarg: int)
datatype TZ = Z(zarg: TW)
datatype TW = W(warg: int)

method M(a: TX) {
  match a
    case X(Y(b),Z(W(c)) => <body1>
    case r => <body2>
}

Is roughly compiled into

// Same datatypes

method M(a: TX) {
  var unmatched := true;
  if (unmatched && a is X) {
    var x1arg1 = ((X)a).1;
    if (x1 is Y) {
      var b = ((Y)x1arg1).1;
      var x2arg2 := ((X)a).2; 
      if (x2 is Z) {
        var zarg1 := ((Z)x2arg2).1;
        if (x4 is W) {
          var c := ((W)zarg1).1;
          unmatched := false;
          <body1>
        }
      } 
    }
  }
  if (unmatched) {
    var r := a;
    <body2>
  }
}

Caveats

Maintainability

The approach taken to compile unflattened matches is one that could be applied generally, across all compilers, but it was slightly simpler to only apply it to C#, so I've done that for now.

Ideally the transformation would be a Dafny-to-Dafny source transformation, instead of a customization of SinglePassCompiler. However, Dafny does not allow using statements in expression contexts, and this is needed for the transformation. I think it would be good to have an intermediate Dafny that does allow this, similar to what @cpitclaudel 's Dafny-in-Dafny compiler allowed, and then to define the rewrite that this PR introduces using a Dafny source translation.

Improvement

For C# we could generate much nicer code, since C# allows declaring new variables inside expressions using x is T xAsType expressions. We could get rid of the nested if statements and the unmatched variable. However, I'll leave this for future work.

How has this been tested?

• Performance change. No additional tests added.

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

[keyboardDrummer]

Closing in favor of #5528