From 3e4281d8ff440e99f6bafa48c07850977aebfa57 Mon Sep 17 00:00:00 2001
From: Lars Hupel <lars.hupel@mytum.de>
Date: Thu, 6 Aug 2015 17:34:07 +0200
Subject: [PATCH] preserve annotation arguments in the AST
---
.../scala/leon/frontends/scalac/ASTExtractors.scala | 12 ++++++++----
.../scala/leon/frontends/scalac/CodeExtraction.scala | 6 +++---
src/main/scala/leon/purescala/Definitions.scala | 9 +++++----
3 files changed, 16 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index ec3c9738a..2d6ec3191 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -20,7 +20,7 @@ trait ASTExtractors {
rootMirror.getClassByName(newTermName(str))
}
- def annotationsOf(s: Symbol): Set[String] = {
+ def annotationsOf(s: Symbol): Map[String, Seq[Option[Any]]] = {
val actualSymbol = s.accessedOrSelf
(for {
@@ -28,8 +28,12 @@ trait ASTExtractors {
name = a.atp.safeToString.replaceAll("\\.package\\.", ".")
if (name startsWith "leon.annotation.")
} yield {
- name.split("\\.", 3)(2)
- }).toSet
+ val args = a.args.map {
+ case Literal(x) => Some(x.value)
+ case _ => None
+ }
+ (name.split("\\.", 3)(2), args)
+ }).toMap
}
protected lazy val tuple2Sym = classFromName("scala.Tuple2")
@@ -406,7 +410,7 @@ trait ASTExtractors {
case DefDef(_, name, tparams, vparamss, tpt, rhs) if name != nme.CONSTRUCTOR && !dd.symbol.isAccessor =>
if (dd.symbol.isSynthetic && dd.symbol.isImplicit && dd.symbol.isMethod) {
// Check that the class it was generated from is not ignored
- if (annotationsOf(tpt.symbol)("ignore")) {
+ if (annotationsOf(tpt.symbol).isDefinedAt("ignore")) {
None
} else {
Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index a95b760ca..cda2d5fae 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -632,7 +632,7 @@ trait CodeExtraction extends ASTExtractors {
fd.setPos(sym.pos)
- fd.addFlags(annotationsOf(sym).map(FunctionFlag.fromName))
+ fd.addFlags(annotationsOf(sym).map { case (name, args) => FunctionFlag.fromName(name, args) }.toSet)
if (sym.isImplicit) {
fd.addFlag(IsInlined)
@@ -667,7 +667,7 @@ trait CodeExtraction extends ASTExtractors {
fd.setPos(sym.pos)
fd.addFlag(IsField(isLazy))
- fd.addFlags(annotationsOf(sym).map(FunctionFlag.fromName))
+ fd.addFlags(annotationsOf(sym).map { case (name, args) => FunctionFlag.fromName(name, args) }.toSet)
defsToDefs += sym -> fd
@@ -1082,7 +1082,7 @@ trait CodeExtraction extends ASTExtractors {
val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap
- fd.addFlags(annotationsOf(d.symbol).map(FunctionFlag.fromName))
+ fd.addFlags(annotationsOf(d.symbol).map { case (name, args) => FunctionFlag.fromName(name, args) }.toSet)
val newDctx = dctx.copy(tparams = dctx.tparams ++ tparamsMap)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index b5cffb4d7..fde6f3de7 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -305,16 +305,16 @@ object Definitions {
sealed abstract class FunctionFlag
object FunctionFlag {
- def fromName(name: String): FunctionFlag = name match {
+ def fromName(name: String, args: Seq[Option[Any]]): FunctionFlag = name match {
case "inline" => IsInlined
- case _ => Annotation(name)
+ case _ => Annotation(name, args)
}
}
// Whether this FunDef was originally a (lazy) field
case class IsField(isLazy: Boolean) extends FunctionFlag
// Compiler annotations given in the source code as @annot
- case class Annotation(annot: String) extends FunctionFlag
+ case class Annotation(annot: String, args: Seq[Option[Any]]) extends FunctionFlag
// If this class was a method. owner is the original owner of the method
case class IsMethod(owner: ClassDef) extends FunctionFlag
// If this function represents a loop that was there before XLangElimination
@@ -401,7 +401,8 @@ object Definitions {
def flags = flags_
- def annotations: Set[String] = flags_ collect { case Annotation(s) => s }
+ def annotations: Set[String] = extAnnotations.keySet
+ def extAnnotations: Map[String, Seq[Option[Any]]] = flags_.collect { case Annotation(s, args) => s -> args }.toMap
def canBeLazyField = flags.contains(IsField(true)) && params.isEmpty && tparams.isEmpty
def canBeStrictField = flags.contains(IsField(false)) && params.isEmpty && tparams.isEmpty
def canBeField = canBeLazyField || canBeStrictField
--
GitLab