Attempt at using nested matches for all backends

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -3523,184 +3523,5 @@ public class CodeCoverage {
  }
 }");
  }
-
- protected override 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);
- }
-
- private ConcreteSyntaxTree EmitAppliedLambda(ConcreteSyntaxTree output, ConcreteSyntaxTree wStmts,
- IToken token, Type resultType) {
- EmitLambdaApply(output, out var lambdaApplyTarget, out _);
- return CreateLambda(new List<Type>(), token, new List<string>(), resultType, lambdaApplyTarget, wStmts);
- }
-
- protected override void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultType, ConcreteSyntaxTree wr,
- ConcreteSyntaxTree wStmts, bool inLetExprBody, IVariable accumulatorVar) {
-
- wStmts = wr.Fork();
-
- EmitNestedMatchGeneric(match, (caseIndex, caseBody) => {
- var myCase = match.Cases[caseIndex];
- TrExprOpt(myCase.Body, myCase.Body.Type, caseBody, wStmts, inLetExprBody: true, accumulatorVar: null);
- }, wr, true);
- }
-
- protected override void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {
- EmitNestedMatchGeneric(match, (caseIndex, caseBody) => {
- TrStmtList(match.Cases[caseIndex].Body, caseBody);
- }, writer, false);
- }
-
- /// <summary>
- ///
- /// match a
- /// case X(Y(b),Z(W(c)) => body1
- /// case r => body2
- ///
- /// var unmatched = true;
- /// if (unmatched && a is X) {
- /// var x1 = ((X)a).1;
- /// if (x1 is Y) {
- /// var b = ((Y)x1).1;
- /// 
- /// var x2 = ((X)a).2; 
- /// if (x2 is Z) {
- /// var x4 = ((Z)x2).1;
- /// if (x4 is W) {
- /// var c = ((W)x4).1;
- /// body1;
- /// }
- /// } 
- /// }
- /// }
- /// if (unmatched) {
- /// var r = a;
- /// body2;
- /// }
- /// 
- /// </summary>
- private void EmitNestedMatchGeneric(INestedMatch match, Action<int, ConcreteSyntaxTree> emitBody,
- ConcreteSyntaxTree output, bool bodyExpected) {
- 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);
- }
- } else {
- string sourceName = ProtectedFreshId("_source");
- DeclareLocalVar(sourceName, match.Source.Type, match.Source.tok, match.Source, false, output);
-
- string unmatched = ProtectedFreshId("unmatched");
- DeclareLocalVar(unmatched, Type.Bool, match.Source.Tok, Expression.CreateBoolLiteral(match.Source.Tok, true), 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);
- Coverage.Instrument(myCase.Tok, "case body", innerWriter);
- EmitAssignment(unmatched, Type.Bool, False, Type.Bool, innerWriter);
-
- emitBody(index, innerWriter);
- }
-
- if (bodyExpected) {
- EmitAbsurd(null, output);
- }
- }
- }
-
- private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName,
- Type sourceType,
- ExtendedPattern pattern, ConcreteSyntaxTree writer, bool lastCase) {
-
- var litExpression = MatchFlattener.GetLiteralExpressionFromPattern(pattern);
- if (litExpression != null) {
- 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,
- out _, out _, out _, out _,
- writer);
- var right = new ConcreteSyntaxTree();
- EmitExpr(litExpression, false, right, writer);
- EmitBinaryExprUsingConcreteSyntax(guardWriter, Type.Bool, preOpString, opString, new LineSegment(sourceName), right, callString, staticCallString, postOpString);
- writer = thenWriter;
- } else if (pattern is IdPattern idPattern) {
- if (idPattern.BoundVar != null) {
- var boundVar = idPattern.BoundVar;
- var valueWriter = DeclareLocalVar(IdName(boundVar), boundVar.Type, idPattern.Tok, writer);
- valueWriter.Write(sourceName);
- return writer;
- } else {
- writer = EmitNestedMatchStmtCaseConstructor(sourceName, sourceType, idPattern, writer, lastCase);
- }
-
- } else if (pattern is DisjunctivePattern disjunctivePattern) {
- string disjunctiveMatch = ProtectedFreshId("disjunctiveMatch");
- DeclareLocalVar(disjunctiveMatch, Type.Bool, disjunctivePattern.Tok, Expression.CreateBoolLiteral(disjunctivePattern.Tok, false), false, writer);
- foreach (var alternative in disjunctivePattern.Alternatives) {
- var alternativeWriter = EmitNestedMatchCaseConditions(sourceName, sourceType, alternative, writer, lastCase);
- EmitAssignment(disjunctiveMatch, Type.Bool, True, Type.Bool, alternativeWriter);
- }
- writer = EmitIf(out var guardWriter, false, writer);
- guardWriter.Write(disjunctiveMatch);
- } else {
- throw new Exception();
- }
-
- return writer;
- }
-
- private ConcreteSyntaxTree EmitNestedMatchStmtCaseConstructor(string sourceName, Type sourceType,
- IdPattern idPattern,
- ConcreteSyntaxTree result, bool lastCase) {
- var ctor = idPattern.Ctor;
-
- if (!lastCase && ctor.EnclosingDatatype.Ctors.Count != 1) {
- result = EmitIf(out var guardWriter, false, result);
- EmitConstructorCheck(sourceName, ctor, guardWriter);
- }
-
- var userDefinedType = (UserDefinedType)sourceType.NormalizeExpand();
-
- var typeSubstMap =
- TypeParameter.SubstitutionMap(userDefinedType.ResolvedClass.TypeArgs, userDefinedType.TypeArgs);
- int nonGhostIndex = 0; // number of processed non-ghost arguments
- for (int index = 0; index < ctor.Formals.Count; index++) {
- var arg = ctor.Formals[index];
-
- if (arg.IsGhost) {
- continue;
- }
-
- var type = arg.Type.Subst(typeSubstMap);
- // ((Dt_Ctor0)source._D).a0;
- var destructor = new ConcreteSyntaxTree();
- EmitDestructor(wr => EmitIdentifier(sourceName, wr), arg, nonGhostIndex, ctor,
- () => SelectNonGhost(userDefinedType.ResolvedClass, userDefinedType.TypeArgs), type, destructor);
-
- if (idPattern.Arguments != null) {
- string newSourceName;
- var childPattern = idPattern.Arguments[index];
- if (childPattern is IdPattern { BoundVar: not null } childIdPattern) {
- var boundVar = childIdPattern.BoundVar;
- newSourceName = IdName(boundVar);
- var valueWriter = DeclareLocalVar(newSourceName, boundVar.Type, idPattern.Tok, result);
- valueWriter.Append(destructor);
- } else {
- newSourceName = ProtectedFreshId(arg.CompileName);
- var valueWriter = DeclareLocalVar(newSourceName, type, idPattern.Tok, result);
- valueWriter.Append(destructor);
- result = EmitNestedMatchCaseConditions(newSourceName, type, childPattern, result, lastCase);
- }
- }
- nonGhostIndex++;
- }
-
- return result;
- }
  }
 }

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

