diff options
Diffstat (limited to 'Source/Dafny/Translator.cs')
| -rw-r--r-- | Source/Dafny/Translator.cs | 151 |
1 files changed, 80 insertions, 71 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 9466f18a..b2b63a07 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -7232,7 +7232,9 @@ namespace Microsoft.Dafny { AddComment(builder, stmt, "assume statement");
AssumeStmt s = (AssumeStmt)stmt;
TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
- builder.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr), etran.TrAttributes(stmt.Attributes, null)));
+ // we need to increase fuel for quantifier expr and functions that contain quantifier expr in the assume context.
+ var existEtran = etran.LayerOffset(1);
+ builder.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr, null, existEtran, existEtran), etran.TrAttributes(stmt.Attributes, null)));
}
this.fuelContext = FuelSetting.PopFuelContext();
} else if (stmt is PrintStmt) {
@@ -8348,7 +8350,7 @@ namespace Microsoft.Dafny { }
var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type);
var p = Substitute(e, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the call's actuals for the method's formals
- qq = callEtran.TrExpr(p, initEtran);
+ qq = callEtran.TrExpr(p, initEtran, null, null);
exporter.Add(TrAssumeCmd(tok, qq));
}
} else {
@@ -8485,7 +8487,7 @@ namespace Microsoft.Dafny { Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
var p = Substitute(s.ForallExpressions[0], null, substMap);
- Bpl.Expr qq = etran.TrExpr(p, initEtran);
+ Bpl.Expr qq = etran.TrExpr(p, initEtran, null, null);
if (s.BoundVars.Count != 0) {
exporter.Add(TrAssumeCmd(s.Tok, qq));
} else {
@@ -10916,9 +10918,9 @@ namespace Microsoft.Dafny { /// then show up in an error message).
/// </summary>
public Bpl.Expr TrExpr(Expression expr) {
- return TrExpr(expr, null);
+ return TrExpr(expr, null, null, null);
}
- public Bpl.Expr TrExpr(Expression expr, ExpressionTranslator etran)
+ public Bpl.Expr TrExpr(Expression expr, ExpressionTranslator initEtran, ExpressionTranslator funcEtran, ExpressionTranslator existEtran)
{
Contract.Requires(expr != null);
Contract.Requires(predef != null);
@@ -10982,7 +10984,7 @@ namespace Microsoft.Dafny { args.Add(Old.HeapExpr);
}
foreach (var arg in e.Args) {
- args.Add(TrExpr(arg));
+ args.Add(TrExpr(arg, initEtran, funcEtran, existEtran));
}
return new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args);
@@ -10990,7 +10992,7 @@ namespace Microsoft.Dafny { SetDisplayExpr e = (SetDisplayExpr)expr;
Bpl.Expr s = translator.FunctionCall(expr.tok, e.Finite ? BuiltinFunction.SetEmpty : BuiltinFunction.ISetEmpty, predef.BoxType);
foreach (Expression ee in e.Elements) {
- Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type));
+ Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee, initEtran, funcEtran, existEtran), cce.NonNull(ee.Type));
s = translator.FunctionCall(expr.tok, e.Finite ? BuiltinFunction.SetUnionOne : BuiltinFunction.ISetUnionOne, predef.BoxType, s, ss);
}
return s;
@@ -10999,7 +11001,7 @@ namespace Microsoft.Dafny { MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;
Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEmpty, predef.BoxType);
foreach (Expression ee in e.Elements) {
- Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type));
+ Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee, initEtran, funcEtran, existEtran), cce.NonNull(ee.Type));
s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetUnionOne, predef.BoxType, s, ss);
}
return s;
@@ -11010,7 +11012,7 @@ namespace Microsoft.Dafny { Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);
bool isLit = true;
foreach (Expression ee in e.Elements) {
- var rawElement = TrExpr(ee);
+ var rawElement = TrExpr(ee, initEtran, funcEtran, existEtran);
isLit = isLit && translator.IsLit(rawElement);
Bpl.Expr elt = BoxIfNecessary(expr.tok, rawElement, ee.Type);
s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, predef.BoxType, s, elt);
@@ -11026,8 +11028,8 @@ namespace Microsoft.Dafny { Bpl.Type maptype = predef.MapType(expr.tok, e.Finite, predef.BoxType, predef.BoxType);
Bpl.Expr s = translator.FunctionCall(expr.tok, e.Finite ? BuiltinFunction.MapEmpty : BuiltinFunction.IMapEmpty, predef.BoxType);
foreach (ExpressionPair p in e.Elements) {
- Bpl.Expr elt = BoxIfNecessary(expr.tok, TrExpr(p.A), cce.NonNull(p.A.Type));
- Bpl.Expr elt2 = BoxIfNecessary(expr.tok, TrExpr(p.B), cce.NonNull(p.B.Type));
+ Bpl.Expr elt = BoxIfNecessary(expr.tok, TrExpr(p.A, initEtran, funcEtran, existEtran), cce.NonNull(p.A.Type));
+ Bpl.Expr elt2 = BoxIfNecessary(expr.tok, TrExpr(p.B, initEtran, funcEtran, existEtran), cce.NonNull(p.B.Type));
s = translator.FunctionCall(expr.tok, e.Finite ? "Map#Build" : "IMap#Build", maptype, s, elt, elt2);
}
return s;
@@ -11036,7 +11038,7 @@ namespace Microsoft.Dafny { var e = (MemberSelectExpr)expr;
return e.MemberSelectCase(
field => {
- Bpl.Expr obj = TrExpr(e.Obj);
+ Bpl.Expr obj = TrExpr(e.Obj, initEtran, funcEtran, existEtran);
Bpl.Expr result;
if (field.IsMutable) {
result = ReadHeap(expr.tok, HeapExpr, obj, new Bpl.IdentifierExpr(expr.tok, translator.GetField(field)));
@@ -11063,7 +11065,7 @@ namespace Microsoft.Dafny { });
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
- Bpl.Expr seq = TrExpr(e.Seq);
+ Bpl.Expr seq = TrExpr(e.Seq, initEtran, funcEtran, existEtran);
var seqType = e.Seq.Type.NormalizeExpand();
Type elmtType = null;
Type domainType = null;
@@ -11083,14 +11085,14 @@ namespace Microsoft.Dafny { } else { Contract.Assert(false); }
Bpl.Type elType = translator.TrType(elmtType);
Bpl.Type dType = translator.TrType(domainType);
- Bpl.Expr e0 = e.E0 == null ? null : TrExpr(e.E0);
- Bpl.Expr e1 = e.E1 == null ? null : TrExpr(e.E1);
+ Bpl.Expr e0 = e.E0 == null ? null : TrExpr(e.E0, initEtran, funcEtran, existEtran);
+ Bpl.Expr e1 = e.E1 == null ? null : TrExpr(e.E1, initEtran, funcEtran, existEtran);
if (e.SelectOne) {
Contract.Assert(e1 == null);
Bpl.Expr x;
if (seqType.IsArrayType) {
Bpl.Expr fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.IndexField, null, e0);
- x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Seq), fieldName);
+ x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Seq, initEtran, funcEtran, existEtran), fieldName);
} else if (seqType is SeqType) {
x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0);
} else if (seqType is MapType) {
@@ -11099,7 +11101,7 @@ namespace Microsoft.Dafny { x = translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), seq);
x = Bpl.Expr.Select(x, BoxIfNecessary(e.tok, e0, domainType));
} else if (seqType is MultiSetType) {
- x = Bpl.Expr.SelectTok(expr.tok, TrExpr(e.Seq), BoxIfNecessary(expr.tok, e0, domainType));
+ x = Bpl.Expr.SelectTok(expr.tok, TrExpr(e.Seq, initEtran, funcEtran, existEtran), BoxIfNecessary(expr.tok, e0, domainType));
} else { Contract.Assert(false); x = null; }
if (!ModeledAsBoxType(elmtType) && !(seqType is MultiSetType)) {
x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);
@@ -11130,32 +11132,32 @@ namespace Microsoft.Dafny { SeqUpdateExpr e = (SeqUpdateExpr)expr;
if (e.ResolvedUpdateExpr != null)
{
- return TrExpr(e.ResolvedUpdateExpr);
+ return TrExpr(e.ResolvedUpdateExpr, initEtran, funcEtran, existEtran);
}
else
{
- Bpl.Expr seq = TrExpr(e.Seq);
+ Bpl.Expr seq = TrExpr(e.Seq, initEtran, funcEtran, existEtran);
var seqType = e.Seq.Type.NormalizeExpand();
if (seqType is SeqType)
{
Type elmtType = cce.NonNull((SeqType)seqType).Arg;
- Bpl.Expr index = TrExpr(e.Index);
- Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType);
+ Bpl.Expr index = TrExpr(e.Index, initEtran, funcEtran, existEtran);
+ Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value, initEtran, funcEtran, existEtran), elmtType);
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val);
}
else if (seqType is MapType)
{
MapType mt = (MapType)seqType;
Bpl.Type maptype = predef.MapType(expr.tok, mt.Finite, predef.BoxType, predef.BoxType);
- Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), mt.Domain);
- Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), mt.Range);
+ Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index, initEtran, funcEtran, existEtran), mt.Domain);
+ Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value, initEtran, funcEtran, existEtran), mt.Range);
return translator.FunctionCall(expr.tok, mt.Finite ? "Map#Build" : "IMap#Build", maptype, seq, index, val);
}
else if (seqType is MultiSetType)
{
Type elmtType = cce.NonNull((MultiSetType)seqType).Arg;
- Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), elmtType);
- Bpl.Expr val = TrExpr(e.Value);
+ Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index, initEtran, funcEtran, existEtran), elmtType);
+ Bpl.Expr val = TrExpr(e.Value, initEtran, funcEtran, existEtran);
return Bpl.Expr.StoreTok(expr.tok, seq, index, val);
}
else
@@ -11171,7 +11173,7 @@ namespace Microsoft.Dafny { Bpl.Type elType = translator.TrType(elmtType);
Bpl.Expr fieldName = GetArrayIndexFieldName(expr.tok, e.Indices);
- Bpl.Expr x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Array), fieldName);
+ Bpl.Expr x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Array, initEtran, funcEtran, existEtran), fieldName);
if (!ModeledAsBoxType(elmtType)) {
x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);
}
@@ -11195,30 +11197,34 @@ namespace Microsoft.Dafny { Function = fn,
Type = e.Type,
TypeArgumentSubstitutions = Util.Dict(GetTypeParams(fn), mem.TypeApplication)
- });
+ }, initEtran, funcEtran, existEtran);
}
}
- Func<Expression, Bpl.Expr> TrArg = arg => translator.BoxIfUnboxed(TrExpr(arg), arg.Type);
+ Func<Expression, Bpl.Expr> TrArg = arg => translator.BoxIfUnboxed(TrExpr(arg, initEtran, funcEtran, existEtran), arg.Type);
var applied = translator.FunctionCall(expr.tok, translator.Apply(arity), predef.BoxType,
Concat(Map(tt.TypeArgs,translator.TypeToTy),
- Cons(TrExpr(e.Function), Cons(HeapExpr, e.Args.ConvertAll(arg => TrArg(arg))))));
+ Cons(TrExpr(e.Function, initEtran, funcEtran, existEtran), Cons(HeapExpr, e.Args.ConvertAll(arg => TrArg(arg))))));
return translator.UnboxIfBoxed(applied, tt.Result);
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
Bpl.Expr layerArgument;
+ var etran = this;
+ if (e.Function.ContainsQuantifier && funcEtran != null) {
+ etran = funcEtran;
+ }
if (e.Function.IsFuelAware()) {
Statistics_CustomLayerFunctionCount++;
ModuleDefinition module = e.Function.EnclosingClass.Module;
- if (this.applyLimited_CurrentFunction != null &&
- this.layerIntraCluster != null &&
+ if (etran.applyLimited_CurrentFunction != null &&
+ etran.layerIntraCluster != null &&
ModuleDefinition.InSameSCC(e.Function, applyLimited_CurrentFunction)) {
- layerArgument = this.layerIntraCluster.GetFunctionFuel(e.Function);
+ layerArgument = etran.layerIntraCluster.GetFunctionFuel(e.Function);
} else {
- layerArgument = this.layerInterCluster.GetFunctionFuel(e.Function);
+ layerArgument = etran.layerInterCluster.GetFunctionFuel(e.Function);
}
} else {
layerArgument = null;
@@ -11253,7 +11259,7 @@ namespace Microsoft.Dafny { for (int i = 0; i < dtv.Arguments.Count; i++) {
Expression arg = dtv.Arguments[i];
Type t = dtv.Ctor.Formals[i].Type;
- var bArg = TrExpr(arg);
+ var bArg = TrExpr(arg, initEtran, funcEtran, existEtran);
argsAreLit = argsAreLit && translator.IsLit(bArg);
args.Add(translator.CondApplyBox(expr.tok, bArg, cce.NonNull(arg.Type), t));
}
@@ -11266,7 +11272,7 @@ namespace Microsoft.Dafny { return ret;
} else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
- return Old.TrExpr(e.E);
+ return Old.TrExpr(e.E, initEtran, funcEtran, existEtran);
} else if (expr is MultiSetFormingExpr) {
MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
@@ -11281,7 +11287,7 @@ namespace Microsoft.Dafny { } else if (expr is UnaryOpExpr) {
var e = (UnaryOpExpr)expr;
- Bpl.Expr arg = TrExpr(e.E);
+ Bpl.Expr arg = TrExpr(e.E, initEtran, funcEtran, existEtran);
switch (e.Op) {
case UnaryOpExpr.Opcode.Lit:
return MaybeLit(arg);
@@ -11321,8 +11327,8 @@ namespace Microsoft.Dafny { // generate: (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Unbox(Seq#Index(X,$i)) != null ==> !old($Heap)[Unbox(Seq#Index(X,$i)),alloc])
Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int));
Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar);
- Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), true, null, false);
- Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i);
+ Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E, initEtran, funcEtran, existEtran), true, null, false);
+ Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E, initEtran, funcEtran, existEtran), i);
XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI);
Bpl.Expr oNotFresh = Old.IsAlloced(expr.tok, XsubI);
Bpl.Expr oIsFresh = Bpl.Expr.Not(oNotFresh);
@@ -11334,12 +11340,12 @@ namespace Microsoft.Dafny { return new Bpl.ForallExpr(expr.tok, new List<Variable> { iVar }, body);
} else if (eeType.IsDatatype) {
// translator.FunctionCall(e.tok, BuiltinFunction.DtAlloc, null, TrExpr(e.E), Old.HeapExpr);
- Bpl.Expr alloc = translator.MkIsAlloc(TrExpr(e.E), eeType, Old.HeapExpr);
+ Bpl.Expr alloc = translator.MkIsAlloc(TrExpr(e.E, initEtran, funcEtran, existEtran), eeType, Old.HeapExpr);
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, alloc);
} else {
// generate: x != null && !old($Heap)[x]
- Bpl.Expr oNull = Bpl.Expr.Neq(TrExpr(e.E), predef.Null);
- Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E)));
+ Bpl.Expr oNull = Bpl.Expr.Neq(TrExpr(e.E, initEtran, funcEtran, existEtran), predef.Null);
+ Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E, initEtran, funcEtran, existEtran)));
return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And, oNull, oIsFresh);
}
default:
@@ -11359,14 +11365,14 @@ namespace Microsoft.Dafny { ct = BuiltinFunction.RealToInt;
} else {
Contract.Assert(fromInt == toInt);
- return TrExpr(e.E);
+ return TrExpr(e.E, initEtran, funcEtran, existEtran);
}
- return translator.FunctionCall(e.tok, ct, null, TrExpr(e.E));
+ return translator.FunctionCall(e.tok, ct, null, TrExpr(e.E, initEtran, funcEtran, existEtran));
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
bool isReal = e.E0.Type.IsNumericBased(Type.NumericPersuation.Real);
- Bpl.Expr e0 = TrExpr(e.E0);
+ Bpl.Expr e0 = TrExpr(e.E0, initEtran, funcEtran, existEtran);
if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet) {
return TrInSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInSet translate e.E1
} else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSet) {
@@ -11378,7 +11384,7 @@ namespace Microsoft.Dafny { Bpl.Expr arg = TrInMultiSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInMultiSet translate e.E1
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, arg);
}
- Bpl.Expr e1 = TrExpr(e.E1);
+ Bpl.Expr e1 = TrExpr(e.E1, initEtran, funcEtran, existEtran);
BinaryOperator.Opcode bOpcode;
Bpl.Type typ;
var oe0 = e0;
@@ -11695,9 +11701,9 @@ namespace Microsoft.Dafny { return re;
} else if (expr is TernaryExpr) {
var e = (TernaryExpr)expr;
- var e0 = TrExpr(e.E0);
- var e1 = TrExpr(e.E1);
- var e2 = TrExpr(e.E2);
+ var e0 = TrExpr(e.E0, initEtran, funcEtran, existEtran);
+ var e1 = TrExpr(e.E1, initEtran, funcEtran, existEtran);
+ var e2 = TrExpr(e.E2, initEtran, funcEtran, existEtran);
switch (e.Op) {
case TernaryExpr.Opcode.PrefixEqOp:
case TernaryExpr.Opcode.PrefixNeqOp:
@@ -11717,24 +11723,25 @@ namespace Microsoft.Dafny { } else if (expr is LetExpr) {
var e = (LetExpr)expr;
if (e.Exact) {
- return TrExpr(GetSubstitutedBody(e));
+ return TrExpr(GetSubstitutedBody(e), initEtran, funcEtran, existEtran);
} else {
var d = translator.LetDesugaring(e);
- return TrExpr(d);
+ return TrExpr(d, initEtran, funcEtran, existEtran);
}
} else if (expr is NamedExpr) {
- return TrExpr(((NamedExpr)expr).Body);
+ return TrExpr(((NamedExpr)expr).Body, initEtran, funcEtran, existEtran);
} else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
if (e.SplitQuantifier != null) {
- return TrExpr(e.SplitQuantifierExpression);
+ return TrExpr(e.SplitQuantifierExpression, initEtran, existEtran, existEtran);
} else {
List<Variable> tyvars = translator.MkTyParamBinders(e.TypeArgs);
List<Variable> bvars = new List<Variable>();
- var initEtran = (etran == null) ? this : etran;
+ var etran = initEtran ?? this;
var bodyEtran = this;
+ existEtran = e is ForallExpr ? this : existEtran;
bool _scratch = true;
Bpl.Expr antecedent = Bpl.Expr.True;
@@ -11750,11 +11757,11 @@ namespace Microsoft.Dafny { antecedent = BplAnd(new List<Bpl.Expr> {
antecedent,
translator.FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, h),
- translator.HeapSameOrSucc(initEtran.HeapExpr, h)
+ translator.HeapSameOrSucc(etran.HeapExpr, h)
});
}
- antecedent = BplAnd(antecedent, initEtran.TrBoundVariables(e.BoundVars, bvars));
+ antecedent = BplAnd(antecedent, etran.TrBoundVariables(e.BoundVars, bvars));
Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");
Bpl.Trigger tr = null;
@@ -11763,15 +11770,15 @@ namespace Microsoft.Dafny { if (aa.Name == "trigger") {
List<Bpl.Expr> tt = new List<Bpl.Expr>();
foreach (var arg in aa.Args) {
- tt.Add(argsEtran.TrExpr(arg));
+ tt.Add(argsEtran.TrExpr(arg, initEtran, existEtran, existEtran));
}
tr = new Bpl.Trigger(expr.tok, true, tt, tr);
}
}
if (e.Range != null) {
- antecedent = BplAnd(antecedent, initEtran.TrExpr(e.Range));
+ antecedent = BplAnd(antecedent, etran.TrExpr(e.Range, initEtran, existEtran, existEtran));
}
- Bpl.Expr body = bodyEtran.TrExpr(e.Term);
+ Bpl.Expr body = bodyEtran.TrExpr(e.Term, initEtran, existEtran, existEtran);
if (e is ForallExpr) {
return new Bpl.ForallExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body));
@@ -11790,8 +11797,8 @@ namespace Microsoft.Dafny { var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, translator.CurrentIdGenerator.FreshId("$y#"), predef.BoxType));
Bpl.Expr y = new Bpl.IdentifierExpr(expr.tok, yVar);
- var eq = Bpl.Expr.Eq(y, BoxIfNecessary(expr.tok, TrExpr(e.Term), e.Term.Type));
- var ebody = Bpl.Expr.And(BplAnd(typeAntecedent, TrExpr(e.Range)), eq);
+ var eq = Bpl.Expr.Eq(y, BoxIfNecessary(expr.tok, TrExpr(e.Term, initEtran, funcEtran, existEtran), e.Term.Type));
+ var ebody = Bpl.Expr.And(BplAnd(typeAntecedent, TrExpr(e.Range, initEtran, funcEtran, existEtran)), eq);
var triggers = translator.TrTrigger(this, e.Attributes, e.tok);
var exst = new Bpl.ExistsExpr(expr.tok, bvars, triggers, ebody);
@@ -11818,9 +11825,9 @@ namespace Microsoft.Dafny { Dictionary<IVariable, Expression> subst = new Dictionary<IVariable,Expression>();
subst.Add(e.BoundVars[0], new BoogieWrapper(unboxy,e.BoundVars[0].Type));
- var ebody = BplAnd(typeAntecedent ?? Bpl.Expr.True, TrExpr(translator.Substitute(e.Range, null, subst)));
+ var ebody = BplAnd(typeAntecedent ?? Bpl.Expr.True, TrExpr(translator.Substitute(e.Range, null, subst), initEtran, funcEtran, existEtran));
Bpl.Expr l1 = new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), new List<Variable> { yVar }, kv, ebody);
- ebody = TrExpr(translator.Substitute(e.Term, null, subst));
+ ebody = TrExpr(translator.Substitute(e.Term, null, subst), initEtran, funcEtran, existEtran);
Bpl.Expr l2 = new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), new List<Variable> { yVar }, kv, BoxIfNecessary(expr.tok, ebody, e.Term.Type));
bool finite = e.Finite;
@@ -11833,31 +11840,31 @@ namespace Microsoft.Dafny { } else if (expr is StmtExpr) {
var e = (StmtExpr)expr;
- return TrExpr(e.E);
+ return TrExpr(e.E, initEtran, funcEtran, existEtran);
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
- var g = translator.RemoveLit(TrExpr(e.Test));
- var thn = translator.RemoveLit(TrExpr(e.Thn));
- var els = translator.RemoveLit(TrExpr(e.Els));
+ var g = translator.RemoveLit(TrExpr(e.Test, initEtran, funcEtran, existEtran));
+ var thn = translator.RemoveLit(TrExpr(e.Thn, initEtran, funcEtran, existEtran));
+ var els = translator.RemoveLit(TrExpr(e.Els, initEtran, funcEtran, existEtran));
return new NAryExpr(expr.tok, new IfThenElse(expr.tok), new List<Bpl.Expr> { g, thn, els });
} else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
var ite = DesugarMatchExpr(e);
- return TrExpr(ite);
+ return TrExpr(ite, initEtran, funcEtran, existEtran);
} else if (expr is ConcreteSyntaxExpression) {
var e = (ConcreteSyntaxExpression)expr;
- return TrExpr(e.ResolvedExpression);
+ return TrExpr(e.ResolvedExpression, initEtran, funcEtran, existEtran);
} else if (expr is BoxingCastExpr) {
BoxingCastExpr e = (BoxingCastExpr)expr;
- return translator.CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType);
+ return translator.CondApplyBox(e.tok, TrExpr(e.E, initEtran, funcEtran, existEtran), e.FromType, e.ToType);
} else if (expr is UnboxingCastExpr) {
UnboxingCastExpr e = (UnboxingCastExpr)expr;
- return translator.CondApplyUnbox(e.tok, TrExpr(e.E), e.FromType, e.ToType);
+ return translator.CondApplyUnbox(e.tok, TrExpr(e.E, initEtran, funcEtran, existEtran), e.FromType, e.ToType);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
@@ -13314,8 +13321,10 @@ namespace Microsoft.Dafny { translatedExpression = etran.TrExpr(expr);
splitHappened = false;
} else {
+ // for quantifierExpr, we don't want to increase fuel in assert context
+ var existEtran = etran;
etran = etran.LayerOffset(1);
- translatedExpression = etran.TrExpr(expr);
+ translatedExpression = etran.TrExpr(expr, null, etran, existEtran);
splitHappened = etran.Statistics_CustomLayerFunctionCount != 0; // return true if the LayerOffset(1) came into play
}
if (TrSplitNeedsTokenAdjustment(expr)) {
|