From 70b011d7e678cac55d4a70825ca1d2eb9523782e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Tue, 18 Feb 2014 15:58:36 +0100
Subject: [PATCH] Fix handling of fields of case-classes v.s. method calls

---
 .../leon/frontends/scalac/ASTExtractors.scala |  8 -------
 .../frontends/scalac/CodeExtraction.scala     | 22 +++++--------------
 2 files changed, 6 insertions(+), 24 deletions(-)

diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index f6daf84c4..a130ee946 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -575,14 +575,6 @@ trait ASTExtractors {
       }
     }
 
-    // used for case classes selectors.
-    object ExParameterlessMethodCall {
-      def unapply(tree: Select): Option[(Tree,Name)] = tree match {
-        case Select(lhs, n) => Some((lhs, n))
-        case _ => None
-      }
-    }
-
     object ExPatternMatching {
       def unapply(tree: Match): Option[(Tree,List[CaseDef])] =
         if(tree != null) Some((tree.selector, tree.cases)) else None
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 3370b6ae6..473319e88 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -667,22 +667,6 @@ trait CodeExtraction extends ASTExtractors {
               outOfSubsetError(current, "Unknown case object "+sym.name)
           }
 
-
-        case ExParameterlessMethodCall(t,n) if extractTree(t).getType.isInstanceOf[CaseClassType] =>
-          val selector = extractTree(t)
-          val selType = selector.getType.asInstanceOf[CaseClassType]
-
-
-          val fieldID = selType.fields.find(_.id.name == n.toString) match {
-            case None =>
-              outOfSubsetError(current, "Invalid method or field invocation (not a case class arg?)")
-
-            case Some(vd) =>
-              vd.id
-          }
-
-          CaseClassSelector(selType, selector, fieldID)
-
         case ExTuple(tpes, exprs) =>
           val tupleExprs = exprs.map(e => extractTree(e))
           val tupleType = TupleType(tupleExprs.map(expr => expr.getType))
@@ -1112,6 +1096,12 @@ trait CodeExtraction extends ASTExtractors {
 
               MethodInvocation(rec, cd, fd.typed(newTps), args)
 
+            case (IsTyped(rec, cct: CaseClassType), name, Nil) if cct.fields.exists(_.id.name == name) =>
+
+              val fieldID = cct.fields.find(_.id.name == name).get.id
+
+              CaseClassSelector(cct, rec, fieldID)
+
             case (IsTyped(_, SetType(base)), "min", Nil) =>
               SetMin(rrec).setType(base)
 
-- 
GitLab