From c4bf3e8899a33b452ae4a7dae2c7916de487fa77 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 4 Sep 2015 12:07:02 +0200
Subject: [PATCH] Fix treatment of 'this' in MethodLifting
'this' can be of a subtype while MethodLifting.
MethodLifting sometimes needs to insert type casts.
---
.../scala/leon/purescala/MethodLifting.scala | 19 ++++++++++++-------
1 file changed, 12 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index 277803109..6dded733c 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -79,8 +79,8 @@ object MethodLifting extends TransformationPhase {
val at = acd.typed
val binder = FreshIdentifier(acd.id.name.toLowerCase, at, true)
def subst(e: Expr): Expr = e match {
- case This(`at`) =>
- Variable(binder)
+ case This(ct) =>
+ asInstOf(Variable(binder), ct)
case e =>
e
}
@@ -158,14 +158,19 @@ object MethodLifting extends TransformationPhase {
nfd.addFlag(IsMethod(cd))
if (cd.knownDescendants.forall( cd => (cd.methods ++ cd.fields).forall(_.id != fd.id))) {
- val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
// Don't need to compose methods
- nfd.fullBody = postMap {
- case th@This(ct) if ct.classDef == cd =>
- Some(receiver.toVariable.setPos(th))
+ val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
+ def thisToReceiver(e: Expr): Option[Expr] = e match {
+ case th@This(ct) => //if ct.classDef == cd =>
+ Some(asInstOf(receiver.toVariable, ct).setPos(th))
case _ =>
None
- }(instantiateType(nfd.fullBody, tparamsMap, paramsMap))
+ }
+ nfd.fullBody = instantiateType(
+ postMap(thisToReceiver)(nfd.fullBody),
+ tparamsMap,
+ paramsMap
+ )
} else {
// We need to compose methods of subclasses
--
GitLab