@@ -707,11 +707,26 @@ public abstract partial class SinglePassCodeGenerator {
  EmitExpr(e.Source, inLetExprBody, wArg, wStmts);
  }
 
- protected virtual void EmitNestedMatchExpr(NestedMatchExpr match, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
- EmitExpr(match.Flattened, inLetExprBody, wr, wStmts);
+ 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);
  }
- protected virtual void TrOptNestedMatchExpr(NestedMatchExpr nestedMatchExpr, Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts, bool inLetExprBody, IVariable accumulatorVar) {
- TrExprOpt(nestedMatchExpr.Flattened, resultType, wr, wStmts, inLetExprBody, accumulatorVar);
+
+ protected virtual void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultType, ConcreteSyntaxTree wr,
+ ConcreteSyntaxTree wStmts, bool inLetExprBody, IVariable accumulatorVar) {
+
+ wStmts = wr.Fork();
+
+ EmitNestedMatchGeneric(match, (caseIndex, caseBody) => {
+ var myCase = match.Cases[caseIndex];
+ TrExprOpt(myCase.Body, myCase.Body.Type, caseBody, wStmts, inLetExprBody: true, accumulatorVar: null);
+ }, wr, true);
+ }
+
+ private ConcreteSyntaxTree EmitAppliedLambda(ConcreteSyntaxTree output, ConcreteSyntaxTree wStmts,
+ IToken token, Type resultType) {
+ EmitLambdaApply(output, out var lambdaApplyTarget, out _);
+ return CreateLambda(new List<Type>(), token, new List<string>(), resultType, lambdaApplyTarget, wStmts);
  }
  }
 }

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

