Optimize compilation of functional-looking assignment RHSs

.gitignore

@@ -84,3 +84,7 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/**/*.html
 Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.dtr
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary-lib
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary.doo
+Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.deps.json
+Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.csproj
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule2
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/PythonModule1

Source/DafnyCore/AST/Members/Function.cs

@@ -96,6 +96,19 @@ public TailStatus
  public readonly Formal Result;
  public PreType ResultPreType;
  public readonly Type ResultType;
+ public Type OriginalResultTypeWithRenamings() {
+ if (OverriddenFunction == null) {
+ return ResultType;
+ }
+
+ Contract.Assert(TypeArgs.Count == OverriddenFunction.TypeArgs.Count);
+ var renamings = new Dictionary<TypeParameter, Type>();
+ for (var i = 0; i < TypeArgs.Count; i++) {
+ renamings.Add(OverriddenFunction.TypeArgs[i], new UserDefinedType(tok, TypeArgs[i]));
+ }
+ return OverriddenFunction.ResultType.Subst(renamings);
+
+ }
  public Expression Body; // an extended expression; Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution
  public IToken /*?*/ ByMethodTok; // null iff ByMethodBody is null
  public BlockStmt /*?*/ ByMethodBody;

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -2975,8 +2975,8 @@ protected override void EmitNestedMatchExpr(NestedMatchExpr match, bool inLetExp
  }
 
  protected override void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts,
- bool inLetExprBody, IVariable accumulatorVar) {
- TrExprOpt(match.Flattened, resultType, wr, wStmts, inLetExprBody, accumulatorVar);
+ bool inLetExprBody, IVariable accumulatorVar, OptimizedExpressionContinuation continuation) {
+ TrExprOpt(match.Flattened, resultType, wr, wStmts, inLetExprBody, accumulatorVar, continuation);
  }
 
  protected override void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -1985,14 +1985,6 @@ protected override void EmitReturn(List<Formal> outParams, ConcreteSyntaxTree wr
  EmitReturnWithCoercions(outParams, null, null, wr);
  }
 
- protected override void EmitReturnExpr(Expression expr, Type resultType, bool inLetExprBody, ConcreteSyntaxTree wr) {
- var wStmts = wr.Fork();
- var w = EmitReturnExpr(wr);
- var fromType = thisContext == null ? expr.Type : expr.Type.Subst(thisContext.ParentFormalTypeParametersToActuals);
- w = EmitCoercionIfNecessary(fromType, resultType, expr.tok, w);
- w.Append(Expr(expr, inLetExprBody, wStmts));
- }
-
  protected void EmitReturnWithCoercions(List<Formal> outParams, List<Formal>/*?*/ overriddenOutParams, Dictionary<TypeParameter, Type>/*?*/ typeMap, ConcreteSyntaxTree wr) {
  wr.Write("return");
  var sep = " ";
@@ -2488,10 +2480,6 @@ private string IdName(Declaration decl) {
 
  protected override string PrefixForForcedCapitalization => "Go_";
 
- public override Type ResultTypeAsViewedByFunctionBody(Function f) {
- return f.Original.ResultType;
- }
-
  protected override string IdMemberName(MemberSelectExpr mse) {
  return Capitalize(mse.MemberName);
  }

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -3606,6 +3606,10 @@ protected override void EmitAbsurd(string message, ConcreteSyntaxTree wr) {
  message = "unexpected control point";
  }
 
+ // Wrapping an "if (true) { ... }" around the "break" statement is a way to tell the Java compiler not to give
+ // errors for any (unreachable) code that may follow. 
+ wr = EmitIf(out var guardWriter, false, wr);
+ guardWriter.Write("true");
  wr.WriteLine($"throw new IllegalArgumentException(\"{message}\");");
  }
 
@@ -4369,16 +4373,28 @@ protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageV
 
  protected override void EmitNestedMatchExpr(NestedMatchExpr match, bool inLetExprBody, ConcreteSyntaxTree output,
  ConcreteSyntaxTree wStmts) {
- EmitExpr(match.Flattened, inLetExprBody, output, wStmts);
+ if (match.Cases.Count == 0) {
+ base.EmitNestedMatchExpr(match, inLetExprBody, output, wStmts);
+ } else {
+ EmitExpr(match.Flattened, inLetExprBody, output, wStmts);
+ }
  }
 
  protected override void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts,
- bool inLetExprBody, IVariable accumulatorVar) {
- TrExprOpt(match.Flattened, resultType, wr, wStmts, inLetExprBody, accumulatorVar);
+ bool inLetExprBody, IVariable accumulatorVar, OptimizedExpressionContinuation continuation) {
+ if (match.Cases.Count == 0) {
+ base.TrOptNestedMatchExpr(match, resultType, wr, wStmts, inLetExprBody, accumulatorVar, continuation);
+ } else {
+ TrExprOpt(match.Flattened, resultType, wr, wStmts, inLetExprBody, accumulatorVar, continuation);
+ }
  }
 
  protected override void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {
- TrStmt(match.Flattened, writer);
+ if (match.Cases.Count == 0) {
+ base.EmitNestedMatchStmt(match, writer);
+ } else {
+ TrStmt(match.Flattened, writer);
+ }
  }
  }
 }

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs

