diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 12:49:11 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 12:49:11 -0700 |
| commit | 5734c8b39065b73835092fc5ede4a7c589374be2 (patch) | |
| tree | ce43eb7340e857c0a0b342c9e4486168b7339c9a /Source/Dafny/Translator.cs | |
| parent | 4b7ef1b817fe00bc32294b75797e7e264e2edbdd (diff) | |
| parent | 270b34fc36dcfc781e8f49df5339cb2e10e69828 (diff) | |
Merge.
Diffstat (limited to 'Source/Dafny/Translator.cs')
| -rw-r--r-- | Source/Dafny/Translator.cs | 64 |
1 files changed, 31 insertions, 33 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index e39b777d..8200f254 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -7683,39 +7683,37 @@ namespace Microsoft.Dafny { }
var missingBounds = new List<BoundVar>();
- var bounds = Resolver.DiscoverBounds(x.tok, new List<BoundVar>() { x }, expr, true, true, missingBounds, reporter);
- if (missingBounds.Count == 0) {
- foreach (var bound in bounds) {
- if (bound is ComprehensionExpr.IntBoundedPool) {
- var bnd = (ComprehensionExpr.IntBoundedPool)bound;
- if (bnd.LowerBound != null) yield return bnd.LowerBound;
- if (bnd.UpperBound != null) yield return Expression.CreateDecrement(bnd.UpperBound, 1);
- } else if (bound is ComprehensionExpr.SubSetBoundedPool) {
- var bnd = (ComprehensionExpr.SubSetBoundedPool)bound;
- yield return bnd.UpperBound;
- } else if (bound is ComprehensionExpr.SuperSetBoundedPool) {
- var bnd = (ComprehensionExpr.SuperSetBoundedPool)bound;
- yield return bnd.LowerBound;
- } else if (bound is ComprehensionExpr.SetBoundedPool) {
- var st = ((ComprehensionExpr.SetBoundedPool)bound).Set.Resolved;
- if (st is DisplayExpression) {
- var display = (DisplayExpression)st;
- foreach (var el in display.Elements) {
- yield return el;
- }
- } else if (st is MapDisplayExpr) {
- var display = (MapDisplayExpr)st;
- foreach (var maplet in display.Elements) {
- yield return maplet.A;
- }
+ var bounds = Resolver.DiscoverAllBounds_SingleVar(x, expr);
+ foreach (var bound in bounds) {
+ if (bound is ComprehensionExpr.IntBoundedPool) {
+ var bnd = (ComprehensionExpr.IntBoundedPool)bound;
+ if (bnd.LowerBound != null) yield return bnd.LowerBound;
+ if (bnd.UpperBound != null) yield return Expression.CreateDecrement(bnd.UpperBound, 1);
+ } else if (bound is ComprehensionExpr.SubSetBoundedPool) {
+ var bnd = (ComprehensionExpr.SubSetBoundedPool)bound;
+ yield return bnd.UpperBound;
+ } else if (bound is ComprehensionExpr.SuperSetBoundedPool) {
+ var bnd = (ComprehensionExpr.SuperSetBoundedPool)bound;
+ yield return bnd.LowerBound;
+ } else if (bound is ComprehensionExpr.SetBoundedPool) {
+ var st = ((ComprehensionExpr.SetBoundedPool)bound).Set.Resolved;
+ if (st is DisplayExpression) {
+ var display = (DisplayExpression)st;
+ foreach (var el in display.Elements) {
+ yield return el;
}
- } else if (bound is ComprehensionExpr.SeqBoundedPool) {
- var sq = ((ComprehensionExpr.SeqBoundedPool)bound).Seq.Resolved;
- var display = sq as DisplayExpression;
- if (display != null) {
- foreach (var el in display.Elements) {
- yield return el;
- }
+ } else if (st is MapDisplayExpr) {
+ var display = (MapDisplayExpr)st;
+ foreach (var maplet in display.Elements) {
+ yield return maplet.A;
+ }
+ }
+ } else if (bound is ComprehensionExpr.SeqBoundedPool) {
+ var sq = ((ComprehensionExpr.SeqBoundedPool)bound).Seq.Resolved;
+ var display = sq as DisplayExpression;
+ if (display != null) {
+ foreach (var el in display.Elements) {
+ yield return el;
}
}
}
@@ -11629,8 +11627,8 @@ namespace Microsoft.Dafny { } else if (expr is LambdaExpr) {
var e = (LambdaExpr)expr;
-
return TrLambdaExpr(e);
+
} else if (expr is StmtExpr) {
var e = (StmtExpr)expr;
return TrExpr(e.E);
|