diff options
-rw-r--r-- | Source/Dafny/DafnyAst.ssc | 13 | ||||
-rw-r--r-- | Source/Dafny/Translator.ssc | 10 | ||||
-rw-r--r-- | Test/dafny1/Celebrity.dfy | 3 |
3 files changed, 23 insertions, 3 deletions
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index ef047c4d..1ea2e150 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -1333,6 +1333,19 @@ namespace Microsoft.Dafny }
}
+ public class BoxingCastExpr : Expression { // a BoxingCastExpr is used only as a temporary placeholding during translation
+ public readonly Expression! E;
+ public readonly Type! FromType;
+ public readonly Type! ToType;
+
+ public BoxingCastExpr(Expression! e, Type! fromType, Type! toType) {
+ base(e.tok);
+ E = e;
+ FromType = fromType;
+ ToType = toType;
+ }
+ }
+
public class MaybeFreeExpression {
public readonly Expression! E;
public readonly bool IsFree;
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index 35e8cdc1..caa8fb2b 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -3071,6 +3071,10 @@ namespace Microsoft.Dafny { Bpl.Expr els = TrExpr(e.Els);
return translator.FunctionCall(expr.tok, BuiltinFunction.IfThenElse, translator.TrType((!)expr.Type), g, thn, els);
+ } else if (expr is BoxingCastExpr) {
+ BoxingCastExpr e = (BoxingCastExpr)expr;
+ return CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType);
+
} else {
assert false; // unexpected expression
}
@@ -3607,7 +3611,11 @@ namespace Microsoft.Dafny { Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
assert fexp.Args.Count == fexp.Function.Formals.Count;
for (int i = 0; i < fexp.Function.Formals.Count; i++) {
- substMap.Add(fexp.Function.Formals[i], fexp.Args[i]);
+ Formal p = fexp.Function.Formals[i];
+ Expression arg = fexp.Args[i];
+ arg = new BoxingCastExpr(arg, (!)arg.Type, p.Type);
+ arg.Type = p.Type; // resolve here
+ substMap.Add(p, arg);
}
Expression body = Substitute(fexp.Function.Body, fexp.Receiver, substMap);
foreach (Expression se in SplitExpr(body, false)) {
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index fd267c71..eed06bb1 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -72,8 +72,7 @@ method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)
requires 0 < n;
requires (forall p :: p in people <==> 0 <= p && p < n);
- // requires IsCelebrity(c, people); // see next line:
- requires c in people && (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p)); // hack to work around bug in Dafny-to-Boogie translator
+ requires IsCelebrity(c, people);
ensures r == c;
{
r := 0;
|