@@ -704,7 +704,8 @@ private void EmitMatchExpr(MatchExpr e, bool inLetExprBody, ConcreteSyntaxTree w
  var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand();
  foreach (MatchCaseExpr mc in e.Cases) {
  var wCase = MatchCasePrelude(source, sourceType, mc.Ctor, mc.Arguments, i, e.Cases.Count, w);
- TrExprOpt(mc.Body, mc.Body.Type, wCase, wStmts, inLetExprBody: true, accumulatorVar: null);
+ var continuation = new OptimizedExpressionContinuation(EmitReturnExpr, false);
+ TrExprOpt(mc.Body, mc.Body.Type, wCase, wStmts, inLetExprBody: true, accumulatorVar: null, continuation);
  i++;
  }
  }
@@ -715,18 +716,19 @@ private void EmitMatchExpr(MatchExpr e, bool inLetExprBody, ConcreteSyntaxTree w
 
  protected virtual void EmitNestedMatchExpr(NestedMatchExpr match, bool inLetExprBody, ConcreteSyntaxTree output, ConcreteSyntaxTree wStmts) {
  var lambdaBody = EmitAppliedLambda(output, wStmts, match.Tok, match.Type);
- TrOptNestedMatchExpr(match, match.Type, lambdaBody, wStmts, inLetExprBody, null);
+ var continuation = new OptimizedExpressionContinuation(EmitReturnExpr, false);
+ TrOptNestedMatchExpr(match, match.Type, lambdaBody, wStmts, inLetExprBody, null, continuation);
  }
 
  protected virtual void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultType, ConcreteSyntaxTree wr,
- ConcreteSyntaxTree wStmts, bool inLetExprBody, IVariable accumulatorVar) {
+ ConcreteSyntaxTree wStmts, bool inLetExprBody, IVariable accumulatorVar, OptimizedExpressionContinuation continuation) {
 
  wStmts = wr.Fork();
 
- EmitNestedMatchGeneric(match, (caseIndex, caseBody) => {
+ EmitNestedMatchGeneric(match, continuation.PreventCaseFallThrough, (caseIndex, caseBody) => {
  var myCase = match.Cases[caseIndex];
- TrExprOpt(myCase.Body, myCase.Body.Type, caseBody, wStmts, inLetExprBody: true, accumulatorVar: null);
- }, wr, true);
+ TrExprOpt(myCase.Body, myCase.Body.Type, caseBody, wStmts, inLetExprBody, accumulatorVar: null, continuation);
+ }, inLetExprBody, wr);
  }
 
  private ConcreteSyntaxTree EmitAppliedLambda(ConcreteSyntaxTree output, ConcreteSyntaxTree wStmts,

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs

@@ -116,13 +116,25 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
  if (Options.ForbidNondeterminism) {
  Error(ErrorId.c_nondeterminism_forbidden, s.Rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr);
  }
- } else if (s.Rhs is ExprRhs eRhs && eRhs.Expr.Resolved is FunctionCallExpr fce && IsTailRecursiveByMethodCall(fce)) {
- TrTailCallStmt(s.Tok, fce.Function.ByMethodDecl, fce.Receiver, fce.Args, null, wr);
- } else {
+ } else if (s.Rhs is TypeRhs typeRhs) {
  var lvalue = CreateLvalue(s.Lhs, wr, wStmts);
  wStmts = wr.Fork();
- var wRhs = EmitAssignment(lvalue, TypeOfLhs(s.Lhs), TypeOfRhs(s.Rhs), wr, assignStmt.Tok);
- TrRhs(s.Rhs, wRhs, wStmts);
+ var wRhs = EmitAssignment(lvalue, TypeOfLhs(s.Lhs), TypeOfRhs(typeRhs), wr, assignStmt.Tok);
+ TrRhs(typeRhs, wRhs, wStmts);
+ } else {
+ var eRhs = (ExprRhs)s.Rhs;
+ if (eRhs.Expr.Resolved is FunctionCallExpr fce && IsTailRecursiveByMethodCall(fce)) {
+ TrTailCallStmt(s.Tok, fce.Function.ByMethodDecl, fce.Receiver, fce.Args, wr);
+ } else {
+ var lvalue = CreateLvalue(s.Lhs, wr, wStmts);
+ var doAssignment = (Expression e, Type resultType, bool inLetExprBody, ConcreteSyntaxTree wrAssignment) => {
+ var wStmtsBeforeAssignment = wrAssignment.Fork();
+ var wRhs = EmitAssignment(lvalue, resultType, e.Type, wrAssignment, assignStmt.Tok);
+ EmitExpr(e, false, wRhs, wStmtsBeforeAssignment);
+ };
+ var continuation = new OptimizedExpressionContinuation(doAssignment, true);
+ TrExprOpt(eRhs.Expr, TypeOfLhs(s.Lhs), wr, wStmts, false, null, continuation);
+ }
  }
 
  break;
