Move towards a return value based style for our code generating methods

[keyboardDrummer]

The methods in Dafny's code generating back-ends often use side-effects to emit generated code.

And example is the method TrExpr:

void TrExpr(Expression expr, ConcreteSyntaxTree wr, bool inLetExprBody, ConcreteSyntaxTree wStmts) 

Instead of returning a value, it writes its output to ConcreteSyntaxTree wr.

The goal of this PR is not to make a particular code change, but to hopefully convince the reader that we should stop promoting the above side-effect style, and instead promote a more pure style, in which TrExpr looks like:

ConcreteSyntaxTree Expr(Expression expr, bool inLetExprBody, ConcreteSyntaxTree wStmts) 

There's two advantages to the more pure style, one is readability and the other is reusability.

Readability

This side-effect style sometimes leads to hard to read code, such as:

if (opString != null) {
  var nativeType = AsNativeType(e.Type);
  string nativeName = null, literalSuffix = null;
  bool needsCast = false;
  if (nativeType != null) {
    GetNativeInfo(nativeType.Sel, out nativeName, out literalSuffix, out needsCast);
  }

  var inner = wr;
  if (needsCast) {
    inner = wr.Write("(" + nativeName + ")").ForkInParens();
  }
  inner.Write(preOpString);
  TrParenExpr(e0, inner, inLetExprBody, wStmts);
  inner.Write(" {0} ", opString);
  if (convertE1_to_int) {
    EmitExprAsNativeInt(e1, inLetExprBody, inner, wStmts);
  } else {
    TrParenExpr(e1, inner, inLetExprBody, wStmts);
  }
  wr.Write(postOpString);
} else if (callString != null) {
  wr.Write(preOpString);
  TrParenExpr(e0, wr, inLetExprBody, wStmts);
  wr.Write(".{0}(", callString);
  if (convertE1_to_int) {
    EmitExprAsNativeInt(e1, inLetExprBody, wr, wStmts);
  } else {
    TrParenExpr(e1, wr, inLetExprBody, wStmts);
  }
  wr.Write(")");
  wr.Write(postOpString);
} else if (staticCallString != null) {
  wr.Write(preOpString);
  wr.Write("{0}(", staticCallString);
  TrExpr(e0, wr, inLetExprBody, wStmts);
  wr.Write(", ");
  TrExpr(e1, wr, inLetExprBody, wStmts);
  wr.Write(")");
  wr.Write(postOpString);
}

The pure style is much shorter and easier to read:

var left = Expr(e0, inLetExprBody, wStmts);
var right = convertE1_to_int 
  ? ExprAsNativeInt(e1, inLetExprBody, wStmts) 
  : Expr(e1, inLetExprBody, wStmts);

wr.Write(preOpString);
if (opString != null) {
  var nativeType = AsNativeType(e.Type);
  string nativeName = null;
  bool needsCast = false;
  if (nativeType != null) {
    GetNativeInfo(nativeType.Sel, out nativeName, out _, out needsCast);
  }

  var opResult = ConcreteSyntaxTree.Create($"{left} {opString} {right}");
  if (needsCast) {
    opResult = Cast(new LineSegment(nativeName), opResult);
  }

  wr.Append(opResult);
} else if (callString != null) {
  wr.Format($"{left}.{callString}({right})");
} else if (staticCallString != null) {
  wr.Format($"{staticCallString}({left}, {right})");
}
wr.Write(postOpString);

Commit 01b1416 and 0e7e0b8 show examples of how the pure style can look nicer than the side-effect one.

Reusability

The side-effect style of compilation is problematic when trying to generalise the code so it can be used to create an AST.

To construct an AST we want to be able to write code such as:

PythonBinaryExpr Binary(BinaryExpr binary) {
  var left = Expr(binary);
  var right = Expr(binary)
  return new PythonBinaryExpr(left, right, ...);
}

Note that we're using an Expr method that returns a value. If instead we had used a method TrExpr that writes its results to some store, we would have needed code like the following to produce an AST, which is hard to read and write:

void Binary(BinaryExpr binary, Stack<PythonExpresion> results) {
  TrExpr(binary, results);
  TrExpr(binary, results)
  results.Push(new PythonBinaryExpr(results.Pop(), results.Pop(), ...);
}

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

[jtristan]

I'm very supportive of this idea. Perhaps we should get a second opinion from either @fabiomadge or @RustanLeino who have more experience with the compiler and may be better equipped to foresee practical issues with this proposal? Regardless, we ought to be able to make it work, and it would be beneficial.