From 041a1a226a96ba55ff22251eb98666241a1d769a Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 8 Jan 2014 18:47:33 -0800 Subject: Allow left-hand sides of a let expression to be patterns (like in the case of a match expression). Moved the implementation of CondApplyBox, BoxIfNecessary, CondApplyUnbox, and ModeledAsBoxType from class ExpressionTranslator to class Translator. Fixed compilation of match expressions, to allow them anywhere. --- Binaries/DafnyRuntime.cs | 1 + Source/Dafny/Cloner.cs | 11 +- Source/Dafny/Compiler.cs | 189 +++++++++++++++++--------- Source/Dafny/Dafny.atg | 66 ++++++--- Source/Dafny/DafnyAst.cs | 85 +++++++++++- Source/Dafny/Parser.cs | 83 ++++++++---- Source/Dafny/Printer.cs | 29 +++- Source/Dafny/Resolver.cs | 127 +++++++++++++---- Source/Dafny/Translator.cs | 329 ++++++++++++++++++++++++++++++--------------- Test/dafny0/Answer | 26 +++- Test/dafny0/LetExpr.dfy | 85 ++++++++++++ 11 files changed, 784 insertions(+), 247 deletions(-) diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index a8faafae..3afac587 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -627,5 +627,6 @@ namespace Dafny { return u; } + public delegate Result Function(Input input); } } diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index ee3820b3..7a057a62 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -295,7 +295,7 @@ namespace Microsoft.Dafny } else if (expr is LetExpr) { var e = (LetExpr)expr; - return new LetExpr(Tok(e.tok), e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body), e.Exact); + return new LetExpr(Tok(e.tok), e.LHSs.ConvertAll(CloneCasePattern), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body), e.Exact); } else if (expr is NamedExpr) { var e = (NamedExpr)expr; @@ -347,6 +347,15 @@ namespace Microsoft.Dafny } } + public CasePattern CloneCasePattern(CasePattern pat) { + Contract.Requires(pat != null); + if (pat.Arguments == null) { + return new CasePattern(pat.tok, CloneBoundVar(pat.Var)); + } else { + return new CasePattern(pat.tok, pat.Id, pat.Arguments.ConvertAll(CloneCasePattern)); + } + } + public AssignmentRhs CloneRHS(AssignmentRhs rhs) { AssignmentRhs c; if (rhs is ExprRhs) { diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index aa59abad..7ab47d7d 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -37,6 +37,17 @@ namespace Microsoft.Dafny { } } + Dictionary uniqueAstNumbers = new Dictionary(); + int GetUniqueAstNumber(Expression expr) { + Contract.Requires(expr != null); + int n; + if (!uniqueAstNumbers.TryGetValue(expr, out n)) { + n = uniqueAstNumbers.Count; + uniqueAstNumbers.Add(expr, n); + } + return n; + } + public int ErrorCount; void Error(string msg, params object[] args) { Contract.Requires(msg != null); @@ -781,49 +792,11 @@ namespace Microsoft.Dafny { void CompileReturnBody(Expression body, int indent) { Contract.Requires(0 <= indent); body = body.Resolved; - if (body is MatchExpr) { - MatchExpr me = (MatchExpr)body; - // Type source = e; - // if (source.is_Ctor0) { - // FormalType f0 = ((Dt_Ctor0)source._D).a0; - // ... - // return Body0; - // } else if (...) { - // ... - // } else if (true) { - // ... - // } - - SpillLetVariableDecls(me.Source, indent); - string source = "_source" + tmpVarCount; - tmpVarCount++; - Indent(indent); - wr.Write("{0} {1} = ", TypeName(cce.NonNull(me.Source.Type)), source); - TrExpr(me.Source); - wr.WriteLine(";"); - - if (me.Cases.Count == 0) { - // the verifier would have proved we never get here; still, we need some code that will compile - Indent(indent); - wr.WriteLine("throw new System.Exception();"); - } else { - int i = 0; - var sourceType = (UserDefinedType)me.Source.Type; - foreach (MatchCaseExpr mc in me.Cases) { - MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, me.Cases.Count, indent + IndentAmount); - CompileReturnBody(mc.Body, indent + IndentAmount); - i++; - } - Indent(indent); wr.WriteLine("}"); - } - - } else { - SpillLetVariableDecls(body, indent); - Indent(indent); - wr.Write("return "); - TrExpr(body); - wr.WriteLine(";"); - } + SpillLetVariableDecls(body, indent); + Indent(indent); + wr.Write("return "); + TrExpr(body); + wr.WriteLine(";"); } void SpillLetVariableDecls(Expression expr, int indent) { @@ -834,17 +807,29 @@ namespace Microsoft.Dafny { } if (expr is LetExpr) { var e = (LetExpr)expr; - foreach (var v in e.Vars) { - if (!v.IsGhost) { - Indent(indent); - wr.WriteLine("{0} @{1};", TypeName(v.Type), v.CompileName); - } - } - Contract.Assert(e.Vars.Count == e.RHSs.Count); + // Bound variables introduced in the LHS are ghost if either the entire let expression is declared + // a ghost or the position of a variable corresponds to the datatype constructor argument that is + // declared a ghost. If all variables are ghost, then the corresponding RHS is not needed; but if + // there is any non-ghost variable, then the corresponding RHS is needed. + Contract.Assert(e.LHSs.Count == e.RHSs.Count); var i = 0; - foreach (var rhs in e.RHSs) { - if (!e.Vars[i].IsGhost) { - SpillLetVariableDecls(rhs, indent); + foreach (var lhs in e.LHSs) { + var needRHS = false; + foreach (var v in lhs.Vars) { + if (!v.IsGhost) { + if (!needRHS) { + // this is the first of lhs's variables that we have found we need + Indent(indent); + var nm = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i); + wr.WriteLine("{0} @{1};", TypeName(e.RHSs[i].Type), nm); + needRHS = true; + } + Indent(indent); + wr.WriteLine("{0} @{1};", TypeName(v.Type), v.CompileName); + } + } + if (needRHS) { + SpillLetVariableDecls(e.RHSs[i], indent); } i++; } @@ -899,7 +884,7 @@ namespace Microsoft.Dafny { UserDefinedType udt = (UserDefinedType)type; string s = "@" + udt.FullCompileName; if (udt.TypeArgs.Count != 0) { - if (Contract.Exists(udt.TypeArgs, argType =>argType is ObjectType)) { + if (udt.TypeArgs.Exists(argType => argType is ObjectType)) { Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost"); } s += "<" + TypeNames(udt.TypeArgs) + ">"; @@ -2354,27 +2339,71 @@ namespace Microsoft.Dafny { } else if (expr is LetExpr) { var e = (LetExpr)expr; // The Dafny "let" expression - // var x := G; E + // var Pattern(x,y) := G; E // is translated into C# as: - // ExpressionSequence(x = G, E) - // preceded by the declaration of x. - Contract.Assert(e.Vars.Count == e.RHSs.Count); // checked by resolution + // ExpressionSequence(tmp = G, + // ExpressionSequence(x = dtorX(tmp), + // ExpressionSequence(y = dtorY(tmp), E))) + // preceded by the declaration of tmp, x, y. + Contract.Assert(e.LHSs.Count == e.RHSs.Count); // checked by resolution Contract.Assert(e.Exact); // because !Exact is ghost only - var nonGhostVars = 0; - for (int i = 0; i < e.Vars.Count; i++) { - var v = e.Vars[i]; - if (!v.IsGhost) { - wr.Write("Dafny.Helpers.ExpressionSequence(@{0} = ", e.Vars[i].CompileName); + var neededCloseParens = 0; + for (int i = 0; i < e.LHSs.Count; i++) { + var lhs = e.LHSs[i]; + if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) { + var rhsName = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i); + wr.Write("Dafny.Helpers.ExpressionSequence({0} = ", rhsName); TrExpr(e.RHSs[i]); wr.Write(", "); - nonGhostVars++; + neededCloseParens++; + var c = TrCasePattern(lhs, rhsName); + Contract.Assert(c != 0); // we already checked that there's at least one non-ghost + neededCloseParens += c; } } TrExpr(e.Body); - for (int i = 0; i < nonGhostVars; i++) { + for (int i = 0; i < neededCloseParens; i++) { wr.Write(")"); } + } else if (expr is MatchExpr) { + var e = (MatchExpr)expr; + // new Dafny.Helpers.Function(delegate (SourceType _source) { + // if (source.is_Ctor0) { + // FormalType f0 = ((Dt_Ctor0)source._D).a0; + // ... + // return Body0; + // } else if (...) { + // ... + // } else if (true) { + // ... + // } + // }(src) + + string source = "_source" + tmpVarCount; + tmpVarCount++; + wr.Write("new Dafny.Helpers.Function<{0}, {1}>(delegate ({0} {2}) {{ ", TypeName(e.Source.Type), TypeName(e.Type), source); + + if (e.Cases.Count == 0) { + // the verifier would have proved we never get here; still, we need some code that will compile + wr.Write("throw new System.Exception();"); + } else { + int i = 0; + var sourceType = (UserDefinedType)e.Source.Type; + foreach (MatchCaseExpr mc in e.Cases) { + MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, 0); + wr.Write("return "); + TrExpr(mc.Body); + wr.Write("; "); + i++; + } + wr.Write("}"); + } + // We end with applying the source expression to the delegate we just built + wr.Write("})("); + TrExpr(e.Source); + wr.Write(")"); + } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; Contract.Assert(e.Bounds != null); // for non-ghost quantifiers, the resolver would have insisted on finding bounds @@ -2582,6 +2611,36 @@ namespace Microsoft.Dafny { } } + int TrCasePattern(CasePattern pat, string rhsName) { + Contract.Requires(pat != null); + Contract.Requires(rhsName != null); + int c = 0; + if (pat.Var != null) { + var bv = pat.Var; + if (!bv.IsGhost) { + wr.Write("Dafny.Helpers.ExpressionSequence(@{0} = {1}, ", bv.CompileName, rhsName); + c++; + } + } else if (pat.Arguments != null) { + var ctor = pat.Ctor; + Contract.Assert(ctor != null); // follows from successful resolution + Contract.Assert(pat.Arguments.Count == ctor.Formals.Count); // follows from successful resolution + var k = 0; // number of non-ghost formals processed + for (int i = 0; i < pat.Arguments.Count; i++) { + var arg = pat.Arguments[i]; + var formal = ctor.Formals[i]; + if (formal.IsGhost) { + // nothing to compile, but do a sanity check + Contract.Assert(!Contract.Exists(arg.Vars, bv => !bv.IsGhost)); + } else { + c += TrCasePattern(arg, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs), rhsName, FormalName(formal, k))); + k++; + } + } + } + return c; + } + delegate void FCE_Arg_Translator(Expression e); void CompileFunctionCallExpr(FunctionCallExpr e, TextWriter twr, FCE_Arg_Translator tr) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 23c31b0d..985dd5cf 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -120,6 +120,11 @@ bool IsParenStar() { return la.kind == _openparen && x.kind == _star; } +bool IsIdentParen() { + Token x = scanner.Peek(); + return la.kind == _ident && x.kind == _openparen; +} + bool SemiFollowsCall(bool allowSemi, Expression e) { return allowSemi && la.kind == _semi && (e is FunctionCallExpr || @@ -425,12 +430,6 @@ LocalIdentTypeOptional ] (. var = new VarDecl(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .) . -IdentTypeOptionalG -= (. Contract.Ensures(Contract.ValueAtReturn(out var) != null); - .) - IdentTypeOptional - (. var.IsGhost = isGhost; .) - . IdentTypeOptional = (. Contract.Ensures(Contract.ValueAtReturn(out var) != null); IToken id; Type ty; Type optType = null; @@ -1916,28 +1915,37 @@ StmtInExpr LetExpr = (. IToken x = null; - e = dummyExpr; - BoundVar d; - List letVars; List letRHSs; - bool exact = true; bool isGhost = false; + var letLHSs = new List(); + var letRHSs = new List(); + CasePattern pat; + bool exact = true; + e = dummyExpr; .) [ "ghost" (. isGhost = true; x = t; .) ] - "var" (. if (!isGhost) { x = t; } - letVars = new List(); - letRHSs = new List(); .) - IdentTypeOptionalG (. letVars.Add(d); .) - { "," IdentTypeOptionalG (. letVars.Add(d); .) + "var" (. if (!isGhost) { x = t; } .) + CasePattern (. if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); } + letLHSs.Add(pat); + .) + { "," CasePattern (. if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); } + letLHSs.Add(pat); + .) } ( ":=" - | ":|" (. exact = false; .) + | ":|" (. exact = false; + foreach (var lhs in letLHSs) { + if (lhs.Arguments != null) { + SemErr(lhs.tok, "LHS of let-such-that expression must be variables, not general patterns"); + } + } + .) ) Expression (. letRHSs.Add(e); .) { "," Expression (. letRHSs.Add(e); .) } ";" - Expression (. e = new LetExpr(x, letVars, letRHSs, e, exact); .) + Expression (. e = new LetExpr(x, letLHSs, letRHSs, e, exact); .) . NamedExpr @@ -1980,6 +1988,30 @@ CaseExpression ")" ] "=>" Expression (. c = new MatchCaseExpr(x, id.val, arguments, body); .) + . +CasePattern += (. IToken id; List arguments; + BoundVar bv; + pat = null; + .) + ( IF(IsIdentParen()) + Ident + "(" (. arguments = new List(); .) + [ CasePattern (. arguments.Add(pat); .) + { "," CasePattern (. arguments.Add(pat); .) + } + ] + ")" (. pat = new CasePattern(id, id.val, arguments); .) + + | IdentTypeOptional (. // This could be a BoundVar of a parameter-less constructor and we may not know until resolution. + // Nevertheless, we do put the "bv" into the CasePattern here (even though it will get thrown out + // later if resolution finds the CasePattern to denote a parameter-less constructor), because this + // (in particular, bv.IsGhost) is the place where a LetExpr records whether or not the "ghost" + // keyword was used in the declaration. + pat = new CasePattern(bv.tok, bv); + .) + ) + . /*------------------------------------------------------------------------*/ DottedIdentifiersAndFunction diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index c9d7dfe2..75b30afd 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4781,14 +4781,14 @@ namespace Microsoft.Dafny { public class LetExpr : Expression { - public readonly List Vars; + public readonly List LHSs; public readonly List RHSs; public readonly Expression Body; public readonly bool Exact; // Exact==true means a regular let expression; Exact==false means an assign-such-that expression public Expression translationDesugaring; // filled in during translation, lazily; to be accessed only via Translation.LetDesugaring; always null when Exact==true - public LetExpr(IToken tok, List vars, List rhss, Expression body, bool exact) + public LetExpr(IToken tok, List lhss, List rhss, Expression body, bool exact) : base(tok) { - Vars = vars; + LHSs = lhss; RHSs = rhss; Body = body; Exact = exact; @@ -4801,6 +4801,15 @@ namespace Microsoft.Dafny { yield return Body; } } + public IEnumerable BoundVars { + get { + foreach (var lhs in LHSs) { + foreach (var bv in lhs.Vars) { + yield return bv; + } + } + } + } } // Represents expr Name: Body // or expr Name: (assert Body == Contract; Body) @@ -5121,6 +5130,76 @@ namespace Microsoft.Dafny { } } + /// + /// A CasePattern is either a BoundVar or a datatype constructor with optional arguments. + /// Lexically, the CasePattern starts with an identifier. If it continues with an open paren (as + /// indicated by Arguments being non-null), then the CasePattern is a datatype constructor. If + /// it continues with a colon (which is indicated by Var.Type not being a proxy type), then it is + /// a BoundVar. But if it ends with just the identifier, then resolution is required to figure out + /// which it is; in this case, Var is non-null, because this is the only place where Var.IsGhost + /// is recorded by the parser. + /// + public class CasePattern + { + public readonly IToken tok; + public readonly string Id; + // After successful resolution, exactly one of the following two fields is non-null. + public DatatypeCtor Ctor; // finalized by resolution (null if the pattern is a bound variable) + public BoundVar Var; // finalized by resolution (null if the pattern is a constructor) Invariant: Var != null ==> Arguments == null + public readonly List Arguments; + + public Expression Expr; // an r-value version of the CasePattern; filled in by resolution + + public CasePattern(IToken tok, string id, [Captured] List arguments) { + Contract.Requires(tok != null); + Contract.Requires(id != null); + this.tok = tok; + Id = id; + Arguments = arguments; + } + + public CasePattern(IToken tok, BoundVar bv) { + Contract.Requires(tok != null); + Contract.Requires(bv != null); + this.tok = tok; + Id = bv.Name; + Var = bv; + } + + /// + /// Sets the Expr field. Assumes the CasePattern and its arguments to have been successfully resolved, except for assigning + /// to Expr. + /// + public void AssembleExpr(List dtvTypeArgs) { + Contract.Requires(Var != null || dtvTypeArgs != null); + if (Var != null) { + var ie = new IdentifierExpr(this.tok, this.Id); + ie.Var = this.Var; ie.Type = this.Var.Type; // resolve here + this.Expr = ie; + } else { + var dtValue = new DatatypeValue(this.tok, this.Ctor.EnclosingDatatype.Name, this.Id, this.Arguments.ConvertAll(arg => arg.Expr)); + dtValue.Ctor = this.Ctor; // resolve here + dtValue.InferredTypeArgs.AddRange(dtvTypeArgs); // resolve here + dtValue.Type = new UserDefinedType(this.tok, this.Ctor.EnclosingDatatype.Name, this.Ctor.EnclosingDatatype, dtvTypeArgs); + this.Expr = dtValue; + } + } + + public IEnumerable Vars { + get { + if (Var != null) { + yield return Var; + } else { + foreach (var arg in Arguments) { + foreach (var bv in arg.Vars) { + yield return bv; + } + } + } + } + } + } + public abstract class MatchCase { public readonly IToken tok; diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index f11e1396..5af2410d 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -145,6 +145,11 @@ bool IsParenStar() { return la.kind == _openparen && x.kind == _star; } +bool IsIdentParen() { + Token x = scanner.Peek(); + return la.kind == _ident && x.kind == _openparen; +} + bool SemiFollowsCall(bool allowSemi, Expression e) { return allowSemi && la.kind == _semi && (e is FunctionCallExpr || @@ -1036,13 +1041,6 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { var = new VarDecl(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); } - void IdentTypeOptionalG(out BoundVar var, bool isGhost) { - Contract.Ensures(Contract.ValueAtReturn(out var) != null); - - IdentTypeOptional(out var); - var.IsGhost = isGhost; - } - void IdentTypeOptional(out BoundVar var) { Contract.Ensures(Contract.ValueAtReturn(out var) != null); IToken id; Type ty; Type optType = null; @@ -3342,32 +3340,41 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void LetExpr(out Expression e, bool allowSemi) { IToken x = null; - e = dummyExpr; - BoundVar d; - List letVars; List letRHSs; - bool exact = true; bool isGhost = false; + var letLHSs = new List(); + var letRHSs = new List(); + CasePattern pat; + bool exact = true; + e = dummyExpr; if (la.kind == 24) { Get(); isGhost = true; x = t; } Expect(29); - if (!isGhost) { x = t; } - letVars = new List(); - letRHSs = new List(); - IdentTypeOptionalG(out d, isGhost); - letVars.Add(d); + if (!isGhost) { x = t; } + CasePattern(out pat); + if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); } + letLHSs.Add(pat); + while (la.kind == 30) { Get(); - IdentTypeOptionalG(out d, isGhost); - letVars.Add(d); + CasePattern(out pat); + if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); } + letLHSs.Add(pat); + } if (la.kind == 67) { Get(); } else if (la.kind == 69) { Get(); - exact = false; + exact = false; + foreach (var lhs in letLHSs) { + if (lhs.Arguments != null) { + SemErr(lhs.tok, "LHS of let-such-that expression must be variables, not general patterns"); + } + } + } else SynErr(220); Expression(out e, false); letRHSs.Add(e); @@ -3378,7 +3385,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(7); Expression(out e, allowSemi); - e = new LetExpr(x, letVars, letRHSs, e, exact); + e = new LetExpr(x, letLHSs, letRHSs, e, exact); } void NamedExpr(out Expression e, bool allowSemi) { @@ -3395,6 +3402,33 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new NamedExpr(x, d.val, expr); } + void CasePattern(out CasePattern pat) { + IToken id; List arguments; + BoundVar bv; + pat = null; + + if (IsIdentParen()) { + Ident(out id); + Expect(10); + arguments = new List(); + if (la.kind == 1) { + CasePattern(out pat); + arguments.Add(pat); + while (la.kind == 30) { + Get(); + CasePattern(out pat); + arguments.Add(pat); + } + } + Expect(33); + pat = new CasePattern(id, id.val, arguments); + } else if (la.kind == 1) { + IdentTypeOptional(out bv); + pat = new CasePattern(bv.tok, bv); + + } else SynErr(221); + } + void CaseExpression(out MatchCaseExpr c, bool allowSemi) { Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id; List arguments = new List(); @@ -3425,7 +3459,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 118) { Get(); - } else SynErr(221); + } else SynErr(222); } void Exists() { @@ -3433,7 +3467,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 120) { Get(); - } else SynErr(222); + } else SynErr(223); } void AttributeBody(ref Attributes attrs) { @@ -3745,8 +3779,9 @@ public class Errors { case 218: s = "invalid QuantifierGuts"; break; case 219: s = "invalid StmtInExpr"; break; case 220: s = "invalid LetExpr"; break; - case 221: s = "invalid Forall"; break; - case 222: s = "invalid Exists"; break; + case 221: s = "invalid CasePattern"; break; + case 222: s = "invalid Forall"; break; + case 223: s = "invalid Exists"; break; default: s = "error " + n; break; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 24375f7b..d9b6abae 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1371,9 +1371,9 @@ namespace Microsoft.Dafny { if (parensNeeded) { wr.Write("("); } wr.Write("var "); string sep = ""; - foreach (var v in e.Vars) { - wr.Write("{0}{1}", sep, v.DisplayName); - PrintType(": ", v.Type); + foreach (var lhs in e.LHSs) { + wr.Write(sep); + PrintCasePattern(lhs); sep = ", "; } if (e.Exact) { @@ -1529,6 +1529,29 @@ namespace Microsoft.Dafny { } } + void PrintCasePattern(CasePattern pat) { + Contract.Requires(pat != null); + var v = pat.Var; + if (v != null) { + wr.Write(v.DisplayName); + if (v.Type is NonProxyType || DafnyOptions.O.DafnyPrintResolvedFile != null) { + PrintType(": ", v.Type); + } + } else { + wr.Write(pat.Id); + if (pat.Arguments != null) { + wr.Write("("); + var sep = ""; + foreach (var arg in pat.Arguments) { + wr.Write(sep); + PrintCasePattern(arg); + sep = ", "; + } + wr.Write(")"); + } + } + } + private void PrintQuantifierDomain(List boundVars, Attributes attrs, Expression range) { Contract.Requires(boundVars != null); string sep = ""; diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 048a75b8..0b84ed36 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1241,7 +1241,7 @@ namespace Microsoft.Dafny } else if (expr is LetExpr) { var e = (LetExpr)expr; - return new LetExpr(e.tok, e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body), e.Exact); + return new LetExpr(e.tok, e.LHSs.ConvertAll(CloneCasePattern), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body), e.Exact); } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; @@ -1290,6 +1290,15 @@ namespace Microsoft.Dafny } } + public CasePattern CloneCasePattern(CasePattern pat) { + Contract.Requires(pat != null); + if (pat.Arguments == null) { + return new CasePattern(pat.tok, CloneBoundVar(pat.Var)); + } else { + return new CasePattern(pat.tok, pat.Id, pat.Arguments.ConvertAll(CloneCasePattern)); + } + } + public static bool ResolvePath(ModuleDecl root, List Path, out ModuleSignature p, ResolutionErrorReporter reporter) { Contract.Requires(reporter != null); p = root.Signature; @@ -2295,7 +2304,7 @@ namespace Microsoft.Dafny } } else if (expr is LetExpr) { var e = (LetExpr)expr; - foreach (var bv in e.Vars) { + foreach (var bv in e.BoundVars) { CheckEqualityTypes_Type(bv.tok, bv.Type); } } else if (expr is FunctionCallExpr) { @@ -4365,7 +4374,7 @@ namespace Microsoft.Dafny } s.IsGhost = bodyIsSpecOnly; - Dictionary memberNamesUsed = new Dictionary(); // this is really a set + ISet memberNamesUsed = new HashSet(); foreach (MatchCaseStmt mc in s.Cases) { DatatypeCtor ctor = null; if (ctors != null) { @@ -4378,10 +4387,10 @@ namespace Microsoft.Dafny if (ctor.Formals.Count != mc.Arguments.Count) { Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count); } - if (memberNamesUsed.ContainsKey(mc.Id)) { + if (memberNamesUsed.Contains(mc.Id)) { Error(mc.tok, "member {0} appears in more than one case", mc.Id); } else { - memberNamesUsed.Add(mc.Id, null); // add mc.Id to the set of names used + memberNamesUsed.Add(mc.Id); // add mc.Id to the set of names used } } } @@ -4413,7 +4422,7 @@ namespace Microsoft.Dafny // but instead we let the verifier do a semantic check. // So, for now, record the missing constructors: foreach (var ctr in dtd.Ctors) { - if (!memberNamesUsed.ContainsKey(ctr.Name)) { + if (!memberNamesUsed.Contains(ctr.Name)) { s.MissingCases.Add(ctr); } } @@ -4513,7 +4522,7 @@ namespace Microsoft.Dafny int errorCountBeforeCheckingLhs = ErrorCount; var update = s as UpdateStmt; - var lhsNameSet = new Dictionary(); // used to check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification) + var lhsNameSet = new HashSet(); // used to check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification) foreach (var lhs in s.Lhss) { var ec = ErrorCount; ResolveExpression(lhs, true, codeContext); @@ -4526,10 +4535,10 @@ namespace Microsoft.Dafny } var ie = lhs.Resolved as IdentifierExpr; if (ie != null) { - if (lhsNameSet.ContainsKey(ie.Name)) { + if (lhsNameSet.Contains(ie.Name)) { Error(update, "duplicate variable in left-hand side of call statement: {0}", ie.Name); } else { - lhsNameSet.Add(ie.Name, null); + lhsNameSet.Add(ie.Name); } } } @@ -5904,17 +5913,24 @@ namespace Microsoft.Dafny ResolveExpression(rhs, twoState, codeContext); } scope.PushMarker(); - if (e.Vars.Count != e.RHSs.Count) { - Error(expr, "let expression must have same number of bound variables (found {0}) as RHSs (found {1})", e.Vars.Count, e.RHSs.Count); + if (e.LHSs.Count != e.RHSs.Count) { + Error(expr, "let expression must have same number of LHSs (found {0}) as RHSs (found {1})", e.LHSs.Count, e.RHSs.Count); } - int i = 0; - foreach (var v in e.Vars) { - if (!scope.Push(v.Name, v)) { - Error(v, "Duplicate let-variable name: {0}", v.Name); + var i = 0; + foreach (var lhs in e.LHSs) { + var rhsType = i < e.RHSs.Count ? e.RHSs[i].Type : new InferredTypeProxy(); + ResolveCasePattern(lhs, rhsType); + // Check for duplicate names now, because not until after resolving the case pattern do we know if identifiers inside it refer to bound variables or nullary constructors + var c = 0; + foreach (var v in lhs.Vars) { + if (!scope.Push(v.Name, v)) { + Error(v, "Duplicate let-variable name: {0}", v.Name); + } + c++; } - ResolveType(v.tok, v.Type, ResolveTypeOption.InferTypeProxies, null); - if (i < e.RHSs.Count && !UnifyTypes(v.Type, e.RHSs[i].Type)) { - Error(e.RHSs[i].tok, "type of RHS ({0}) does not match type of bound variable ({1})", e.RHSs[i].Type, v.Type); + if (c == 0) { + // Every identifier-looking thing in the patterned resolved to a constructor; that is, this LHS is a constant literal + Error(lhs.tok, "LHS is a constant literal; to be legal, it must introduce at least one bound variable"); } i++; } @@ -5925,7 +5941,9 @@ namespace Microsoft.Dafny } // the bound variables are in scope in the RHS of a let-such-that expression scope.PushMarker(); - foreach (var v in e.Vars) { + foreach (var lhs in e.LHSs) { + Contract.Assert(lhs.Var != null); // the parser already checked that every LHS is a BoundVar, not a general pattern + var v = lhs.Var; if (!scope.Push(v.Name, v)) { Error(v, "Duplicate let-variable name: {0}", v.Name); } @@ -6132,7 +6150,7 @@ namespace Microsoft.Dafny } } - Dictionary memberNamesUsed = new Dictionary(); // this is really a set + ISet memberNamesUsed = new HashSet(); expr.Type = new InferredTypeProxy(); foreach (MatchCaseExpr mc in me.Cases) { DatatypeCtor ctor = null; @@ -6146,10 +6164,10 @@ namespace Microsoft.Dafny if (ctor.Formals.Count != mc.Arguments.Count) { Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count); } - if (memberNamesUsed.ContainsKey(mc.Id)) { + if (memberNamesUsed.Contains(mc.Id)) { Error(mc.tok, "member {0} appears in more than one case", mc.Id); } else { - memberNamesUsed.Add(mc.Id, null); // add mc.Id to the set of names used + memberNamesUsed.Add(mc.Id); // add mc.Id to the set of names used } } } @@ -6183,7 +6201,7 @@ namespace Microsoft.Dafny // but instead we let the verifier do a semantic check. // So, for now, record the missing constructors: foreach (var ctr in dtd.Ctors) { - if (!memberNamesUsed.ContainsKey(ctr.Name)) { + if (!memberNamesUsed.Contains(ctr.Name)) { me.MissingCases.Add(ctr); } } @@ -6200,6 +6218,65 @@ namespace Microsoft.Dafny } } + void ResolveCasePattern(CasePattern pat, Type sourceType) { + Contract.Requires(pat != null); + Contract.Requires(sourceType != null); + + DatatypeDecl dtd = null; + UserDefinedType udt = null; + if (sourceType.IsDatatype) { + udt = (UserDefinedType)sourceType; + dtd = (DatatypeDecl)udt.ResolvedClass; + } + // Find the constructor in the given datatype + // If what was parsed was just an identifier, we will interpret it as a datatype constructor, if possible + DatatypeCtor ctor = null; + if (pat.Var == null || (pat.Var != null && pat.Var.Type is TypeProxy && dtd != null)) { + if (datatypeCtors[dtd].TryGetValue(pat.Id, out ctor)) { + pat.Ctor = ctor; + pat.Var = null; + } + } + + if (pat.Var != null) { + // this is a simple resolution + var v = pat.Var; + ResolveType(v.tok, v.Type, ResolveTypeOption.InferTypeProxies, null); + if (!UnifyTypes(v.Type, sourceType)) { + Error(v.tok, "type of corresponding source/RHS ({0}) does not match type of bound variable ({1})", sourceType, v.Type); + } + pat.AssembleExpr(null); + } else if (dtd == null) { + Error(pat.tok, "to use a pattern, the type of the source/RHS expression must be a datatype (instead found {0})", sourceType); + } else if (ctor == null) { + Error(pat.tok, "constructor {0} does not exist in datatype {1}", pat.Id, dtd.Name); + } else { + var argCount = pat.Arguments == null ? 0 : pat.Arguments.Count; + if (ctor.Formals.Count != argCount) { + Error(pat.tok, "pattern for constructor {0} has wrong number of formals (found {1}, expected {2})", pat.Id, argCount, ctor.Formals.Count); + } + // build the type-parameter substitution map for this use of the datatype + Contract.Assert(dtd.TypeArgs.Count == udt.TypeArgs.Count); // follows from the type previously having been successfully resolved + var subst = new Dictionary(); + for (int i = 0; i < dtd.TypeArgs.Count; i++) { + subst.Add(dtd.TypeArgs[i], udt.TypeArgs[i]); + } + // recursively call ResolveCasePattern on each of the arguments + var j = 0; + foreach (var arg in pat.Arguments) { + if (j < ctor.Formals.Count) { + var formal = ctor.Formals[j]; + Type st = SubstType(formal.Type, subst); + ResolveCasePattern(arg, st); + } + j++; + } + if (j == ctor.Formals.Count) { + pat.AssembleExpr(udt.TypeArgs); + } + } + } + private void ResolveDatatypeValue(bool twoState, ICodeContext codeContext, DatatypeValue dtv, DatatypeDecl dt) { // this resolution is a little special, in that the syntax shows only the base name, not its instantiation (which is inferred) List gt = new List(dt.TypeArgs.Count); @@ -6382,10 +6459,10 @@ namespace Microsoft.Dafny if (!e.Exact) { Error(expr, "let-such-that expressions are allowed only in ghost contexts"); } - Contract.Assert(e.Vars.Count == e.RHSs.Count); + Contract.Assert(e.LHSs.Count == e.RHSs.Count); var i = 0; foreach (var ee in e.RHSs) { - if (!e.Vars[i].IsGhost) { + if (!e.LHSs[i].Vars.All(bv => bv.IsGhost)) { CheckIsNonGhost(ee); } i++; diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 92ce09bc..e5d0920d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3044,7 +3044,7 @@ namespace Microsoft.Dafny { if (wh != null) { localTypeAssumptions.Add(new Bpl.AssumeCmd(p.tok, wh)); } - args.Add(etran.CondApplyBox(mc.tok, new Bpl.IdentifierExpr(p.tok, local), cce.NonNull(p.Type), t)); + args.Add(CondApplyBox(mc.tok, new Bpl.IdentifierExpr(p.tok, local), cce.NonNull(p.Type), t)); } Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(mc.tok, mc.Ctor.FullName, predef.DatatypeType); return new Bpl.NAryExpr(mc.tok, new Bpl.FunctionCall(id), args); @@ -3185,13 +3185,15 @@ namespace Microsoft.Dafny { // CanCall[[ RHS(g) ]] && // CanCall[[ Body(b,g,h)[b := PROTECT(RHS(g))] ]] // where PROTECT(e) means protect e from variable capture (which is achieved by translating - // e and then putting it into a BoogieWrapper). + // e and then putting it into a BoogieWrapper). Actually, since the b may be a pattern, + // the substitution is really [b0 := PROTECT( RHS(g).dtor )] for each b0 in b and each corresponding + // path of destructors dtor. Bpl.Expr canCallRHS = Bpl.Expr.True; var substMap = new Dictionary(); int i = 0; - foreach (var bv in e.Vars) { + foreach (var lhs in e.LHSs) { canCallRHS = BplAnd(canCallRHS, CanCallAssumption(e.RHSs[i], etran)); - substMap.Add(bv, new BoogieWrapper(etran.TrExpr(e.RHSs[i]), bv.Type)); + AddCasePatternVarSubstitutions(lhs, etran.TrExpr(e.RHSs[i]), substMap); i++; } var canCallBody = CanCallAssumption(Substitute(e.Body, null, substMap), etran); @@ -3203,7 +3205,7 @@ namespace Microsoft.Dafny { // (RHS(b,g) ==> CanCall[[ Body(b,g,h) ]]) && // $let$canCall(b,g)) var bvars = new List(); - Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.Vars, bvars); + Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars.ToList(), bvars); Contract.Assert(e.RHSs.Count == 1); // this is true of all successfully resolved let-such-that expressions var canCallRHS = CanCallAssumption(e.RHSs[0], etran); var canCallBody = Bpl.Expr.Imp(etran.TrExpr(e.RHSs[0]), CanCallAssumption(e.Body, etran)); @@ -3257,6 +3259,53 @@ namespace Microsoft.Dafny { } } + void AddCasePatternVarSubstitutions(CasePattern pat, Bpl.Expr rhs, Dictionary substMap) { + Contract.Requires(pat != null); + Contract.Requires(rhs != null); + Contract.Requires(substMap != null); + if (pat.Var != null) { + substMap.Add(pat.Var, new BoogieWrapper(rhs, pat.Var.Type)); + } else if (pat.Arguments != null) { + Contract.Assert(pat.Ctor != null); // follows from successful resolution + Contract.Assert(pat.Arguments.Count == pat.Ctor.Destructors.Count); // follows from successful resolution + for (int i = 0; i < pat.Arguments.Count; i++) { + var arg = pat.Arguments[i]; + var dtor = pat.Ctor.Destructors[i]; + var r = new Bpl.NAryExpr(pat.tok, new Bpl.FunctionCall(GetReadonlyField(dtor)), new List { rhs }); + var de = CondApplyUnbox(pat.tok, r, dtor.Type, arg.Expr.Type); + AddCasePatternVarSubstitutions(arg, de, substMap); + } + } + } + + void CheckCasePatternShape(CasePattern pat, Bpl.Expr rhs, StmtListBuilder builder) { + Contract.Requires(pat != null); + Contract.Requires(rhs != null); + Contract.Requires(builder != null); + if (pat.Var != null) { + CheckSubrange(pat.tok, rhs, pat.Var.Type, builder); + } else if (pat.Arguments != null) { + Contract.Assert(pat.Ctor != null); // follows from successful resolution + Contract.Assert(pat.Arguments.Count == pat.Ctor.Destructors.Count); // follows from successful resolution + for (int i = 0; i < pat.Arguments.Count; i++) { + var arg = pat.Arguments[i]; + var ctor = pat.Ctor; + var dtor = ctor.Destructors[i]; + var correctConstructor = FunctionCall(pat.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, rhs); + if (ctor.EnclosingDatatype.Ctors.Count == 1) { + // There is only one constructor, so the value must have been constructed by it; might as well assume that here. + builder.Add(new Bpl.AssumeCmd(pat.tok, correctConstructor)); + } else { + builder.Add(Assert(pat.tok, correctConstructor, string.Format("RHS is not certain to look like the pattern '{0}'", ctor.Name))); + } + + var r = new Bpl.NAryExpr(pat.tok, new Bpl.FunctionCall(GetReadonlyField(dtor)), new List { rhs }); + var de = CondApplyUnbox(pat.tok, r, dtor.Type, arg.Expr.Type); + CheckCasePatternShape(arg, de, builder); + } + } + } + Bpl.Expr/*!*/ CanCallAssumption(List/*!*/ exprs, ExpressionTranslator/*!*/ etran) { Contract.Requires(etran != null); Contract.Requires(exprs != null); @@ -3444,7 +3493,7 @@ namespace Microsoft.Dafny { e0 = etran.TrExpr(e.E0); CheckWellformed(e.E0, options, locals, builder, etran); Bpl.Expr inDomain = FunctionCall(expr.tok, BuiltinFunction.MapDomain, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq); - inDomain = Bpl.Expr.Select(inDomain, etran.BoxIfNecessary(e.tok, e0, e.E0.Type)); + inDomain = Bpl.Expr.Select(inDomain, BoxIfNecessary(e.tok, e0, e.E0.Type)); builder.Add(Assert(expr.tok, inDomain, "element may not be in domain", options.AssertKv)); } else if (e.Seq.Type is MultiSetType) { // cool @@ -3536,7 +3585,7 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified? Expression ee = e.Args[i]; CheckSubrange(ee.tok, etran.TrExpr(ee), p.Type, builder); - Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), p.Type)); + Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, CondApplyBox(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), p.Type)); builder.Add(cmd); } // Check that every parameter is available in the state in which the function is invoked; this means checking that it has @@ -3688,18 +3737,19 @@ namespace Microsoft.Dafny { } else if (expr is LetExpr) { var e = (LetExpr)expr; if (e.Exact) { - var substMap = new Dictionary(); - Contract.Assert(e.Vars.Count == e.RHSs.Count); // checked by resolution - for (int i = 0; i < e.Vars.Count; i++) { - var vr = e.Vars[i]; - var tp = TrType(vr.Type); - var nm = vr.AssignUniqueName(currentDeclaration); - var v = new Bpl.LocalVariable(vr.tok, new Bpl.TypedIdent(vr.tok, nm, tp)); - locals.Add(v); - var lhs = new Bpl.IdentifierExpr(vr.tok, nm, tp); - - CheckWellformedWithResult(e.RHSs[i], options, lhs, vr.Type, locals, builder, etran); - substMap.Add(vr, new BoogieWrapper(lhs, vr.Type)); + var substMap = SetupBoundVarsAsLocals(e.BoundVars.ToList(), builder, locals, etran); + Contract.Assert(e.LHSs.Count == e.RHSs.Count); // checked by resolution + for (int i = 0; i < e.LHSs.Count; i++) { + var pat = e.LHSs[i]; + var rhs = e.RHSs[i]; + var nm = string.Format("let{0}#{1}", i, otherTmpVarCount); + otherTmpVarCount++; + var r = new Bpl.LocalVariable(pat.tok, new Bpl.TypedIdent(pat.tok, nm, TrType(rhs.Type))); + locals.Add(r); + var rIe = new Bpl.IdentifierExpr(pat.tok, r); + CheckWellformedWithResult(e.RHSs[i], options, rIe, pat.Expr.Type, locals, builder, etran); + CheckCasePatternShape(pat, rIe, builder); + builder.Add(new Bpl.AssumeCmd(pat.tok, Bpl.Expr.Eq(etran.TrExpr(Substitute(pat.Expr, null, substMap)), rIe))); } CheckWellformedWithResult(Substitute(e.Body, null, substMap), options, result, resultType, locals, builder, etran); result = null; @@ -3711,10 +3761,11 @@ namespace Microsoft.Dafny { // assume RHS(b); // CheckWellformed(Body(b)); Contract.Assert(e.RHSs.Count == 1); // this is true of all successfully resolved let-such-that expressions - var substMap = SetupBoundVarsAsLocals(e.Vars, builder, locals, etran); + List lhsVars = e.BoundVars.ToList(); + var substMap = SetupBoundVarsAsLocals(lhsVars, builder, locals, etran); var rhs = Substitute(e.RHSs[0], null, substMap); CheckWellformed(rhs, options, locals, builder, etran); - List, Expression>> partialGuesses = GeneratePartialGuesses(e.Vars, e.RHSs[0]); + List, Expression>> partialGuesses = GeneratePartialGuesses(lhsVars, e.RHSs[0]); Bpl.Expr w = Bpl.Expr.False; foreach (var tup in partialGuesses) { var body = etran.TrExpr(tup.Item2); @@ -4298,7 +4349,7 @@ namespace Microsoft.Dafny { var param = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified? var bActual = new Bpl.IdentifierExpr(Token.NoToken, m.Ins[i].AssignUniqueName(methodCheck.Refining), TrType(m.Ins[i].Type)); - var cmd = Bpl.Cmd.SimpleAssign(p.tok, param, etran.CondApplyUnbox(Token.NoToken, bActual, cce.NonNull( m.Ins[i].Type),p.Type)); + var cmd = Bpl.Cmd.SimpleAssign(p.tok, param, CondApplyUnbox(Token.NoToken, bActual, cce.NonNull( m.Ins[i].Type),p.Type)); builder.Add(cmd); ins.Add(param); } @@ -4311,7 +4362,7 @@ namespace Microsoft.Dafny { var tmpOuts = new List(); for (int i = 0; i < m.Outs.Count; i++) { var bLhs = m.Outs[i]; - if (!ExpressionTranslator.ModeledAsBoxType(method.Outs[i].Type) && ExpressionTranslator.ModeledAsBoxType(bLhs.Type)) { + if (!ModeledAsBoxType(method.Outs[i].Type) && ModeledAsBoxType(bLhs.Type)) { // we need an Box Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, "$tmp##" + otherTmpVarCount, TrType(method.Outs[i].Type))); otherTmpVarCount++; @@ -4704,6 +4755,58 @@ namespace Microsoft.Dafny { return typeParams; } + public Bpl.Expr CondApplyBox(IToken tok, Bpl.Expr e, Type fromType, Type toType) { + Contract.Requires(tok != null); + Contract.Requires(e != null); + Contract.Requires(fromType != null); + Contract.Ensures(Contract.Result() != null); + + if (!ModeledAsBoxType(fromType) && (toType == null || ModeledAsBoxType(toType))) { + return FunctionCall(tok, BuiltinFunction.Box, null, e); + } else { + return e; + } + } + + public Bpl.Expr BoxIfNecessary(IToken tok, Bpl.Expr e, Type fromType) { + Contract.Requires(tok != null); + Contract.Requires(e != null); + Contract.Requires(fromType != null); + Contract.Ensures(Contract.Result() != null); + + return CondApplyBox(tok, e, fromType, null); + } + + public Bpl.Expr CondApplyUnbox(IToken tok, Bpl.Expr e, Type fromType, Type toType) { + Contract.Requires(tok != null); + Contract.Requires(e != null); + Contract.Requires(fromType != null); + Contract.Requires(toType != null); + Contract.Ensures(Contract.Result() != null); + + if (ModeledAsBoxType(fromType) && !ModeledAsBoxType(toType)) { + return FunctionCall(tok, BuiltinFunction.Unbox, TrType(toType), e); + } else { + return e; + } + } + + public static bool ModeledAsBoxType(Type t) { + Contract.Requires(t != null); + while (true) { + TypeProxy tp = t as TypeProxy; + if (tp == null) { + break; + } else if (tp.T == null) { + // unresolved proxy + return false; + } else { + t = tp.T; + } + } + return t.IsTypeParameter; + } + // ----- Statement ---------------------------------------------------------------------------- /// @@ -5632,7 +5735,7 @@ namespace Microsoft.Dafny { } else { lhsType = null; } - g = etran.CondApplyBox(rhs.tok, g, rhs.Type, lhsType); + g = CondApplyBox(rhs.tok, g, rhs.Type, lhsType); qq = new Bpl.ForallExpr(s.Tok, xBvars, Bpl.Expr.Imp(xAnte, Bpl.Expr.Eq(xHeapOF, g))); updater.Add(new Bpl.AssumeCmd(s.Tok, qq)); @@ -6159,7 +6262,7 @@ namespace Microsoft.Dafny { if (lhsType != null) { CheckSubrange(lhs.tok, bRhs, lhsType, builder); } - bRhs = etran.CondApplyBox(lhs.tok, bRhs, lhs.Type, lhsType); + bRhs = CondApplyBox(lhs.tok, bRhs, lhs.Type, lhsType); lhsBuilders[i](bRhs, builder, etran); } @@ -6259,7 +6362,7 @@ namespace Microsoft.Dafny { actual = Args[i]; } TrStmt_CheckWellformed(actual, builder, locals, etran, true); - bActual = etran.CondApplyBox(actual.tok, etran.TrExpr(actual), actual.Type, formal.Type); + bActual = CondApplyBox(actual.tok, etran.TrExpr(actual), actual.Type, formal.Type); CheckSubrange(actual.tok, bActual, formal.Type, builder); } Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(formal.tok, param, bActual); @@ -6285,7 +6388,7 @@ namespace Microsoft.Dafny { var tmpOuts = new List(); for (int i = 0; i < Lhss.Count; i++) { var bLhs = Lhss[i]; - if (ExpressionTranslator.ModeledAsBoxType(callee.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType(LhsTypes[i])) { + if (ModeledAsBoxType(callee.Outs[i].Type) && !ModeledAsBoxType(LhsTypes[i])) { // we need an Unbox Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, "$tmp##" + otherTmpVarCount, predef.BoxType)); otherTmpVarCount++; @@ -6705,7 +6808,7 @@ namespace Microsoft.Dafny { otherTmpVarCount++; Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar); Bpl.Expr xSubT = Bpl.Expr.SelectTok(tok, x, t); - Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t); + Bpl.Expr unboxT = ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t); Bpl.Expr wh = GetWhereClause(tok, unboxT, st.Arg, etran); if (wh != null) { @@ -6720,7 +6823,7 @@ namespace Microsoft.Dafny { otherTmpVarCount++; Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar); Bpl.Expr xSubT = Bpl.Expr.SelectTok(tok, x, t); - Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t); + Bpl.Expr unboxT = ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t); Bpl.Expr isGoodMultiset = FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, null, x); Bpl.Expr wh = GetWhereClause(tok, unboxT, st.Arg, etran); @@ -6739,7 +6842,7 @@ namespace Microsoft.Dafny { otherTmpVarCount++; Bpl.Expr i = new Bpl.IdentifierExpr(tok, iVar); Bpl.Expr xSubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, x, i); - Bpl.Expr unbox = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? xSubI : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), xSubI); + Bpl.Expr unbox = ModeledAsBoxType(st.Arg) ? xSubI : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), xSubI); Bpl.Expr c = GetBoolBoxCondition(xSubI, st.Arg); Bpl.Expr wh = GetWhereClause(tok, unbox, st.Arg, etran); @@ -6765,8 +6868,8 @@ namespace Microsoft.Dafny { Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar); Bpl.Expr inDomain = Bpl.Expr.SelectTok(tok, FunctionCall(tok, BuiltinFunction.MapDomain, maptype, x), t); Bpl.Expr xAtT = Bpl.Expr.SelectTok(tok, FunctionCall(tok, BuiltinFunction.MapElements, maptype, x), t); - Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(mt.Domain) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(mt.Domain), t); - Bpl.Expr unboxXAtT = ExpressionTranslator.ModeledAsBoxType(mt.Range) ? xAtT : FunctionCall(tok, BuiltinFunction.Unbox, TrType(mt.Range), xAtT); + Bpl.Expr unboxT = ModeledAsBoxType(mt.Domain) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(mt.Domain), t); + Bpl.Expr unboxXAtT = ModeledAsBoxType(mt.Range) ? xAtT : FunctionCall(tok, BuiltinFunction.Unbox, TrType(mt.Range), xAtT); Bpl.Expr wh = GetWhereClause(tok, unboxT, mt.Domain, etran); if (wh != null) { @@ -7184,7 +7287,7 @@ namespace Microsoft.Dafny { Bpl.Expr bRhs = etran.TrExpr(e.Expr); CheckSubrange(tok, bRhs, checkSubrangeType, builder); - bRhs = etran.CondApplyBox(tok, bRhs, e.Expr.Type, lhsType); + bRhs = CondApplyBox(tok, bRhs, e.Expr.Type, lhsType); Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, bRhs); builder.Add(cmd); @@ -7258,12 +7361,12 @@ namespace Microsoft.Dafny { TrCallStmt(tRhs.InitCall, builder, locals, etran, nw); } // bLhs := $nw; - builder.Add(Bpl.Cmd.SimpleAssign(tok, bLhs, etran.CondApplyBox(tok, nw, tRhs.Type, lhsType))); + builder.Add(Bpl.Cmd.SimpleAssign(tok, bLhs, CondApplyBox(tok, nw, tRhs.Type, lhsType))); } return bLhs; } - void CheckSubrange(IToken tok, Expr bRhs, Type tp, StmtListBuilder builder) { + void CheckSubrange(IToken tok, Bpl.Expr bRhs, Type tp, StmtListBuilder builder) { Contract.Requires(tok != null); Contract.Requires(bRhs != null); Contract.Requires(tp != null); @@ -7275,7 +7378,7 @@ namespace Microsoft.Dafny { } } - Bpl.Expr CheckSubrange_Expr(IToken tok, Expr bRhs, Type tp) { + Bpl.Expr CheckSubrange_Expr(IToken tok, Bpl.Expr bRhs, Type tp) { Contract.Requires(tok != null); Contract.Requires(bRhs != null); Contract.Requires(tp != null); @@ -7346,21 +7449,21 @@ namespace Microsoft.Dafny { // and create the desugaring: // var x:X, y:Y := $let$x(g), $let$y(g); F(...) - // First, determine "g" as a list of Dafny variables FV plus possibly this, $Heap, and old($Heap) + // First, determine "g" as a list of Dafny variables FVs plus possibly this, $Heap, and old($Heap) LetSuchThatExprInfo info; { var FVs = new HashSet(); bool usesHeap = false, usesOldHeap = false; Type usesThis = null; ComputeFreeVariables(e.RHSs[0], FVs, ref usesHeap, ref usesOldHeap, ref usesThis, false); - foreach (var bv in e.Vars) { + foreach (var bv in e.BoundVars) { FVs.Remove(bv); } info = new LetSuchThatExprInfo(e.tok, letSuchThatExprInfo.Count, FVs.ToList(), usesHeap, usesOldHeap, usesThis, currentDeclaration); letSuchThatExprInfo.Add(e, info); } - foreach (var bv in e.Vars) { + foreach (var bv in e.BoundVars) { Bpl.Variable resType = new Bpl.Formal(bv.tok, new Bpl.TypedIdent(bv.tok, Bpl.TypedIdent.NoName, TrType(bv.Type)), false); Bpl.Expr ante; List formals = info.GAsVars(this, true, out ante, null); @@ -7396,7 +7499,7 @@ namespace Microsoft.Dafny { } Bpl.Trigger tr = null; Dictionary substMap = new Dictionary(); - foreach (var bv in e.Vars) { + foreach (var bv in e.BoundVars) { // create a call to $let$x(g) var call = FunctionCall(e.tok, info.SkolemFunctionName(bv), TrType(bv.Type), gExprs); tr = new Bpl.Trigger(e.tok, true, new List { call }, tr); @@ -7428,13 +7531,13 @@ namespace Microsoft.Dafny { { var etran = new ExpressionTranslator(this, predef, e.tok); var rhss = new List(); - foreach (var bv in e.Vars) { + foreach (var bv in e.BoundVars) { var args = info.SkolemFunctionArgs(bv, this, etran); var rhs = new BoogieFunctionCall(bv.tok, info.SkolemFunctionName(bv), info.UsesHeap, info.UsesOldHeap, args); rhs.Type = bv.Type; rhss.Add(rhs); } - e.translationDesugaring = new LetExpr(e.tok, e.Vars, rhss, e.Body, true); + e.translationDesugaring = new LetExpr(e.tok, e.LHSs, rhss, e.Body, true); e.translationDesugaring.Type = e.Type; // resolve here } } @@ -7827,11 +7930,10 @@ namespace Microsoft.Dafny { { Contract.Requires(e != null); Contract.Requires(e.Exact); - Contract.Assert(e.Vars.Count == e.RHSs.Count); // checked by resolution + Contract.Assert(e.LHSs.Count == e.RHSs.Count); // checked by resolution var substMap = new Dictionary(); - for (int i = 0; i < e.Vars.Count; i++) { - Expression rhs = e.RHSs[i]; - substMap.Add(e.Vars[i], new BoogieWrapper(TrExpr(rhs), rhs.Type)); + for (int i = 0; i < e.LHSs.Count; i++) { + translator.AddCasePatternVarSubstitutions(e.LHSs[i], TrExpr(e.RHSs[i]), substMap); } return translator.Substitute(e.Body, null, substMap); } @@ -7934,7 +8036,7 @@ namespace Microsoft.Dafny { } else { result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(translator.GetReadonlyField(e.Field)), new List { obj }); } - return CondApplyUnbox(expr.tok, result, e.Field.Type, cce.NonNull(expr.Type)); + return translator.CondApplyUnbox(expr.tok, result, e.Field.Type, cce.NonNull(expr.Type)); } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; @@ -8047,7 +8149,7 @@ namespace Microsoft.Dafny { var id = new Bpl.IdentifierExpr(e.tok, e.Function.FullSanitizedName, translator.TrType(e.Type)); var args = FunctionInvocationArguments(e, layerArgument); var result = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args); - return CondApplyUnbox(e.tok, result, e.Function.ResultType, e.Type); + return translator.CondApplyUnbox(e.tok, result, e.Function.ResultType, e.Type); } else if (expr is DatatypeValue) { DatatypeValue dtv = (DatatypeValue)expr; @@ -8057,7 +8159,7 @@ namespace Microsoft.Dafny { Expression arg = dtv.Arguments[i]; Type t = dtv.Ctor.Formals[i].Type; var bArg = TrExpr(arg); - args.Add(CondApplyBox(expr.tok, bArg, cce.NonNull(arg.Type), t)); + args.Add(translator.CondApplyBox(expr.tok, bArg, cce.NonNull(arg.Type), t)); } Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(dtv.tok, dtv.Ctor.FullName, predef.DatatypeType); return new Bpl.NAryExpr(dtv.tok, new Bpl.FunctionCall(id), args); @@ -8453,11 +8555,11 @@ namespace Microsoft.Dafny { } else if (expr is BoxingCastExpr) { BoxingCastExpr e = (BoxingCastExpr)expr; - return CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType); + return translator.CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType); } else if (expr is UnboxingCastExpr) { UnboxingCastExpr e = (UnboxingCastExpr)expr; - return CondApplyUnbox(e.tok, TrExpr(e.E), e.FromType, e.ToType); + return translator.CondApplyUnbox(e.tok, TrExpr(e.E), e.FromType, e.ToType); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression @@ -8575,7 +8677,7 @@ namespace Microsoft.Dafny { for (int i = 0; i < e.Args.Count; i++) { Expression ee = e.Args[i]; Type t = e.Function.Formals[i].Type; - args.Add(CondApplyBox(e.tok, TrExpr(ee), cce.NonNull(ee.Type), t)); + args.Add(translator.CondApplyBox(e.tok, TrExpr(ee), cce.NonNull(ee.Type), t)); } return args; } @@ -8595,56 +8697,12 @@ namespace Microsoft.Dafny { return fieldName; } - public Bpl.Expr CondApplyBox(IToken tok, Bpl.Expr e, Type fromType, Type toType) { - Contract.Requires(tok != null); - Contract.Requires(e != null); - Contract.Requires(fromType != null); - Contract.Ensures(Contract.Result() != null); - - if (!ModeledAsBoxType(fromType) && (toType == null || ModeledAsBoxType(toType))) { - return translator.FunctionCall(tok, BuiltinFunction.Box, null, e); - } else { - return e; - } - } - public Bpl.Expr BoxIfNecessary(IToken tok, Bpl.Expr e, Type fromType) { Contract.Requires(tok != null); Contract.Requires(e != null); Contract.Requires(fromType != null); Contract.Ensures(Contract.Result() != null); - - return CondApplyBox(tok, e, fromType, null); - } - - public Bpl.Expr CondApplyUnbox(IToken tok, Bpl.Expr e, Type fromType, Type toType) { - Contract.Requires(tok != null); - Contract.Requires(e != null); - Contract.Requires(fromType != null); - Contract.Requires(toType != null); - Contract.Ensures(Contract.Result() != null); - - if (ModeledAsBoxType(fromType) && !ModeledAsBoxType(toType)) { - return translator.FunctionCall(tok, BuiltinFunction.Unbox, translator.TrType(toType), e); - } else { - return e; - } - } - - public static bool ModeledAsBoxType(Type t) { - Contract.Requires(t != null); - while (true) { - TypeProxy tp = t as TypeProxy; - if (tp == null) { - break; - } else if (tp.T == null) { - // unresolved proxy - return false; - } else { - t = tp.T; - } - } - return t.IsTypeParameter; + return translator.BoxIfNecessary(tok, e, fromType); } public static Bpl.NAryExpr ReadHeap(IToken tok, Expr heap, Expr r, Expr f) { @@ -9422,7 +9480,7 @@ namespace Microsoft.Dafny { var ss = new List(); if (TrSplitExpr(bce.E, ss, position, heightLimit, etran)) { foreach (var s in ss) { - splits.Add(new SplitExprInfo(s.Kind, etran.CondApplyBox(s.E.tok, s.E, bce.FromType, bce.ToType))); + splits.Add(new SplitExprInfo(s.Kind, CondApplyBox(s.E.tok, s.E, bce.FromType, bce.ToType))); } return true; } @@ -9614,7 +9672,7 @@ namespace Microsoft.Dafny { var needsTokenAdjust = TrSplitNeedsTokenAdjustment(typeSpecializedBody); foreach (var s in ss) { if (s.IsChecked) { - var unboxedConjunct = etran.CondApplyUnbox(s.E.tok, s.E, typeSpecializedResultType, expr.Type); + var unboxedConjunct = CondApplyUnbox(s.E.tok, s.E, typeSpecializedResultType, expr.Type); var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct); var tok = needsTokenAdjust ? (IToken)new ForceCheckToken(typeSpecializedBody.tok) : (IToken)new NestedToken(fexp.tok, s.E.tok); var p = Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct); @@ -9624,7 +9682,7 @@ namespace Microsoft.Dafny { // body var trBody = etran.TrExpr(body); - trBody = etran.CondApplyUnbox(trBody.tok, trBody, f.ResultType, expr.Type); + trBody = CondApplyUnbox(trBody.tok, trBody, f.ResultType, expr.Type); // F#canCall(args) && F(args) && (b0 && b1 && b2) var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody)); splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr)); @@ -10102,7 +10160,7 @@ namespace Microsoft.Dafny { Bpl.Expr typeAntecedent = Bpl.Expr.True; foreach (Formal arg in ctor.Formals) { var instantiatedArgType = Resolver.SubstType(arg.Type, subst); - Bpl.Expr wh = GetWhereClause(arg.tok, etran.CondApplyUnbox(arg.tok, args[i], arg.Type, instantiatedArgType), instantiatedArgType, etran); + Bpl.Expr wh = GetWhereClause(arg.tok, CondApplyUnbox(arg.tok, args[i], arg.Type, instantiatedArgType), instantiatedArgType, etran); if (wh != null) { typeAntecedent = BplAnd(typeAntecedent, wh); } @@ -10183,7 +10241,7 @@ namespace Microsoft.Dafny { if (expr is LetExpr) { var e = (LetExpr)expr; - foreach (var v in e.Vars) { + foreach (var v in e.BoundVars) { fvs.Remove(v); } } else if (expr is ComprehensionExpr) { @@ -10443,18 +10501,18 @@ namespace Microsoft.Dafny { // Note, CreateBoundVarSubstitutions has the side effect of updating the substitution map. // For an Exact let expression, this is something that needs to be done after substituting // in the RHSs. - var newBoundVars = CreateBoundVarSubstitutions(e.Vars); - if (newBoundVars != e.Vars) { + var newCasePatterns = CreateCasePatternSubstitutions(e.LHSs); + if (newCasePatterns != e.LHSs) { anythingChanged = true; } var body = Substitute(e.Body); // undo any changes to substMap (could be optimized to do this only if newBoundVars != e.Vars) - foreach (var bv in e.Vars) { + foreach (var bv in e.BoundVars) { substMap.Remove(bv); } // Put things together if (anythingChanged || body != e.Body) { - newExpr = new LetExpr(e.tok, newBoundVars, rhss, body, e.Exact); + newExpr = new LetExpr(e.tok, newCasePatterns, rhss, body, e.Exact); } } else { var rhs = Substitute(e.RHSs[0]); @@ -10462,7 +10520,7 @@ namespace Microsoft.Dafny { if (rhs == e.RHSs[0] && body == e.Body) { return e; } - var newLet = new LetExpr(e.tok, e.Vars, new List{ rhs }, body, e.Exact); + var newLet = new LetExpr(e.tok, e.LHSs, new List{ rhs }, body, e.Exact); Expression d = translator.LetDesugaring(e); newLet.translationDesugaring = Substitute(d); var info = translator.letSuchThatExprInfo[e]; @@ -10571,7 +10629,7 @@ namespace Microsoft.Dafny { } /// - /// Return a list of bound variables, of the same length as vars but with possible substitutions. + /// Return a list of bound variables, of the same length as 'vars' but with possible substitutions. /// For any change necessary, update 'substMap' to reflect the new substitution; the caller is responsible for /// undoing these changes once the updated 'substMap' has been used. /// If no changes are necessary, the list returned is exactly 'vars' and 'substMap' is unchanged. @@ -10597,6 +10655,61 @@ namespace Microsoft.Dafny { return anythingChanged ? newBoundVars : vars; } + /// + /// Return a list of case patterns, of the same length as 'patterns' but with possible substitutions. + /// For any change necessary, update 'substMap' to reflect the new substitution; the caller is responsible for + /// undoing these changes once the updated 'substMap' has been used. + /// If no changes are necessary, the list returned is exactly 'patterns' and 'substMap' is unchanged. + /// + protected virtual List CreateCasePatternSubstitutions(List patterns) { + bool anythingChanged = false; + var newPatterns = new List(); + foreach (var pat in patterns) { + var newPat = SubstituteCasePattern(pat); + newPatterns.Add(newPat); + if (newPat != pat) { + anythingChanged = true; + } + } + return anythingChanged ? newPatterns : patterns; + } + CasePattern SubstituteCasePattern(CasePattern pat) { + Contract.Requires(pat != null); + if (pat.Var != null) { + var bv = pat.Var; + var tt = Resolver.SubstType(bv.Type, typeMap); + if (tt != bv.Type) { + var newBv = new BoundVar(pat.tok, pat.Id, tt); + // update substMap to reflect the new BoundVar substitutions + var ie = new IdentifierExpr(newBv.tok, newBv.Name); + ie.Var = newBv; // resolve here + ie.Type = newBv.Type; // resolve here + substMap.Add(bv, ie); + var newPat = new CasePattern(pat.tok, newBv); + newPat.AssembleExpr(null); + return newPat; + } + } else if (pat.Arguments != null) { + bool anythingChanged = false; + var newArgs = new List(); + foreach (var arg in pat.Arguments) { + var newArg = SubstituteCasePattern(arg); + newArgs.Add(newArg); + if (newArg != arg) { + anythingChanged = true; + } + } + if (anythingChanged) { + var patE = (DatatypeValue)pat.Expr; + var newPat = new CasePattern(pat.tok, pat.Id, newArgs); + newPat.Ctor = pat.Ctor; + newPat.AssembleExpr(patE.InferredTypeArgs.ConvertAll(tp => Resolver.SubstType(tp, typeMap))); + return newPat; + } + } + return pat; + } + protected List/*!*/ SubstituteExprList(List/*!*/ elist) { Contract.Requires(cce.NonNullElements(elist)); Contract.Ensures(cce.NonNullElements(Contract.Result>())); diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 472932c5..7da30e96 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -2289,8 +2289,32 @@ LetExpr.dfy(104,21): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon11_Then +LetExpr.dfy(248,19): Error: value assigned to a nat must be non-negative +Execution trace: + (0,0): anon0 + (0,0): anon5_Then +LetExpr.dfy(251,19): Error: value assigned to a nat must be non-negative +Execution trace: + (0,0): anon0 + (0,0): anon6_Then +LetExpr.dfy(253,24): Error: value assigned to a nat must be non-negative +Execution trace: + (0,0): anon0 + (0,0): anon6_Else +LetExpr.dfy(282,14): Error: RHS is not certain to look like the pattern 'Agnes' +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +LetExpr.dfy(299,42): Error: value assigned to a nat must be non-negative +Execution trace: + (0,0): anon0 + (0,0): anon6_Else +LetExpr.dfy(301,12): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon6_Else -Dafny program verifier finished with 28 verified, 2 errors +Dafny program verifier finished with 38 verified, 8 errors Dafny program verifier finished with 0 verified, 0 errors diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy index 3947737b..77bb4fad 100644 --- a/Test/dafny0/LetExpr.dfy +++ b/Test/dafny0/LetExpr.dfy @@ -216,3 +216,88 @@ class TrickySubstitution { s := old(var y :| y == w; y); } } + +datatype List = Nil | Cons(head: T, tail: List) + +method Q(list: List, anotherList: List) + requires list != Nil; +{ + var x := + var Cons(h, t) := list; + Cons(h, t); + var y := match anotherList + case Nil => (match anotherList case Nil => 5) + case Cons(h, t) => h; + assert list == x; + assert anotherList.Cons? ==> y == anotherList.head; + assert anotherList.Nil? ==> y == 5; +} + +// ------------- pattern LHSs --------------- + +datatype Tuple = Pair(0: T, 1: U) + +function method Together(x: int, y: bool): Tuple +{ + Pair(x, y) +} + +method LikeTogether() returns (z: int) +{ + if * { + z := var Pair(xx: nat, yy) := Together(-10, true); xx + 3; // error: int-to-nat failure + assert 0 <= z; // follows from the bogus type of xx + } else if * { + var t: nat := -30; // error: int-to-nat failure in assignment statement + } else { + z := var t: nat := -30; t; // error: int-to-nat failure in let expression + } +} + +method Mountain() returns (z: int, t: nat) +{ + z := var Pair(xx: nat, yy) := Together(10, true); xx + 3; + assert 0 <= z; +} + +function method Rainbow(tup: Tuple): int + ensures 0 <= Rainbow(tup); +{ + var Pair(left, right) := tup; right*right +} + +datatype Friend = Agnes(int) | Agatha(int) | Jermaine(int) | Jack(int) + +function Fr(x: int): Friend +{ + if x < 10 then Jermaine(x) else Agnes(x) +} + +method Friendly(n: nat) returns (ghost c: int) + ensures c == n; +{ + if n < 3 { + c := var Jermaine(y) := Fr(n); y; + } else { + c := var Agnes(y) := Fr(n); y; // error: Fr might return something other than an Agnes + } +} + +function method F_good(d: Tuple< + Tuple, + Tuple< Tuple, Tuple >>): int + requires 0 <= d.1.0.1 < 100; +{ + var p, Pair(Pair(b0, x), Pair(Pair(y0, y1: nat), Pair(b1, b2))), q: int := d.0, d, d.1.0.1; + assert q < 200; + p.1 + if b0 then x + y0 else x + y1 +} +function method F_bad(d: Tuple< + Tuple, + Tuple< Tuple, Tuple >>): int +{ + var p, Pair(Pair(b0, x), Pair(Pair(y0, y1: nat), Pair(b1, b2))), q: int // error: int-to-nat failure + := d.0, d, d.1.0.1; + assert q < 200; // error: assertion failure + p.1 + if b0 then x + y0 else x + y1 +} -- cgit v1.2.3