diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala index f6daf84c4e68abedc32cab2b9af8d9ddd8f1fe8b..a130ee946d0a4b033cb5526b1ce964ebfd54ce8e 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 3370b6ae6f82e7e131277be078eaf824dca72c50..473319e886d8a16ae05889a80589ce2ec17d7782 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)