diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-08-30 11:22:37 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-08-30 11:22:37 -0700 |
| commit | dde158110ed1e9f2517475c7fd6ebdd42c4940e5 (patch) | |
| tree | 5b7445f25b630a68cb5021faaf480c9d3ac69879 /Dafny | |
| parent | 4a522f9458decdf7865be79596788c50e9145faf (diff) | |
Dafny: allow more corecursive calls for copredicates
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 5879995a..f3fe1bf5 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -1199,6 +1199,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 c8cc11f6..9966b915 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -8075,7 +8075,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)));
|