Emit less nested target code #4683
Conversation
There was a problem hiding this comment.
Great progress, and I love how simple the actual change is. Are you correcting any cases of accidentally failing to provide the right values to recursive calls, as opposed to intentionally being conservative? If so is there anything we can do to the signatures to make that less likely in the future?
There was a problem hiding this comment.
I think this is a case where we actually want to assert something about the structure of the code we're emitting. Otherwise we could regress and the test would still pass, but perhaps take 30 mins to pass, which we might not notice in CI. :)
You could add an additional LIT command that uses our support for %OutputCheck to apply a CHECK-NOT regex to the Java code we emit to say the nested structure doesn't appear.
| @@ -2740,7 +2740,7 @@ void TrCasePatternOpt<VT>(CasePattern<VT> pat, Expression rhs, Action<ConcreteSy | |||
| } | |||
| } | |||
|
|
|||
| void TrExprOpt(Expression expr, Type resultType, ConcreteSyntaxTree wr, IVariable/*?*/ accumulatorVar) { | |||
| void TrExprOpt(Expression expr, Type resultType, ConcreteSyntaxTree wr, bool inLetExprBody, [CanBeNull] IVariable accumulatorVar) { | |||
There was a problem hiding this comment.
I think this and TrCaseExpressionOpt deserve a short comment about what optimizations they are applying and when they are valid. AFAICT it's something like "parallel optimized implementations for when we are translating the return value of a function, and hence can do things like compile chains of LetExprs into sequences of statements"
| /// <summary> | ||
| /// This method compiles "expr" into a statement context of the target. This typically means that, for example, Dafny let-bound variables can | ||
| /// be compiled into local variables in the target code, and that Dafny if-then-else expressions can be compiled into if statements in the | ||
| /// target code. | ||
| /// In contrast, the "Expr(...)" method compiles its given expression into an expression context of the target. This can result in | ||
| /// more complicated constructions in target languages that don't support name bindings in expressions (like most of our target | ||
| /// languages) or that don't support if-then-else expressions (like Go). | ||
| /// Other than the syntactic differences in the target code, the idea is that "TrExprOpt(...)" and "Expr(...)" generate code with the | ||
| /// same semantics. | ||
| /// </summary> |
Emit better target code for match-case expressions. In particular, avoid some deeply nested IIFE's that (were hard for a human to read and) caused the Java compiler to choke.
Fixes #3868
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.