From 449725fec05add4190662ebe2be24ac3cb6d886e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 15 Apr 2015 20:45:05 +0200
Subject: [PATCH] Do not ignore all implicits, only implicit synthetic
functions.
> @ignore
> implicit class Foo(x: ..)
generates an implicit synthetic conversion without @ignore. We
explicitly ignore these as they are extracted specially. However, we
should *not* ignore implicit defs that the user defined for convenience.
Sadly, Scala does not support "implicit case class", so in Leon
you have to use a normal case class with a normal implicit conversion
that wraps in the case-class:
> case class Foo(x: Bar)
> implicit def barToFoo(b: Bar): Foo = Foo(b)
---
src/main/scala/leon/frontends/scalac/CodeExtraction.scala | 7 +++----
1 file changed, 3 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9a80528f3..cd3638a66 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -184,7 +184,7 @@ trait CodeExtraction extends ASTExtractors {
}
def isIgnored(s: Symbol) = {
- (annotationsOf(s) contains "ignore") || s.isImplicit || s.fullName.toString.endsWith(".main")
+ (annotationsOf(s) contains "ignore") || s.fullName.toString.endsWith(".main")
}
def isExtern(s: Symbol) = {
@@ -867,7 +867,7 @@ trait CodeExtraction extends ASTExtractors {
case ExFieldDef(_,_,_) =>
case ExLazyFieldDef() =>
case ExFieldAccessorFunction() =>
- case d if isIgnored(d.symbol) =>
+ case d if isIgnored(d.symbol) || (d.symbol.isImplicit && d.symbol.isSynthetic) =>
case tree =>
outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
}
@@ -1759,8 +1759,7 @@ trait CodeExtraction extends ASTExtractors {
// default behaviour is to complain :)
case _ =>
- println(tr.getClass)
- outOfSubsetError(tr, "Could not extract as PureScala")
+ outOfSubsetError(tr, "Could not extract as PureScala (Scala tree of type "+tr.getClass+")")
}
res.setPos(current.pos)
--
GitLab