@@ -513,7 +513,160 @@ public abstract partial class SinglePassCodeGenerator {
  }
 
  protected virtual void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {
- TrStmt(match.Flattened, writer);
+ EmitNestedMatchGeneric(match, (caseIndex, caseBody) => {
+ TrStmtList(match.Cases[caseIndex].Body, caseBody);
+ }, writer, false);
+ }
+
+ /// <summary>
+ ///
+ /// match a
+ /// case X(Y(b),Z(W(c)) => body1
+ /// case r => body2
+ ///
+ /// var unmatched = true;
+ /// if (unmatched && a is X) {
+ /// var x1 = ((X)a).1;
+ /// if (x1 is Y) {
+ /// var b = ((Y)x1).1;
+ /// 
+ /// var x2 = ((X)a).2; 
+ /// if (x2 is Z) {
+ /// var x4 = ((Z)x2).1;
+ /// if (x4 is W) {
+ /// var c = ((W)x4).1;
+ /// body1;
+ /// }
+ /// } 
+ /// }
+ /// }
+ /// if (unmatched) {
+ /// var r = a;
+ /// body2;
+ /// }
+ /// 
+ /// </summary>
+ private void EmitNestedMatchGeneric(INestedMatch match, Action<int, ConcreteSyntaxTree> emitBody,
+ ConcreteSyntaxTree output, bool bodyExpected) {
+ 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);
+ }
+ } else {
+ string sourceName = ProtectedFreshId("_source");
+ DeclareLocalVar(sourceName, match.Source.Type, match.Source.tok, match.Source, false, output);
+
+ string unmatched = ProtectedFreshId("unmatched");
+ DeclareLocalVar(unmatched, Type.Bool, match.Source.Tok, Expression.CreateBoolLiteral(match.Source.Tok, true), 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);
+ Coverage.Instrument(myCase.Tok, "case body", innerWriter);
+ EmitAssignment(unmatched, Type.Bool, False, Type.Bool, innerWriter);
+
+ emitBody(index, innerWriter);
+ }
+
+ if (bodyExpected) {
+ EmitAbsurd(null, output);
+ }
+ }
+ }
+
+ private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName,
+ Type sourceType,
+ ExtendedPattern pattern, ConcreteSyntaxTree writer, bool lastCase) {
+
+ var litExpression = MatchFlattener.GetLiteralExpressionFromPattern(pattern);
+ if (litExpression != null) {
+ 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,
+ out _, out _, out _, out _,
+ writer);
+ var right = new ConcreteSyntaxTree();
+ EmitExpr(litExpression, false, right, writer);
+ EmitBinaryExprUsingConcreteSyntax(guardWriter, Type.Bool, preOpString, opString, new LineSegment(sourceName), right, callString, staticCallString, postOpString);
+ writer = thenWriter;
+ } else if (pattern is IdPattern idPattern) {
+ if (idPattern.BoundVar != null) {
+ var boundVar = idPattern.BoundVar;
+ var valueWriter = DeclareLocalVar(IdName(boundVar), boundVar.Type, idPattern.Tok, writer);
+ valueWriter.Write(sourceName);
+ return writer;
+ } else {
+ writer = EmitNestedMatchStmtCaseConstructor(sourceName, sourceType, idPattern, writer, lastCase);
+ }
+
+ } else if (pattern is DisjunctivePattern disjunctivePattern) {
+ string disjunctiveMatch = ProtectedFreshId("disjunctiveMatch");
+ DeclareLocalVar(disjunctiveMatch, Type.Bool, disjunctivePattern.Tok, Expression.CreateBoolLiteral(disjunctivePattern.Tok, false), false, writer);
+ foreach (var alternative in disjunctivePattern.Alternatives) {
+ var alternativeWriter = EmitNestedMatchCaseConditions(sourceName, sourceType, alternative, writer, lastCase);
+ EmitAssignment(disjunctiveMatch, Type.Bool, True, Type.Bool, alternativeWriter);
+ }
+ writer = EmitIf(out var guardWriter, false, writer);
+ guardWriter.Write(disjunctiveMatch);
+ } else {
+ throw new Exception();
+ }
+
+ return writer;
+ }
+
+ private ConcreteSyntaxTree EmitNestedMatchStmtCaseConstructor(string sourceName, Type sourceType,
+ IdPattern idPattern,
+ ConcreteSyntaxTree result, bool lastCase) {
+ var ctor = idPattern.Ctor;
+
+ if (!lastCase && ctor.EnclosingDatatype.Ctors.Count != 1) {
+ result = EmitIf(out var guardWriter, false, result);
+ EmitConstructorCheck(sourceName, ctor, guardWriter);
+ }
+
+ var userDefinedType = (UserDefinedType)sourceType.NormalizeExpand();
+
+ var typeSubstMap =
+ TypeParameter.SubstitutionMap(userDefinedType.ResolvedClass.TypeArgs, userDefinedType.TypeArgs);
+ int nonGhostIndex = 0; // number of processed non-ghost arguments
+ for (int index = 0; index < ctor.Formals.Count; index++) {
+ var arg = ctor.Formals[index];
+
+ if (arg.IsGhost) {
+ continue;
+ }
+
+ var type = arg.Type.Subst(typeSubstMap);
+ // ((Dt_Ctor0)source._D).a0;
+ var destructor = new ConcreteSyntaxTree();
+ EmitDestructor(wr => EmitIdentifier(sourceName, wr), arg, nonGhostIndex, ctor,
+ () => SelectNonGhost(userDefinedType.ResolvedClass, userDefinedType.TypeArgs), type, destructor);
+
+ if (idPattern.Arguments != null) {
+ string newSourceName;
+ var childPattern = idPattern.Arguments[index];
+ if (childPattern is IdPattern { BoundVar: not null } childIdPattern) {
+ var boundVar = childIdPattern.BoundVar;
+ newSourceName = IdName(boundVar);
+ var valueWriter = DeclareLocalVar(newSourceName, boundVar.Type, idPattern.Tok, result);
+ valueWriter.Append(destructor);
+ } else {
+ newSourceName = ProtectedFreshId(arg.CompileName);
+ var valueWriter = DeclareLocalVar(newSourceName, type, idPattern.Tok, result);
+ valueWriter.Append(destructor);
+ result = EmitNestedMatchCaseConditions(newSourceName, type, childPattern, result, lastCase);
+ }
+ }
+ nonGhostIndex++;
+ }
+
+ return result;
  }
  }
 }