Dafny: Fix type bug in SplitExpr translation.

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;