From 27fc635d08a175f1d878249a1d5ec4f2e735421c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 5 Mar 2014 12:29:48 +0100
Subject: [PATCH] Correctly extract methods from single case-classes

---
 .../frontends/scalac/CodeExtraction.scala     | 44 +++++++++++--------
 1 file changed, 25 insertions(+), 19 deletions(-)

diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 7dad7128b..e7c9b6c90 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -415,32 +415,38 @@ trait CodeExtraction extends ASTExtractors {
 
     private def extractMethodDefs(defs: List[Tree]) = {
       // We collect defined function bodies
-      for (d <- defs) d match {
-        case ExAbstractClass(_, csym, tmpl) =>
-          val cd = classesToClasses(csym)
+      def extractFromClass(csym: Symbol, tmpl: Template) {
+        val cd = classesToClasses(csym)
 
-          val ctparams = csym.tpe match {
-            case TypeRef(_, _, tps) =>
-              extractTypeParams(tps).map(_._1)
-            case _ =>
-              Nil
-          }
+        val ctparams = csym.tpe match {
+          case TypeRef(_, _, tps) =>
+            extractTypeParams(tps).map(_._1)
+          case _ =>
+            Nil
+        }
 
-          val ctparamsMap = ctparams zip cd.tparams.map(_.tp)
+        val ctparamsMap = ctparams zip cd.tparams.map(_.tp)
 
-          for (d <- tmpl.body) d match {
-            case ExFunctionDef(sym, tparams, params, _, body) =>
-              val fd = defsToDefs(sym)
+        for (d <- tmpl.body) d match {
+          case ExFunctionDef(sym, tparams, params, _, body) if !sym.isSynthetic && !sym.isAccessor =>
+            val fd = defsToDefs(sym)
 
-              val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap ++ ctparamsMap
+            val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap ++ ctparamsMap
 
-              if(body != EmptyTree) {
-                extractFunBody(fd, params, body)(DefContext(tparamsMap))
-              }
+            if(body != EmptyTree) {
+              extractFunBody(fd, params, body)(DefContext(tparamsMap))
+            }
 
-            case _ =>
+          case _ =>
 
-          }
+        }
+      }
+      for (d <- defs) d match {
+        case ExAbstractClass(_, csym, tmpl) =>
+          extractFromClass(csym, tmpl)
+
+        case ExCaseClass(_, csym, _, tmpl) =>
+          extractFromClass(csym, tmpl)
 
         case _ =>
       }
-- 
GitLab