diff options
author | 2011-11-09 17:27:36 -0800 | |
---|---|---|
committer | 2011-11-09 17:27:36 -0800 | |
commit | cea05485e8f58b1831bc5a1c68178164927f1c5b (patch) | |
tree | 5487b3c5829be18581a7978b80efa537b444e782 /Source | |
parent | 29524a38ed773a399011f42526c80ed790ce83d6 (diff) |
Dafny: added assert/assume expressions
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Dafny/Compiler.cs | 4 | ||||
-rw-r--r-- | Source/Dafny/Dafny.atg | 10 | ||||
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 47 | ||||
-rw-r--r-- | Source/Dafny/Parser.cs | 53 | ||||
-rw-r--r-- | Source/Dafny/Printer.cs | 10 | ||||
-rw-r--r-- | Source/Dafny/Resolver.cs | 14 | ||||
-rw-r--r-- | Source/Dafny/Translator.cs | 64 |
7 files changed, 186 insertions, 16 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 61b0398f..de863e39 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1767,6 +1767,10 @@ namespace Microsoft.Dafny { wr.Write("return Dafny.Set<{0}>.FromCollection(_coll); ", typeName);
wr.Write("})()");
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ TrExpr(e.Body);
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
wr.Write("(");
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index fa857aad..8a9108f0 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1205,13 +1205,19 @@ EndlessExpression<out Expression e> Expression e0, e1;
e = dummyExpr;
.)
- ( "if" (. x = t; .)
+ ( "if" (. x = t; .)
Expression<out e>
"then" Expression<out e0>
- "else" Expression<out e1> (. e = new ITEExpr(x, e, e0, e1); .)
+ "else" Expression<out e1> (. e = new ITEExpr(x, e, e0, e1); .)
| MatchExpression<out e>
| QuantifierGuts<out e>
| ComprehensionExpr<out e>
+ | "assert" (. x = t; .)
+ Expression<out e0> ";"
+ Expression<out e1> (. e = new AssertExpr(x, e0, e1); .)
+ | "assume" (. x = t; .)
+ Expression<out e0> ";"
+ Expression<out e1> (. e = new AssumeExpr(x, e0, e1); .)
)
.
MatchExpression<out Expression/*!*/ e>
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index bf8eb6b0..04b6b00e 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2721,7 +2721,52 @@ namespace Microsoft.Dafny { }
}
- public class ITEExpr : Expression {
+ public abstract class PredicateExpr : Expression
+ {
+ public readonly Expression Guard;
+ public readonly Expression Body;
+ public PredicateExpr(IToken tok, Expression guard, Expression body)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(guard != null);
+ Contract.Requires(body != null);
+ Guard = guard;
+ Body = body;
+ }
+ public abstract string Kind { get; }
+
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Guard;
+ yield return Body;
+ }
+ }
+ }
+
+ public class AssertExpr : PredicateExpr
+ {
+ public AssertExpr(IToken tok, Expression guard, Expression body)
+ : base(tok, guard, body) {
+ Contract.Requires(tok != null);
+ Contract.Requires(guard != null);
+ Contract.Requires(body != null);
+ }
+ public override string Kind { get { return "assert"; } }
+ }
+
+ public class AssumeExpr : PredicateExpr
+ {
+ public AssumeExpr(IToken tok, Expression guard, Expression body)
+ : base(tok, guard, body) {
+ Contract.Requires(tok != null);
+ Contract.Requires(guard != null);
+ Contract.Requires(body != null);
+ }
+ public override string Kind { get { return "assume"; } }
+ }
+
+ public class ITEExpr : Expression
+ {
public readonly Expression Test;
public readonly Expression Thn;
public readonly Expression Els;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 2fc50c37..0dc30e8a 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1789,7 +1789,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 38: case 55: case 61: case 98: case 99: case 100: case 101: {
+ case 38: case 55: case 61: case 62: case 63: case 98: case 99: case 100: case 101: {
EndlessExpression(out e);
break;
}
@@ -1846,7 +1846,8 @@ List<Expression/*!*/>/*!*/ decreases) { Expression e0, e1;
e = dummyExpr;
- if (la.kind == 55) {
+ switch (la.kind) {
+ case 55: {
Get();
x = t;
Expression(out e);
@@ -1855,13 +1856,40 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(56);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
- } else if (la.kind == 61) {
+ break;
+ }
+ case 61: {
MatchExpression(out e);
- } else if (StartOf(15)) {
+ break;
+ }
+ case 98: case 99: case 100: case 101: {
QuantifierGuts(out e);
- } else if (la.kind == 38) {
+ break;
+ }
+ case 38: {
ComprehensionExpr(out e);
- } else SynErr(133);
+ break;
+ }
+ case 62: {
+ Get();
+ x = t;
+ Expression(out e0);
+ Expect(17);
+ Expression(out e1);
+ e = new AssertExpr(x, e0, e1);
+ break;
+ }
+ case 63: {
+ Get();
+ x = t;
+ Expression(out e0);
+ Expect(17);
+ Expression(out e1);
+ e = new AssumeExpr(x, e0, e1);
+ break;
+ }
+ default: SynErr(133); break;
+ }
}
void DottedIdentifiersAndFunction(out Expression e) {
@@ -2014,7 +2042,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expression(out e);
e = new MultiSetFormingExpr(x, e);
Expect(34);
- } else if (StartOf(16)) {
+ } else if (StartOf(15)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
} else SynErr(138);
}
@@ -2233,7 +2261,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(22);
Expect(1);
aName = t.val;
- if (StartOf(17)) {
+ if (StartOf(16)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 19) {
@@ -2263,18 +2291,17 @@ List<Expression/*!*/>/*!*/ decreases) { {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
{x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, T,T,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},
- {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
+ {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
};
} // end Parser
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 7f7ba963..10099bf4 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1054,6 +1054,16 @@ namespace Microsoft.Dafny { } else if (expr is WildcardExpr) {
wr.Write("*");
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ bool parensNeeded = !isRightmost;
+ if (parensNeeded) { wr.Write("("); }
+ wr.Write("{0} ", e.Kind);
+ PrintExpression(e.Guard);
+ wr.Write("; ");
+ PrintExpression(e.Body);
+ if (parensNeeded) { wr.Write(")"); }
+
} else if (expr is ITEExpr) {
ITEExpr ite = (ITEExpr)expr;
bool parensNeeded = !isRightmost;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 2d3ddcca..c7fb8481 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2823,6 +2823,17 @@ namespace Microsoft.Dafny { } else if (expr is WildcardExpr) {
expr.Type = new SetType(new ObjectType());
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ ResolveExpression(e.Guard, twoState);
+ Contract.Assert(e.Guard.Type != null); // follows from postcondition of ResolveExpression
+ ResolveExpression(e.Body, twoState);
+ Contract.Assert(e.Body.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Guard.Type, Type.Bool)) {
+ Error(expr, "guard condition in {0} expression must be a boolean (instead got {1})", e.Kind, e.Guard.Type);
+ }
+ expr.Type = e.Body.Type;
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
ResolveExpression(e.Test, twoState);
@@ -3932,6 +3943,9 @@ namespace Microsoft.Dafny { return (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));
} else if (expr is WildcardExpr) {
return false;
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ return UsesSpecFeatures(e.Body);
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
return UsesSpecFeatures(e.Test) || UsesSpecFeatures(e.Thn) || UsesSpecFeatures(e.Els);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index e455561a..37f80bf1 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1789,6 +1789,16 @@ namespace Microsoft.Dafny { total = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, total));
}
return total;
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ Bpl.Expr gTotal = IsTotal(e.Guard, etran);
+ Bpl.Expr g = etran.TrExpr(e.Guard);
+ Bpl.Expr bTotal = IsTotal(e.Body, etran);
+ if (e is AssertExpr) {
+ return BplAnd(gTotal, BplAnd(g, bTotal));
+ } else {
+ return BplAnd(gTotal, Bpl.Expr.Imp(g, bTotal));
+ }
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
Bpl.Expr total = IsTotal(e.Test, etran);
@@ -1925,6 +1935,16 @@ namespace Microsoft.Dafny { total = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, total));
}
return total;
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ Bpl.Expr gCanCall = CanCallAssumption(e.Guard, etran);
+ Bpl.Expr g = etran.TrExpr(e.Guard);
+ Bpl.Expr bCanCall = CanCallAssumption(e.Body, etran);
+ if (e is AssertExpr) {
+ return BplAnd(gCanCall, BplAnd(g, bCanCall));
+ } else {
+ return BplAnd(gCanCall, Bpl.Expr.Imp(g, bCanCall));
+ }
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
Bpl.Expr total = CanCallAssumption(e.Test, etran);
@@ -2316,6 +2336,27 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(range), b.Collect(expr.tok), null, null));
}
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ CheckWellformed(e.Guard, options, locals, builder, etran);
+ if (e is AssertExpr) {
+ bool splitHappened;
+ var ss = TrSplitExpr(e.Guard, etran, out splitHappened);
+ if (!splitHappened) {
+ builder.Add(Assert(e.Guard.tok, etran.TrExpr(e.Guard), "condition in assert expression might not hold"));
+ } else {
+ foreach (var split in ss) {
+ if (!split.IsFree) {
+ builder.Add(AssertNS(split.E.tok, split.E, "condition in assert expression might not hold"));
+ }
+ }
+ builder.Add(new Bpl.AssumeCmd(e.tok, etran.TrExpr(e.Guard)));
+ }
+ } else {
+ builder.Add(new Bpl.AssumeCmd(e.tok, etran.TrExpr(e.Guard)));
+ }
+ CheckWellformed(e.Body, options, locals, builder, etran);
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
CheckWellformed(e.Test, options, locals, builder, etran);
@@ -5547,6 +5588,10 @@ namespace Microsoft.Dafny { return new Bpl.LambdaExpr(expr.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, exst);
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ return TrExpr(e.Body);
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
Bpl.Expr g = TrExpr(e.Test);
@@ -6349,6 +6394,10 @@ namespace Microsoft.Dafny { var e = (ConcreteSyntaxExpression)expr;
return TrSplitExpr(e.ResolvedExpression, splits, position, expandFunctions, etran);
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ return TrSplitExpr(e.Body, splits, position, expandFunctions, etran);
+
} else if (expr is UnaryExpr) {
var e = (UnaryExpr)expr;
if (e.Op == UnaryExpr.Opcode.Not) {
@@ -6819,6 +6868,11 @@ namespace Microsoft.Dafny { }
return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) ||
VarOccursInArgumentToRecursiveFunction(e.E1, n, q);
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ // ignore the guard
+ return VarOccursInArgumentToRecursiveFunction(e.Body, n);
+
} else if (expr is ITEExpr) {
var e = (ITEExpr)expr;
return VarOccursInArgumentToRecursiveFunction(e.Test, n, subExprIsProminent) || // test is not "prominent"
@@ -7044,6 +7098,16 @@ namespace Microsoft.Dafny { Contract.Assume(false); // unexpected ComprehensionExpr
}
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ Expression g = Substitute(e.Guard, receiverReplacement, substMap);
+ Expression b = Substitute(e.Body, receiverReplacement, substMap);
+ if (expr is AssertExpr) {
+ newExpr = new AssertExpr(e.tok, g, b);
+ } else {
+ newExpr = new AssumeExpr(e.tok, g, b);
+ }
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
Expression test = Substitute(e.Test, receiverReplacement, substMap);
|