From bcd8949ab6d5bd86dc3e81226b1f936d05babfa4 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Tue, 8 Jun 2010 20:09:12 +0000
Subject: Dafny:  Fix type bug in SplitExpr translation.

---
 Dafny/DafnyAst.ssc        | 13 +++++++++++++
 Dafny/Translator.ssc      | 10 +++++++++-
 Test/dafny1/Celebrity.dfy |  3 +--
 3 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/Dafny/DafnyAst.ssc b/Dafny/DafnyAst.ssc
index ef047c4d..1ea2e150 100644
--- a/Dafny/DafnyAst.ssc
+++ b/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/Dafny/Translator.ssc b/Dafny/Translator.ssc
index 35e8cdc1..caa8fb2b 100644
--- a/Dafny/Translator.ssc
+++ b/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;
-- 
cgit v1.2.3