@@ -511,78 +523,91 @@ private void EmitMatchStmt(ConcreteSyntaxTree wr, MatchStmt s) {
  }
 
  protected virtual void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {
- EmitNestedMatchGeneric(match, (caseIndex, caseBody) => {
+ EmitNestedMatchGeneric(match, true, (caseIndex, caseBody) => {
  TrStmtList(match.Cases[caseIndex].Body, caseBody);
- }, writer, false);
+ }, false, writer);
  }
 
  /// <summary>
- ///
- /// match a
+ /// Given
+ /// 
+ /// match a
  /// case X(Y(b),Z(W(c)) => body1
  /// case r => body2
+ /// 
+ /// If there are no cases, then emit:
+ ///
+ /// throw ABSURD;
  ///
- /// var unmatched = true;
- /// if (unmatched && a is X) {
- /// var x1 = ((X)a).1;
- /// if (x1 is Y) {
- /// var b = ((Y)x1).1;
+ /// Else, emit:
  /// 
- /// var x2 = ((X)a).2; 
- /// if (x2 is Z) {
- /// var x4 = ((Z)x2).1;
- /// if (x4 is W) {
- /// var c = ((W)x4).1;
- /// body1;
+ /// BLOCK {
+ /// { // this defines the scope for any new local variables in the case
+ /// if (a is X) {
+ /// var x0 = ((X)a).0;
+ /// if (x0 is Y) {
+ /// var b = ((Y)x0).0;
+ /// 
+ /// var x1 = ((X)a).1; 
+ /// if (x1 is Z) {
+ /// var xz0 = ((Z)x1).0;
+ /// if (xz0 is W) {
+ /// var c = ((W)xz0).0;
+ /// 
+ /// body1;
+ /// break BLOCK;
+ /// }
+ /// }
  /// }
- /// } 
+ /// }
+ /// 
+ /// {
+ /// var r = a;
+ /// body2;
+ /// }
  /// }
- /// }
- /// if (unmatched) {
- /// var r = a;
- /// body2;
- /// }
  /// 
  /// </summary>
