Fix literal pattern bug

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -3655,15 +3655,14 @@ public class CodeCoverage {
 
  var litExpression = MatchFlattener.GetLiteralExpressionFromPattern(pattern);
  if (litExpression != null) {
-
  var thenWriter = EmitIf(out var guardWriter, false, writer);
- guardWriter.Write(sourceName);
- // CompileBinOp(BinaryExpr.ResolvedOpcode.EqCommon, sourceType, sourceType, pattern.Tok, Type.Bool,
- // out var opString, out var _, out var _, out var _, out var _,
- // out var _, out var _, out var _, out var _,
- // writer);
- guardWriter.Write(" == ");
- EmitExpr(litExpression, false, guardWriter, 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.Ctor == null) {

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

@@ -272,70 +272,8 @@ public abstract partial class SinglePassCodeGenerator {
  } else if (expr is TypeTestExpr typeTestExpr) {
  CompileTypeTest(typeTestExpr, inLetExprBody, wr, ref wStmts);
 
- } else if (expr is BinaryExpr) {
- var e = (BinaryExpr)expr;
-
- if (IsComparisonToZero(e, out var arg, out var sign, out var negated) &&
- CompareZeroUsingSign(arg.Type)) {
- // Transform e.g. x < BigInteger.Zero into x.Sign == -1
- var w = EmitSign(arg.Type, wr);
- TrParenExpr(arg, w, inLetExprBody, wStmts);
- wr.Write(negated ? " != " : " == ");
- wr.Write(sign.ToString());
- } else {
- CompileBinOp(e.ResolvedOp, e.E0.Type, e.E1.Type, e.tok, expr.Type.GetRuntimeType(),
- out var opString,
- out var preOpString,
- out var postOpString,
- out var callString,
- out var staticCallString,
- out var reverseArguments,
- out var truncateResult,
- out var convertE1_to_int,
- out var coerceE1,
- wr);
-
- if (truncateResult && e.Type.NormalizeToAncestorType().AsBitVectorType is { } bitvectorType) {
- wr = EmitBitvectorTruncation(bitvectorType, e.Type.AsNativeType(), true, wr);
- }
-
- var e0 = reverseArguments ? e.E1 : e.E0;
- var e1 = reverseArguments ? e.E0 : e.E1;
-
- var left = Expr(e0, inLetExprBody, wStmts);
- ConcreteSyntaxTree right;
- if (convertE1_to_int) {
- right = ExprAsNativeInt(e1, inLetExprBody, wStmts);
- } else {
- right = Expr(e1, inLetExprBody, wStmts);
- if (coerceE1) {
- right = CoercionIfNecessary(e1.Type, TypeForCoercion(e1.Type), e1.tok, right);
- }
- }
-
- 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.InParens()} {opString} {right.InParens()}");
- if (needsCast) {
- opResult = Cast(new LineSegment(nativeName), opResult);
- }
-
- wr.Append(opResult);
- } else if (callString != null) {
- wr.Format($"{left.InParens()}.{callString}({right})");
- } else if (staticCallString != null) {
- wr.Format($"{staticCallString}({left}, {right})");
- }
-
- wr.Write(postOpString);
- }
+ } else if (expr is BinaryExpr binary) {
+ EmitBinaryExpr(inLetExprBody, wr, wStmts, binary);
  } else if (expr is TernaryExpr) {
  Contract.Assume(false); // currently, none of the ternary expressions is compilable
 
@@ -616,6 +554,79 @@ public abstract partial class SinglePassCodeGenerator {
  }
  }
 
+ private void EmitBinaryExpr(bool inLetExprBody, ConcreteSyntaxTree wr,
+ ConcreteSyntaxTree wStmts, BinaryExpr binary)
+ {
+ if (IsComparisonToZero(binary, out var arg, out var sign, out var negated) &&
+ CompareZeroUsingSign(arg.Type)) {
+ // Transform e.g. x < BigInteger.Zero into x.Sign == -1
+ var w = EmitSign(arg.Type, wr);
+ TrParenExpr(arg, w, inLetExprBody, wStmts);
+ wr.Write(negated ? " != " : " == ");
+ wr.Write(sign.ToString());
+ } else {
+ CompileBinOp(binary.ResolvedOp, binary.E0.Type, binary.E1.Type, binary.tok, binary.Type.GetRuntimeType(),
+ out var opString,
+ out var preOpString,
+ out var postOpString,
+ out var callString,
+ out var staticCallString,
+ out var reverseArguments,
+ out var truncateResult,
+ out var convertE1_to_int,
+ out var coerceE1,
+ wr);
+
+ if (truncateResult && binary.Type.NormalizeToAncestorType().AsBitVectorType is { } bitvectorType) {
+ wr = EmitBitvectorTruncation(bitvectorType, binary.Type.AsNativeType(), true, wr);
+ }
+
+ var e0 = reverseArguments ? binary.E1 : binary.E0;
+ var e1 = reverseArguments ? binary.E0 : binary.E1;
+
+ var left = Expr(e0, inLetExprBody, wStmts);
+ ConcreteSyntaxTree right;
+ if (convertE1_to_int) {
+ right = ExprAsNativeInt(e1, inLetExprBody, wStmts);
+ } else {
+ right = Expr(e1, inLetExprBody, wStmts);
+ if (coerceE1) {
+ right = CoercionIfNecessary(e1.Type, TypeForCoercion(e1.Type), e1.tok, right);
+ }
+ }
+
+ EmitBinaryExprUsingConcreteSyntax(wr, binary.Type, preOpString, opString, left, right, callString, staticCallString, postOpString);
+ }
+ }
+
+ protected void EmitBinaryExprUsingConcreteSyntax(ConcreteSyntaxTree wr, Type resultType, string preOpString,
+ string opString, ICanRender left, ICanRender right, string callString, string staticCallString,
+ string postOpString)
+ {
+ wr.Write(preOpString);
+ if (opString != null) {
+ var nativeType = AsNativeType(resultType);
+ string nativeName = null;
+ bool needsCast = false;
+ if (nativeType != null) {
+ GetNativeInfo(nativeType.Sel, out nativeName, out _, out needsCast);
+ }
+
+ var opResult = ConcreteSyntaxTree.Create($"{left.InParens()} {opString} {right.InParens()}");
+ if (needsCast) {
+ opResult = Cast(new LineSegment(nativeName), opResult);
+ }
+
+ wr.Append(opResult);
+ } else if (callString != null) {
+ wr.Format($"{left.InParens()}.{callString}({right})");
+ } else if (staticCallString != null) {
+ wr.Format($"{staticCallString}({left}, {right})");
+ }
+
+ wr.Write(postOpString);
+ }
+
  private void EmitMatchExpr(MatchExpr e, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
  // ((System.Func<SourceType, TargetType>)((SourceType _source) => {
  // if (source.is_Ctor0) {

Source/DafnyCore/ConcreteSyntax/ConcreteSyntaxTree.cs

@@ -15,6 +15,12 @@ public enum BlockStyle {
  NewlineBrace
  }
 
+ public static class CanRenderExtensions {
+ public static ConcreteSyntaxTree InParens(this ICanRender canRender) {
+ return ConcreteSyntaxTree.Create($"({canRender})");
+ }
+ }
+
  public class ConcreteSyntaxTree : ICanRender {
  public ConcreteSyntaxTree(int relativeIndent = 0) {
  RelativeIndentLevel = relativeIndent;
@@ -152,10 +158,6 @@ public T Append<T>(T node)
  return this;
  }
 
- public ConcreteSyntaxTree InParens() {
- return Create($"({this})");
- }
-
  // ----- Nested blocks ------------------------------
 
  public virtual ConcreteSyntaxTree ForkInParens() {

Source/DafnyCore/GeneratedFromDafny/DCOMP.cs

@@ -2081,7 +2081,7 @@ public void GenExprLiteral(DAST._IExpression e, Std.Wrappers._IOption<Dafny.ISeq
  DAST._ILiteral _h150 = _source61.dtor_Literal_i_a0;
  if (_h150.is_BoolLiteral) {
  bool _h200 = _h150.dtor_BoolLiteral_i_a0;
- if (_h200 == false) {
+ if ((_h200) == (false)) {
  unmatched61 = false;
  {
  RAST._IExpr _out140;
@@ -2101,7 +2101,7 @@ public void GenExprLiteral(DAST._IExpression e, Std.Wrappers._IOption<Dafny.ISeq
  DAST._ILiteral _h151 = _source61.dtor_Literal_i_a0;
  if (_h151.is_BoolLiteral) {
  bool _h201 = _h151.dtor_BoolLiteral_i_a0;
- if (_h201 == true) {
+ if ((_h201) == (true)) {
  unmatched61 = false;
  {
  RAST._IExpr _out142;
@@ -2339,9 +2339,9 @@ public void GenExprBinary(DAST._IExpression e, Std.Wrappers._IOption<Dafny.ISequ
  if (unmatched66) {
  if (_source66.is_Eq) {
  bool referential0 = _source66.dtor_referential;
- if (referential0 == true) {
+ if ((referential0) == (true)) {
  bool nullable0 = _source66.dtor_nullable;
- if (nullable0 == false) {
+ if ((nullable0) == (false)) {
  unmatched66 = false;
  return true;
  }