diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-02 18:18:07 -0800 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-02 18:18:07 -0800 |
| commit | a99b88779bd11f102ef69d94bc284d2a35b53888 (patch) | |
| tree | 64ef21b8236a5998818d93f962a4a747784205ac /Dafny | |
| parent | 4fdb83b82eb6949fcfb7e46e0010dc4b9c95c62f (diff) | |
| parent | 8bcdbb318c0c61b1148705accccb294906cdffb1 (diff) | |
Merge
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/Translator.cs | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index c0a56d05..40d7c266 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -2406,10 +2406,21 @@ namespace Microsoft.Dafny { } else if (expr is LetExpr) {
var e = (LetExpr)expr;
- foreach (var rhs in e.RHSs) {
- CheckWellformed(rhs, options, locals, builder, etran);
+
+ 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 v = new Bpl.LocalVariable(vr.tok, new Bpl.TypedIdent(vr.tok, vr.UniqueName, tp));
+ locals.Add(v);
+ var lhs = new Bpl.IdentifierExpr(vr.tok, vr.UniqueName, tp);
+
+ CheckWellformedWithResult(e.RHSs[i], options, lhs, vr.Type, locals, builder, etran);
+ substMap.Add(vr, new BoogieWrapper(lhs, vr.Type));
}
- CheckWellformedWithResult(etran.GetSubstitutedBody(e), options, result, resultType, locals, builder, etran);
+ CheckWellformedWithResult(Substitute(e.Body, null, substMap), options, result, resultType, locals, builder, etran);
+ result = null;
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
|