- private void EmitNestedMatchGeneric(INestedMatch match, Action<int, ConcreteSyntaxTree> emitBody,
- ConcreteSyntaxTree output, bool bodyExpected) {
+ private void EmitNestedMatchGeneric(INestedMatch match, bool preventCaseFallThrough, Action<int, ConcreteSyntaxTree> emitBody,
+ bool inLetExprBody, ConcreteSyntaxTree output) {
  if (match.Cases.Count == 0) {
- if (bodyExpected) {
- // the verifier would have proved we never get here; still, we need some code that will compile
- EmitAbsurd(null, output);
- }
+ // the verifier would have proved we never get here; still, we need some code that will compile
+ EmitAbsurd(null, output);
  } else {
  string sourceName = ProtectedFreshId("_source");
- DeclareLocalVar(sourceName, match.Source.Type, match.Source.tok, match.Source, false, output);
+ DeclareLocalVar(sourceName, match.Source.Type, match.Source.tok, match.Source, inLetExprBody, output);
 
- string unmatched = ProtectedFreshId("unmatched");
- DeclareLocalVar(unmatched, Type.Bool, match.Source.Tok, Expression.CreateBoolLiteral(match.Source.Tok, true), false, output);
+ var label = preventCaseFallThrough ? ProtectedFreshId("match") : null;
+ if (label != null) {
+ output = CreateLabeledCode(label, false, output);
+ }
 
  var sourceType = match.Source.Type.NormalizeExpand();
  for (var index = 0; index < match.Cases.Count; index++) {
  var myCase = match.Cases[index];
  var lastCase = index == match.Cases.Count - 1;
- var result = EmitIf(out var guardWriter, false, output);
- guardWriter.Write(unmatched);
- var innerWriter = EmitNestedMatchCaseConditions(sourceName, sourceType, myCase.Pat, result, lastCase);
+
+ var caseBlock = EmitBlock(output);
+ var innerWriter = EmitNestedMatchCaseConditions(sourceName, sourceType, myCase.Pat, caseBlock, lastCase);
  Coverage.Instrument(myCase.Tok, "case body", innerWriter);
- EmitAssignment(unmatched, Type.Bool, False, Type.Bool, innerWriter);
 
  emitBody(index, innerWriter);
- }
-
- if (bodyExpected) {
- EmitAbsurd(null, output);
+ if (label != null && !lastCase) {
+ EmitBreak(label, innerWriter);
+ }
  }
  }
  }
 
- private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName,
- Type sourceType,
+ private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName, Type sourceType,
  ExtendedPattern pattern, ConcreteSyntaxTree writer, bool lastCase) {
 
  var litExpression = MatchFlattener.GetLiteralExpressionFromPattern(pattern);
  if (litExpression != null) {
+ if (lastCase) {
+ return writer;
+ }
+
  var thenWriter = EmitIf(out var guardWriter, false, writer);
  CompileBinOp(BinaryExpr.ResolvedOpcode.EqCommon, sourceType, litExpression.Type, pattern.Tok, Type.Bool,
  out var opString, out var preOpString, out var postOpString, out var callString, out var staticCallString,
@@ -591,22 +616,25 @@ private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName,
  var right = new ConcreteSyntaxTree();
  EmitExpr(litExpression, false, right, writer);
  EmitBinaryExprUsingConcreteSyntax(guardWriter, Type.Bool, preOpString, opString, new LineSegment(sourceName), right, callString, staticCallString, postOpString);
- writer = thenWriter;
+ return thenWriter;
+
  } else if (pattern is IdPattern idPattern) {
- if (idPattern.BoundVar != null) {
- var boundVar = idPattern.BoundVar;
- if (boundVar.Tok.val.StartsWith(IdPattern.WildcardString)) {
- return writer;
- }
+ if (idPattern.BoundVar == null) {
+ return EmitNestedMatchStmtCaseConstructor(sourceName, sourceType, idPattern, writer, lastCase);
+ }
 
+ var boundVar = idPattern.BoundVar;
+ if (!boundVar.Tok.val.StartsWith(IdPattern.WildcardString)) {
  var valueWriter = DeclareLocalVar(IdName(boundVar), boundVar.Type, idPattern.Tok, writer);
  valueWriter.Write(sourceName);
- return writer;
- } else {
- writer = EmitNestedMatchStmtCaseConstructor(sourceName, sourceType, idPattern, writer, lastCase);
  }
+ return writer;
 
  } else if (pattern is DisjunctivePattern disjunctivePattern) {
+ if (lastCase) {
+ return writer;
+ }
+
  string disjunctiveMatch = ProtectedFreshId("disjunctiveMatch");
  DeclareLocalVar(disjunctiveMatch, Type.Bool, disjunctivePattern.Tok, Expression.CreateBoolLiteral(disjunctivePattern.Tok, false), false, writer);
  foreach (var alternative in disjunctivePattern.Alternatives) {
@@ -615,11 +643,11 @@ private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName,
  }
  writer = EmitIf(out var guardWriter, false, writer);
  guardWriter.Write(disjunctiveMatch);
+ return writer;
+
  } else {
  throw new Exception();
  }
-
- return writer;
  }
 
  private ConcreteSyntaxTree EmitNestedMatchStmtCaseConstructor(string sourceName, Type sourceType,