diff options
| author |  Rustan Leino <unknown> | 2014-01-08 18:47:33 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-01-08 18:47:33 -0800 |
| commit | 041a1a226a96ba55ff22251eb98666241a1d769a (patch) | |
| tree | 88a3d00b32dcb02883fb85293d27f73ae9c3cfec | |
| parent | 621178a0da1fee756dcf6dd713c8ef5b14530800 (diff) | |
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.
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 1 | ||||
| -rw-r--r-- | Source/Dafny/Cloner.cs | 11 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 189 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 66 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 85 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 83 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 29 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 127 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 329 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 26 | ||||
| -rw-r--r-- | 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,Result>(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<Expression, int> uniqueAstNumbers = new Dictionary<Expression, int>();
+ 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<SourceType, TargetType>(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<out VarDecl var, bool isGhost> ]
(. var = new VarDecl(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
.
-IdentTypeOptionalG<out BoundVar var, bool isGhost>
-= (. Contract.Ensures(Contract.ValueAtReturn(out var) != null);
- .)
- IdentTypeOptional<out var>
- (. var.IsGhost = isGhost; .)
- .
IdentTypeOptional<out BoundVar var>
= (. Contract.Ensures(Contract.ValueAtReturn(out var) != null);
IToken id; Type ty; Type optType = null;
@@ -1916,28 +1915,37 @@ StmtInExpr<out Statement s> LetExpr<out Expression e, bool allowSemi>
= (. IToken x = null;
- e = dummyExpr;
- BoundVar d;
- List<BoundVar> letVars; List<Expression> letRHSs;
- bool exact = true;
bool isGhost = false;
+ var letLHSs = new List<CasePattern>();
+ var letRHSs = new List<Expression>();
+ CasePattern pat;
+ bool exact = true;
+ e = dummyExpr;
.)
[ "ghost" (. isGhost = true; x = t; .)
]
- "var" (. if (!isGhost) { x = t; }
- letVars = new List<BoundVar>();
- letRHSs = new List<Expression>(); .)
- IdentTypeOptionalG<out d, isGhost> (. letVars.Add(d); .)
- { "," IdentTypeOptionalG<out d, isGhost> (. letVars.Add(d); .)
+ "var" (. if (!isGhost) { x = t; } .)
+ CasePattern<out pat> (. if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
+ letLHSs.Add(pat);
+ .)
+ { "," CasePattern<out pat> (. 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<out e, false> (. letRHSs.Add(e); .)
{ "," Expression<out e, false> (. letRHSs.Add(e); .)
}
";"
- Expression<out e, allowSemi> (. e = new LetExpr(x, letVars, letRHSs, e, exact); .)
+ Expression<out e, allowSemi> (. e = new LetExpr(x, letLHSs, letRHSs, e, exact); .)
.
NamedExpr<out Expression e, bool allowSemi>
@@ -1981,6 +1989,30 @@ CaseExpression<out MatchCaseExpr c, bool allowSemi> "=>"
Expression<out body, allowSemi> (. c = new MatchCaseExpr(x, id.val, arguments, body); .)
.
+CasePattern<out CasePattern pat>
+= (. IToken id; List<CasePattern> arguments;
+ BoundVar bv;
+ pat = null;
+ .)
+ ( IF(IsIdentParen())
+ Ident<out id>
+ "(" (. arguments = new List<CasePattern>(); .)
+ [ CasePattern<out pat> (. arguments.Add(pat); .)
+ { "," CasePattern<out pat> (. arguments.Add(pat); .)
+ }
+ ]
+ ")" (. pat = new CasePattern(id, id.val, arguments); .)
+
+ | IdentTypeOptional<out bv> (. // 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<out Expression e>
= (. IToken id; IToken openParen = null;
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<BoundVar> Vars;
+ public readonly List<CasePattern> LHSs;
public readonly List<Expression> 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<BoundVar> vars, List<Expression> rhss, Expression body, bool exact)
+ public LetExpr(IToken tok, List<CasePattern> lhss, List<Expression> 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<BoundVar> 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 { }
}
+ /// <summary>
+ /// 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.
+ /// </summary>
+ 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<CasePattern> Arguments;
+
+ public Expression Expr; // an r-value version of the CasePattern; filled in by resolution
+
+ public CasePattern(IToken tok, string id, [Captured] List<CasePattern> 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;
+ }
+
+ /// <summary>
+ /// Sets the Expr field. Assumes the CasePattern and its arguments to have been successfully resolved, except for assigning
+ /// to Expr.
+ /// </summary>
+ public void AssembleExpr(List<Type> 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<BoundVar> 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<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void LetExpr(out Expression e, bool allowSemi) {
IToken x = null;
- e = dummyExpr;
- BoundVar d;
- List<BoundVar> letVars; List<Expression> letRHSs;
- bool exact = true;
bool isGhost = false;
+ var letLHSs = new List<CasePattern>();
+ var letRHSs = new List<Expression>();
+ 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<BoundVar>();
- letRHSs = new List<Expression>();
- 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new NamedExpr(x, d.val, expr);
}
+ void CasePattern(out CasePattern pat) {
+ IToken id; List<CasePattern> arguments;
+ BoundVar bv;
+ pat = null;
+
+ if (IsIdentParen()) {
+ Ident(out id);
+ Expect(10);
+ arguments = new List<CasePattern>();
+ 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<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
@@ -3425,7 +3459,7 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<BoundVar> 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<IToken> 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<string, object> memberNamesUsed = new Dictionary<string, object>(); // this is really a set
+ ISet<string> memberNamesUsed = new HashSet<string>();
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<string, object>(); // 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<string>(); // 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<string, object> memberNamesUsed = new Dictionary<string, object>(); // this is really a set
+ ISet<string> memberNamesUsed = new HashSet<string>();
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<TypeParameter, Type>();
+ 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<Type> gt = new List<Type>(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<IVariable, Expression>();
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<Variable>();
- Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.Vars, bvars);
+ Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars.ToList<BoundVar>(), 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<IVariable, Expression> 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<Bpl.Expr> { 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<Bpl.Expr> { rhs });
+ var de = CondApplyUnbox(pat.tok, r, dtor.Type, arg.Expr.Type);
+ CheckCasePatternShape(arg, de, builder);
+ }
+ }
+ }
+
Bpl.Expr/*!*/ CanCallAssumption(List<Expression/*!*/>/*!*/ 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<IVariable, Expression>();
- 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<BoundVar>(), 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<BoundVar> lhsVars = e.BoundVars.ToList<BoundVar>();
+ var substMap = SetupBoundVarsAsLocals(lhsVars, builder, locals, etran);
var rhs = Substitute(e.RHSs[0], null, substMap);
CheckWellformed(rhs, options, locals, builder, etran);
- List<Tuple<List<BoundVar>, Expression>> partialGuesses = GeneratePartialGuesses(e.Vars, e.RHSs[0]);
+ List<Tuple<List<BoundVar>, 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<Bpl.IdentifierExpr>();
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<Bpl.Expr>() != 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<Bpl.Expr>() != 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<Bpl.Expr>() != 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 ----------------------------------------------------------------------------
/// <summary>
@@ -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<Bpl.IdentifierExpr>();
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<IVariable>();
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<Variable> formals = info.GAsVars(this, true, out ante, null);
@@ -7396,7 +7499,7 @@ namespace Microsoft.Dafny { }
Bpl.Trigger tr = null;
Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
- 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<Bpl.Expr> { call }, tr);
@@ -7428,13 +7531,13 @@ namespace Microsoft.Dafny { {
var etran = new ExpressionTranslator(this, predef, e.tok);
var rhss = new List<Expression>();
- 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<IVariable, Expression>();
- 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<Bpl.Expr> { 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<Bpl.Expr>() != 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<Bpl.Expr>() != 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<Bpl.Expr>() != 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<SplitExprInfo>();
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<Expression>{ rhs }, body, e.Exact);
+ var newLet = new LetExpr(e.tok, e.LHSs, new List<Expression>{ 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 { }
/// <summary>
- /// 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;
}
+ /// <summary>
+ /// 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.
+ /// </summary>
+ protected virtual List<CasePattern> CreateCasePatternSubstitutions(List<CasePattern> patterns) {
+ bool anythingChanged = false;
+ var newPatterns = new List<CasePattern>();
+ 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<CasePattern>();
+ 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<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist) {
Contract.Requires(cce.NonNullElements(elist));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));
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<T> = Nil | Cons(head: T, tail: List)
+
+method Q(list: List<int>, anotherList: List<int>)
+ 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<T,U> = Pair(0: T, 1: U)
+
+function method Together(x: int, y: bool): Tuple<int, bool>
+{
+ 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<X>(tup: Tuple<X, int>): 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<bool, int>,
+ Tuple< Tuple<int,int>, Tuple<bool,bool> >>): 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<bool, int>,
+ Tuple< Tuple<int,int>, Tuple<bool,bool> >>): 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
+}
|