diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-09-10 12:50:52 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-09-10 12:50:52 -0700 |
| commit | 37b59d5df03233b9c777252a0e96a5c1dfe61877 (patch) | |
| tree | b63c3b981442d5126bc5fd6eba275cad896e2934 /Dafny | |
| parent | 575a7b1acc5404210b3e2d865ffae660d7ab651e (diff) | |
| parent | dde158110ed1e9f2517475c7fd6ebdd42c4940e5 (diff) | |
Merge
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/Resolver.cs | 10 | ||||
| -rw-r--r-- | Dafny/Translator.cs | 4 |
2 files changed, 13 insertions, 1 deletions
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 38766b58..53449979 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -1393,6 +1393,16 @@ namespace Microsoft.Dafny default:
break;
}
+ } else if (expr is MatchExpr) {
+ var e = (MatchExpr)expr;
+ CoPredicateChecks(e.Source, context, CallingPosition.Neither);
+ e.Cases.Iter(kase => CoPredicateChecks(kase.Body, context, cp));
+ return;
+ } else if (expr is ITEExpr) {
+ var e = (ITEExpr)expr;
+ CoPredicateChecks(e.Test, context, CallingPosition.Neither);
+ CoPredicateChecks(e.Thn, context, cp);
+ CoPredicateChecks(e.Els, context, cp);
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
CoPredicateChecks(e.Body, context, cp);
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 8ecd93e7..f2011b72 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -8089,7 +8089,9 @@ namespace Microsoft.Dafny { Bpl.Expr Conclusion = new Bpl.ForallExpr(tok, bvs, new Bpl.Trigger(tok, true, new ExprSeq(etran.TrExpr(C))),
Bpl.Expr.Imp(preStuff, etran.TrExpr(C)));
// Now for the antecedent of the axiom
- // TODO: if e.Body uses a 'match' expression, first desugar it into an ordinary expression
+ if (coPredicate.Body is MatchExpr) {
+ return Bpl.Expr.True; // TODO: if coPredicate.Body uses a 'match' expression, first desugar it into an ordinary expression
+ }
var s = new CoinductionSubstituter(coPredicate, receiverReplacement, substMap, pre, boundVars, receiverReplacement, args);
var body = s.Substitute(coPredicate.Body);
Bpl.Expr Antecedent = new Bpl.ForallExpr(tok, bvs, Bpl.Expr.Imp(preStuff, etran.TrExpr(body)));
|