From 3dd012e088d420309e9b4a449a70d0fb515c4426 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 8 Sep 2015 14:54:39 +0200
Subject: [PATCH] Revert "Fix treatment of 'this' in MethodLifting"

This reverts commit c4bf3e8899a33b452ae4a7dae2c7916de487fa77.
---
 .../scala/leon/purescala/MethodLifting.scala  | 19 +++++++------------
 1 file changed, 7 insertions(+), 12 deletions(-)

diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index 6dded733c..277803109 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(ct) =>
-            asInstOf(Variable(binder), ct)
+          case This(`at`) =>
+            Variable(binder)
           case e =>
             e
         }
@@ -158,19 +158,14 @@ object MethodLifting extends TransformationPhase {
         nfd.addFlag(IsMethod(cd))
 
         if (cd.knownDescendants.forall( cd => (cd.methods ++ cd.fields).forall(_.id != fd.id))) {
-          // Don't need to compose methods
           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))
+          // Don't need to compose methods
+          nfd.fullBody = postMap {
+            case th@This(ct) if ct.classDef == cd =>
+              Some(receiver.toVariable.setPos(th))
             case _ =>
               None
-          }
-          nfd.fullBody = instantiateType(
-            postMap(thisToReceiver)(nfd.fullBody),
-            tparamsMap,
-            paramsMap
-          )
+          }(instantiateType(nfd.fullBody, tparamsMap, paramsMap))
         } else {
           // We need to compose methods of subclasses
 
-- 
GitLab