From 1298b62b4374db38fdb219a8a44eff4b5ba69d79 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 22 May 2015 17:45:41 +0200
Subject: [PATCH] Fix issue with extraction of case objects on top-level

---
 src/main/scala/leon/frontends/scalac/ASTExtractors.scala | 9 +++++++--
 .../scala/leon/frontends/scalac/CodeExtraction.scala     | 5 ++++-
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 3d8df24e1..d469f0ce1 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -270,10 +270,15 @@ trait ASTExtractors {
 
     object ExObjectDef {
       /** Matches an object with no type parameters, and regardless of its
-       * visibility. Does not match on the automatically generated companion
+       * visibility. Does not match on case objects or the automatically generated companion
        * objects of case classes (or any synthetic class). */
       def unapply(cd: ClassDef): Option[(String,Template)] = cd match {
-        case ClassDef(_, name, tparams, impl) if (cd.symbol.isModuleClass || cd.symbol.hasPackageFlag) && tparams.isEmpty && !cd.symbol.isSynthetic => {
+        case ClassDef(_, name, tparams, impl) if
+          (cd.symbol.isModuleClass || cd.symbol.hasPackageFlag) &&
+          tparams.isEmpty &&
+          !cd.symbol.isSynthetic &&
+          !cd.symbol.isCaseClass
+        => {
           Some((name.toString, impl))
         }
         case _ => None
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9e209b5d5..44125a370 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -858,7 +858,10 @@ trait CodeExtraction extends ASTExtractors {
         case ExFieldDef(_,_,_) =>
         case ExLazyFieldDef() => 
         case ExFieldAccessorFunction() => 
-        case d if isIgnored(d.symbol) || (d.symbol.isImplicit && d.symbol.isSynthetic) =>
+        case d if // Various synthetic junk
+          isIgnored(d.symbol) ||
+          (d.symbol.isImplicit && d.symbol.isSynthetic ) ||
+          (d.symbol.isMethod && d.symbol.isSynthetic) =>
         case tree =>
           println(tree)
           outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
-- 
GitLab