diff --git a/Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs b/Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs index df7aafbf22e..309207fa531 100644 --- a/Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs +++ b/Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs @@ -261,37 +261,39 @@ public void Print(DAST.Expression expr) { } public AssignBuilder Assign() { - var ret = new AssignBuilder(this, false, null); + var ret = new AssignBuilder(false, null); AddBuildable(ret); return ret; } public AssignBuilder DeclareAndAssign(DAST.Type type) { - var ret = new AssignBuilder(this, true, type); + var ret = new AssignBuilder(true, type); AddBuildable(ret); return ret; } public IfElseBuilder IfElse() { - var ret = new IfElseBuilder(this); + var ret = new IfElseBuilder(); AddBuildable(ret); return ret; } public WhileBuilder While() { - var ret = new WhileBuilder(this); + var ret = new WhileBuilder(); AddBuildable(ret); return ret; } - public CallStmtBuilder Call(object returnTo) { - var ret = new CallStmtBuilder(this, returnTo); + public CallStmtBuilder Call() { + var ret = new CallStmtBuilder(); AddBuildable(ret); return ret; } public ReturnBuilder Return() { - return new ReturnBuilder(this); + var ret = new ReturnBuilder(); + AddBuildable(ret); + return ret; } } @@ -320,14 +322,12 @@ public List ForkList() { } class AssignBuilder : ExprContainer, BuildableStatement { - public readonly StatementContainer parent; readonly bool isDeclare; readonly DAST.Type type; string name = null; - public DAST.Expression value; + public object value; - public AssignBuilder(StatementContainer parent, bool isDeclare, DAST.Type type) { - this.parent = parent; + public AssignBuilder(bool isDeclare, DAST.Type type) { this.isDeclare = isDeclare; this.type = type; } @@ -348,33 +348,41 @@ public void AddExpr(DAST.Expression value) { } } + public void AddBuildable(BuildableExpr value) { + if (this.value != null) { + throw new InvalidOperationException(); + } else { + this.value = value; + } + } + public DAST.Statement Build() { if (isDeclare) { if (this.value == null) { return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence.UnicodeFromString(name), type, DAST.Optional.create_None()); } else { - return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence.UnicodeFromString(name), type, DAST.Optional.create_Some(this.value)); + var builtValue = new List(); + ExprContainer.RecursivelyBuild(new List { value }, builtValue); + return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence.UnicodeFromString(name), type, DAST.Optional.create_Some(builtValue[0])); } } else { if (this.value == null) { throw new InvalidOperationException("Cannot assign null value to variable: " + name); } else { - return (DAST.Statement)DAST.Statement.create_Assign(Sequence.UnicodeFromString(name), value); + var builtValue = new List(); + ExprContainer.RecursivelyBuild(new List { value }, builtValue); + return (DAST.Statement)DAST.Statement.create_Assign(Sequence.UnicodeFromString(name), builtValue[0]); } } } } class IfElseBuilder : ExprContainer, StatementContainer, BuildableStatement { - public readonly StatementContainer parent; - - DAST.Expression condition = null; + object condition = null; readonly List ifBody = new(); readonly List elseBody = new(); - public IfElseBuilder(StatementContainer parent) { - this.parent = parent; - } + public IfElseBuilder() { } public void AddExpr(DAST.Expression value) { if (condition != null) { @@ -384,6 +392,14 @@ public void AddExpr(DAST.Expression value) { } } + public void AddBuildable(BuildableExpr value) { + if (condition != null) { + throw new InvalidOperationException(); + } else { + condition = value; + } + } + public void AddStatement(DAST.Statement item) { ifBody.Add(item); } @@ -417,6 +433,9 @@ public ElseBuilder Else() { } public DAST.Statement Build() { + List builtCondition = new(); + ExprContainer.RecursivelyBuild(new List { condition }, builtCondition); + List builtIfStatements = new(); StatementContainer.RecursivelyBuild(ifBody, builtIfStatements); @@ -424,7 +443,7 @@ public DAST.Statement Build() { StatementContainer.RecursivelyBuild(elseBody, builtElseStatements); return (DAST.Statement)DAST.Statement.create_If( - condition, + builtCondition[0], Sequence.FromArray(builtIfStatements.ToArray()), Sequence.FromArray(builtElseStatements.ToArray()) ); @@ -452,14 +471,10 @@ public void AddBuildable(BuildableStatement item) { } class WhileBuilder : ExprContainer, StatementContainer, BuildableStatement { - public readonly StatementContainer parent; - - DAST.Expression condition = null; + object condition = null; readonly List body = new(); - public WhileBuilder(StatementContainer parent) { - this.parent = parent; - } + public WhileBuilder() { } public void AddExpr(DAST.Expression value) { if (condition != null) { @@ -469,6 +484,14 @@ public void AddExpr(DAST.Expression value) { } } + public void AddBuildable(BuildableExpr value) { + if (condition != null) { + throw new InvalidOperationException(); + } else { + condition = value; + } + } + public void AddStatement(DAST.Statement item) { body.Add(item); } @@ -484,30 +507,27 @@ public List ForkList() { } public DAST.Statement Build() { + List builtCondition = new(); + ExprContainer.RecursivelyBuild(new List { condition }, builtCondition); + List builtStatements = new(); StatementContainer.RecursivelyBuild(body, builtStatements); return (DAST.Statement)DAST.Statement.create_While( - condition, + builtCondition[0], Sequence.FromArray(builtStatements.ToArray()) ); } } class CallStmtBuilder : ExprContainer, BuildableStatement { - public readonly StatementContainer parent; - public readonly object returnTo; - - DAST.Expression on = null; + object on = null; string name = null; List typeArgs = null; - readonly List args = new(); + readonly List args = new(); List> outs = null; - public CallStmtBuilder(StatementContainer parent, object returnTo) { - this.parent = parent; - this.returnTo = returnTo; - } + public CallStmtBuilder() { } public void SetName(string name) { if (this.name != null) { @@ -533,6 +553,14 @@ public void AddExpr(DAST.Expression value) { } } + public void AddBuildable(BuildableExpr value) { + if (on == null) { + on = value; + } else { + args.Add(value); + } + } + public void SetOuts(List> outs) { if (this.outs != null) { throw new InvalidOperationException(); @@ -542,37 +570,53 @@ public void SetOuts(List> outs) { } public DAST.Statement Build() { + List builtOn = new(); + ExprContainer.RecursivelyBuild(new List { on }, builtOn); + + List builtArgs = new(); + ExprContainer.RecursivelyBuild(args, builtArgs); + return (DAST.Statement)DAST.Statement.create_Call( - on, + builtOn[0], Sequence.UnicodeFromString(name), Sequence.FromArray(typeArgs.ToArray()), - Sequence.FromArray(args.ToArray()), + Sequence.FromArray(builtArgs.ToArray()), outs == null ? DAST.Optional>>.create_None() : DAST.Optional>>.create_Some(Sequence>.FromArray(outs.ToArray())) ); } } - class ReturnBuilder : ExprContainer { - readonly StatementContainer parent; + class ReturnBuilder : ExprContainer, BuildableStatement { + object value = null; - DAST.Expression value = null; + public ReturnBuilder() { } - public ReturnBuilder(StatementContainer parent) { - this.parent = parent; + public void AddExpr(DAST.Expression value) { + if (this.value != null) { + throw new InvalidOperationException(); + } else { + this.value = value; + } } - public void AddExpr(DAST.Expression value) { + public void AddBuildable(BuildableExpr value) { if (this.value != null) { throw new InvalidOperationException(); } else { this.value = value; - parent.AddStatement((DAST.Statement)DAST.Statement.create_Return(value)); } } + + public DAST.Statement Build() { + var builtValue = new List(); + ExprContainer.RecursivelyBuild(new List { value }, builtValue); + + return (DAST.Statement)DAST.Statement.create_Return(builtValue[0]); + } } class ExprBuffer : ExprContainer { - Stack exprs = new(); + Stack exprs = new(); public readonly object parent; public ExprBuffer(object returnTo) { @@ -583,15 +627,23 @@ public void AddExpr(DAST.Expression item) { exprs.Push(item); } + public void AddBuildable(BuildableExpr item) { + exprs.Push(item); + } + public List PopN(int n) { if (exprs.Count < n) { throw new InvalidOperationException(); } else { - var result = new List(); + var result = new List(); for (int i = 0; i < n; i++) { result.Insert(0, exprs.Pop()); } - return result; + + var builtResult = new List(); + ExprContainer.RecursivelyBuild(result, builtResult); + + return builtResult; } } @@ -603,7 +655,7 @@ public DAST.Expression Finish() { if (exprs.Count != 1) { throw new InvalidOperationException("Expected exactly one expression in buffer, got " + exprs.Comma(e => e.ToString())); } else { - return exprs.Pop(); + return PopN(1)[0]; } } } @@ -611,63 +663,72 @@ public DAST.Expression Finish() { interface ExprContainer { void AddExpr(DAST.Expression item); - BinOpBuilder BinOp(string op, DafnyCompiler compiler, object returnTo) { - return new BinOpBuilder(compiler, this, op, returnTo); + void AddBuildable(BuildableExpr item); + + BinOpBuilder BinOp(string op) { + var ret = new BinOpBuilder(op); + AddBuildable(ret); + return ret; } CallExprBuilder Call() { - return new CallExprBuilder(this); + var ret = new CallExprBuilder(); + AddBuildable(ret); + return ret; + } + + protected static void RecursivelyBuild(List body, List builtExprs) { + foreach (var maybeBuilt in body) { + if (maybeBuilt is DAST.Expression built) { + builtExprs.Add(built); + } else if (maybeBuilt is BuildableExpr buildable) { + builtExprs.Add(buildable.Build()); + } else { + throw new InvalidOperationException("Unknown buildable type: " + maybeBuilt.GetType()); + } + } } } - class BinOpBuilder : ExprContainer { - readonly DafnyCompiler compiler; - readonly ExprContainer parent; + interface BuildableExpr { + DAST.Expression Build(); + } + + class BinOpBuilder : ExprContainer, BuildableExpr { readonly string op; - readonly object returnTo; - DAST.Expression left = null; - DAST.Expression right = null; + readonly List operands = new(); - public BinOpBuilder(DafnyCompiler compiler, ExprContainer parent, string op, object returnTo) { - this.compiler = compiler; - this.parent = parent; + public BinOpBuilder(string op) { this.op = op; - this.returnTo = returnTo; } public void AddExpr(DAST.Expression item) { - if (left == null) { - left = item; - } else if (right == null) { - right = item; - if (compiler.currentBuilder == this) { - compiler.currentBuilder = this.returnTo; - this.Finish(); - } else { - throw new InvalidOperationException(); - } - } else { - throw new InvalidOperationException(); - } + operands.Add(item); } - public void Finish() { - parent.AddExpr((DAST.Expression)DAST.Expression.create_BinOp(Sequence.UnicodeFromString(op), left, right)); + public void AddBuildable(BuildableExpr item) { + operands.Add(item); } - } - class CallExprBuilder : ExprContainer { - public readonly ExprContainer parent; + public DAST.Expression Build() { + if (operands.Count != 2) { + throw new InvalidOperationException("Expected exactly two operands, got " + operands.Comma(o => o.ToString())); + } - DAST.Expression on = null; + var builtOperands = new List(); + ExprContainer.RecursivelyBuild(operands, builtOperands); + return (DAST.Expression)DAST.Expression.create_BinOp(Sequence.UnicodeFromString(op), builtOperands[0], builtOperands[1]); + } + } + + class CallExprBuilder : ExprContainer, BuildableExpr { + object on = null; string name = null; List typeArgs = null; - readonly List args = new(); + readonly List args = new(); List> outs = null; - public CallExprBuilder(ExprContainer parent) { - this.parent = parent; - } + public CallExprBuilder() { } public void SetName(string name) { if (this.name != null) { @@ -693,6 +754,14 @@ public void AddExpr(DAST.Expression value) { } } + public void AddBuildable(BuildableExpr value) { + if (on == null) { + on = value; + } else { + args.Add(value); + } + } + public void SetOuts(List> outs) { if (this.outs != null) { throw new InvalidOperationException(); @@ -701,15 +770,19 @@ public void SetOuts(List> outs) { } } - public object Finish() { - parent.AddExpr((DAST.Expression)DAST.Expression.create_Call( - on, + public DAST.Expression Build() { + var builtOn = new List(); + ExprContainer.RecursivelyBuild(new List { on }, builtOn); + + var builtArgs = new List(); + ExprContainer.RecursivelyBuild(args, builtArgs); + + return (DAST.Expression)DAST.Expression.create_Call( + builtOn[0], Sequence.UnicodeFromString(name), Sequence.FromArray(typeArgs.ToArray()), - Sequence.FromArray(args.ToArray()) - )); - - return parent; + Sequence.FromArray(builtArgs.ToArray()) + ); } } diff --git a/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs b/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs index a2f656ea3e5..5cb2e6791ce 100644 --- a/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs +++ b/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs @@ -5,8 +5,8 @@ using DAST; using System.Numerics; using Microsoft.BaseTypes; -using Microsoft.Boogie; using System.Linq; +using System.Diagnostics.Contracts; namespace Microsoft.Dafny.Compilers { @@ -231,7 +231,7 @@ private DAST.Type GenType(Type typ) { _ => throw new InvalidOperationException(), }); } else { - throw new NotImplementedException("Type name for " + typ); + throw new NotImplementedException("Type name for " + xType + " (" + typ.GetType() + ")"); } } @@ -485,8 +485,6 @@ protected override void DeclareLocalVar(string name, Type type, IToken tok, bool if (leaveRoomForRhs) { throw new InvalidOperationException(); - } else { - variable.AddExpr(null); } } else { if (bufferedInitializationValue == null) { @@ -537,7 +535,7 @@ protected override void EmitCallReturnOuts(List outTmps, ConcreteSyntaxT protected override void TrCallStmt(CallStmt s, string receiverReplacement, ConcreteSyntaxTree wr, ConcreteSyntaxTree wrStmts, ConcreteSyntaxTree wrStmtsAfterCall) { if (wr is BuilderSyntaxTree stmtContainer) { - var callBuilder = stmtContainer.Builder.Call(currentBuilder); + var callBuilder = stmtContainer.Builder.Call(); base.TrCallStmt(s, receiverReplacement, new BuilderSyntaxTree(callBuilder), wrStmts, wrStmtsAfterCall); } else { throw new InvalidOperationException("Cannot call statement in this context: " + currentBuilder); @@ -549,7 +547,6 @@ protected override void CompileFunctionCallExpr(FunctionCallExpr e, ConcreteSynt if (wr is BuilderSyntaxTree builder) { var callBuilder = builder.Builder.Call(); base.CompileFunctionCallExpr(e, new BuilderSyntaxTree(callBuilder), inLetExprBody, wStmts, tr); - callBuilder.Finish(); } else { throw new InvalidOperationException("Cannot call function in this context: " + currentBuilder); } @@ -659,23 +656,13 @@ protected override void EmitHalt(IToken tok, Expression messageExpr, ConcreteSyn throw new NotImplementedException(); } - private ElseBuilder builderForElse = null; + private readonly Stack elseBuilderStack = new(); protected override ConcreteSyntaxTree EmitIf(out ConcreteSyntaxTree guardWriter, bool hasElse, ConcreteSyntaxTree wr) { - if (builderForElse != null) { // else-if - var ifBuilder = ((StatementContainer)builderForElse).IfElse(); - builderForElse = null; - - if (hasElse) { - builderForElse = ifBuilder.Else(); - } - - guardWriter = new BuilderSyntaxTree(ifBuilder); - return new BuilderSyntaxTree(ifBuilder); - } else if (wr is BuilderSyntaxTree statementContainer) { + if (wr is BuilderSyntaxTree statementContainer) { var ifBuilder = statementContainer.Builder.IfElse(); if (hasElse) { - builderForElse = ifBuilder.Else(); + elseBuilderStack.Push(ifBuilder.Else()); } guardWriter = new BuilderSyntaxTree(ifBuilder); @@ -686,10 +673,8 @@ protected override ConcreteSyntaxTree EmitIf(out ConcreteSyntaxTree guardWriter, } protected override ConcreteSyntaxTree EmitBlock(ConcreteSyntaxTree wr) { - if (builderForElse != null) { - var ret = new BuilderSyntaxTree(builderForElse); - builderForElse = null; - return ret; + if (elseBuilderStack.Count > 0) { + return new BuilderSyntaxTree(elseBuilderStack.Pop()); } else { throw new NotImplementedException(); } @@ -920,7 +905,7 @@ private DAST.Type TypeNameASTFromTopLevel(TopLevelDecl topLevel, List type public override ConcreteSyntaxTree Expr(Expression expr, bool inLetExprBody, ConcreteSyntaxTree wStmts) { if (currentBuilder is ExprContainer container) { - base.EmitExpr(expr, inLetExprBody, new BuilderSyntaxTree(container), wStmts); + EmitExpr(expr, inLetExprBody, new BuilderSyntaxTree(container), wStmts); return new ConcreteSyntaxTree(); } else { throw new InvalidOperationException(); @@ -944,6 +929,10 @@ public override void EmitExpr(Expression expr, bool inLetExprBody, ConcreteSynta // sometimes, we don't actually call EmitDatatypeValue currentBuilder = origBuilder; } + } else if (expr is BinaryExpr) { + var origBuilder = currentBuilder; + base.EmitExpr(expr, inLetExprBody, actualWr, wStmts); + currentBuilder = origBuilder; } else { base.EmitExpr(expr, inLetExprBody, actualWr, wStmts); } @@ -997,7 +986,7 @@ protected override void EmitDatatypeValue(DatatypeValue dtv, string typeDescript )); } } else { - throw new InvalidOperationException("Cannot emit datatype value outside of expression context: " + wr.GetType()); + throw new InvalidOperationException("Cannot emit datatype value outside of expression context: " + wr.GetType() + ", " + currentBuilder); } } @@ -1114,7 +1103,26 @@ protected override ConcreteSyntaxTree EmitBetaRedex(List boundVars, List protected override void EmitDestructor(string source, Formal dtor, int formalNonGhostIndex, DatatypeCtor ctor, List typeArgs, Type bvType, ConcreteSyntaxTree wr) { - throw new NotImplementedException(); + if (wr is BuilderSyntaxTree builder) { + if (DatatypeWrapperEraser.IsErasableDatatypeWrapper(Options, ctor.EnclosingDatatype, out var coreDtor)) { + Contract.Assert(coreDtor.CorrespondingFormals.Count == 1); + Contract.Assert(dtor == coreDtor.CorrespondingFormals[0]); // any other destructor is a ghost + EmitIdentifier(source, wr); + } else { + if (ctor.EnclosingDatatype is TupleTypeDecl) { + builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_TupleSelect( + (DAST.Expression)DAST.Expression.create_Ident(Sequence.UnicodeFromString(source)), + int.Parse(dtor.NameForCompilation) + )); + } else { + builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_Select( + (DAST.Expression)DAST.Expression.create_Ident(Sequence.UnicodeFromString(source)), + Sequence.UnicodeFromString(dtor.CompileName), + true + )); + } + } + } } protected override bool TargetLambdasRestrictedToExpressions => true; @@ -1215,7 +1223,8 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op, _ => throw new NotImplementedException(), }; - currentBuilder = builder.Builder.BinOp(opString, this, currentBuilder); + currentBuilder = builder.Builder.BinOp(opString); + // cleaned up by EmitExpr } else { throw new InvalidOperationException(); } @@ -1251,6 +1260,18 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody, } } + protected override void EmitConstructorCheck(string source, DatatypeCtor ctor, ConcreteSyntaxTree wr) { + if (wr is BuilderSyntaxTree builder) { + builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_TypeTest( + DAST.Expression.create_Ident(Sequence.UnicodeFromString(source)), + PathFromTopLevel(ctor.EnclosingDatatype), + Sequence.UnicodeFromString(ctor.GetCompileName(Options)) + )); + } else { + throw new InvalidOperationException(); + } + } + protected override void EmitTypeTest(string localName, Type fromType, Type toType, IToken tok, ConcreteSyntaxTree wr) { throw new NotImplementedException(); } diff --git a/Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy index fd58af5f515..2ec6014d8f7 100644 --- a/Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy +++ b/Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy @@ -735,11 +735,12 @@ module {:extern "DCOMP"} DCOMP { } case TupleSelect(on, idx) => { var onString, _, recIdents := GenExpr(on, params, false); - s := onString + "." + natToString(idx); + s := "(" + onString + ")." + natToString(idx); if mustOwn { - s := s + ".clone()"; + s := "(" + s + ")" + ".clone()"; isOwned := true; } else { + s := "&" + s; isOwned := false; } readIdents := recIdents; diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs index 713ba68d498..5a6f661d521 100644 --- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs +++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs @@ -2627,11 +2627,11 @@ void TrCasePatternOpt(CasePattern pat, Expression rhs, ConcreteSyntaxTre TrCasePatternOpt(pat, rhs, null, rhs.Type, rhs.tok, wr, inLetExprBody); } - void TrCasePatternOpt(CasePattern pat, Expression rhs, string rhs_string, Type rhsType, IToken rhsTok, ConcreteSyntaxTree wr, bool inLetExprBody) + void TrCasePatternOpt(CasePattern pat, Expression rhs, Action emitRhs, Type rhsType, IToken rhsTok, ConcreteSyntaxTree wr, bool inLetExprBody) where VT : class, IVariable { Contract.Requires(pat != null); - Contract.Requires(pat.Var != null || rhs != null || rhs_string != null); - Contract.Requires(rhs != null || rhs_string != null); + Contract.Requires(pat.Var != null || rhs != null || emitRhs != null); + Contract.Requires(rhs != null || emitRhs != null); Contract.Requires(rhsType != null && rhsTok != null); if (pat.Var != null) { @@ -2647,7 +2647,7 @@ void TrCasePatternOpt(CasePattern pat, Expression rhs, string rhs_string w = EmitCoercionIfNecessary(from: rhs.Type, to: bv.Type, tok: rhsTok, wr: w); EmitExpr(rhs, inLetExprBody, w, wStmts); } else { - w.Write(rhs_string); + emitRhs(w); } } } else if (pat.Arguments != null) { @@ -2666,7 +2666,8 @@ void TrCasePatternOpt(CasePattern pat, Expression rhs, string rhs_string if (rhs != null) { DeclareLocalVar(tmp_name, rhs.Type, rhs.tok, rhs, inLetExprBody, wr); } else { - DeclareLocalVar(tmp_name, rhsType, rhsTok, false, rhs_string, wr); + var w = DeclareLocalVar(tmp_name, rhsType, rhsTok, wr); + emitRhs(w); } var dtv = (DatatypeValue)pat.Expr; @@ -2679,10 +2680,8 @@ void TrCasePatternOpt(CasePattern pat, Expression rhs, string rhs_string // nothing to compile, but do a sanity check Contract.Assert(Contract.ForAll(arg.Vars, bv => bv.IsGhost)); } else { - var sw = new ConcreteSyntaxTree(wr.RelativeIndentLevel); - EmitDestructor(tmp_name, formal, k, ctor, dtv.InferredTypeArgs, arg.Expr.Type, sw); Type targetType = formal.Type.Subst(substMap); - TrCasePatternOpt(arg, null, sw.ToString(), targetType, pat.Expr.tok, wr, inLetExprBody); + TrCasePatternOpt(arg, null, sw => EmitDestructor(tmp_name, formal, k, ctor, dtv.InferredTypeArgs, arg.Expr.Type, sw), targetType, pat.Expr.tok, wr, inLetExprBody); k++; } } @@ -4775,7 +4774,11 @@ ConcreteSyntaxTree MatchCasePrelude(string source, UserDefinedType sourceType, D // Need to avoid if (true) because some languages (Go, someday Java) // pretend that an if (true) isn't a certainty, leading to a complaint // about a missing return statement - w = EmitBlock(wr); + if (caseCount > 1) { + w = EmitBlock(wr); + } else { + w = wr; + } } else { w = EmitIf(out var guardWriter, !lastCase, wr); EmitConstructorCheck(source, ctor, guardWriter); diff --git a/Source/DafnyCore/GeneratedFromDafnyRust.cs b/Source/DafnyCore/GeneratedFromDafnyRust.cs index 7ec202f65f3..41b1eff6627 100644 --- a/Source/DafnyCore/GeneratedFromDafnyRust.cs +++ b/Source/DafnyCore/GeneratedFromDafnyRust.cs @@ -3093,11 +3093,9 @@ public COMP() { } else { Dafny.ISequence _72___mcc_h6 = _source1.dtor_TypeArg_a0; Dafny.ISequence _source4 = _72___mcc_h6; - { - Dafny.ISequence _73___mcc_h7 = _source4; - Dafny.ISequence _74_name = _73___mcc_h7; - s = _74_name; - } + Dafny.ISequence _73___mcc_h7 = _source4; + Dafny.ISequence _74_name = _73___mcc_h7; + s = _74_name; } return s; } @@ -3972,11 +3970,12 @@ public static void GenExpr(DAST._IExpression e, Dafny.ISequence.Concat(Dafny.Sequence.Concat(_302_onString, Dafny.Sequence.UnicodeFromString(".")), DCOMP.__default.natToString(_300_idx)); + s = Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("("), _302_onString), Dafny.Sequence.UnicodeFromString(").")), DCOMP.__default.natToString(_300_idx)); if (mustOwn) { - s = Dafny.Sequence.Concat(s, Dafny.Sequence.UnicodeFromString(".clone()")); + s = Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("("), s), Dafny.Sequence.UnicodeFromString(")")), Dafny.Sequence.UnicodeFromString(".clone()")); isOwned = true; } else { + s = Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("&"), s); isOwned = false; } readIdents = _304_recIdents;