From 54bc9b3aa7b734ee4f689a8e4667c51ae0ff566f Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 26 Aug 2015 14:31:04 +0200
Subject: [PATCH] Correctly parse abstract val's
---
.../leon/frontends/scalac/ASTExtractors.scala | 8 +++++++-
.../leon/frontends/scalac/CodeExtraction.scala | 18 +++++++++++-------
2 files changed, 18 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 3c4818737..bfc097c37 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -438,15 +438,21 @@ trait ASTExtractors {
object ExFieldDef {
/** Matches a definition of a strict field inside a class constructor */
- def unapply(vd : ValDef) : Option[(Symbol, Type, Tree)] = {
+ def unapply(vd: SymTree) : Option[(Symbol, Type, Tree)] = {
val sym = vd.symbol
vd match {
+ // Implemented fields
case ValDef(mods, name, tpt, rhs) if (
!sym.isCaseAccessor && !sym.isParamAccessor &&
!sym.isLazy && !sym.isSynthetic && !sym.isAccessor
) =>
// Since scalac uses the accessor symbol all over the place, we pass that instead:
Some( (sym.getterIn(sym.owner),tpt.tpe,rhs) )
+ // Unimplemented fields
+ case DefDef(_, name, _, _, tpt, _) if (
+ sym.isStable && sym.isAccessor && sym.name != nme.CONSTRUCTOR
+ ) =>
+ Some( (sym, tpt.tpe, EmptyTree))
case _ => None
}
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 4fbecc9cd..87418d2dd 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -450,10 +450,10 @@ trait CodeExtraction extends ASTExtractors {
* and registers $fd as the default value function for this parameter.
*/
private def registerDefaultMethod(
- defs : List[Tree],
- matcher : PartialFunction[Tree,Symbol],
- index : Int,
- fd : FunDef
+ defs : List[Tree],
+ matcher : PartialFunction[Tree,Symbol],
+ index : Int,
+ fd : FunDef
) {
// Search tmpl to find the function that includes this parameter
val paramOwner = defs.collectFirst(matcher).get
@@ -467,6 +467,9 @@ trait CodeExtraction extends ASTExtractors {
}
def extractClassDef(sym: Symbol, args: Seq[(Symbol, ValDef)], tmpl: Template): LeonClassDef = {
+
+ //println(s"Extracting $sym")
+
val id = FreshIdentifier(sym.name.toString).setPos(sym.pos)
val tparamsMap = sym.tpe match {
@@ -536,7 +539,7 @@ trait CodeExtraction extends ASTExtractors {
ccd
}
-
+ //println(s"Body of $sym")
// We collect the methods and fields
for (d <- tmpl.body) d match {
@@ -580,6 +583,7 @@ trait CodeExtraction extends ASTExtractors {
// normal fields
case t @ ExFieldDef(fsym, _, _) =>
+ //println(fsym + "matched as ExFieldDef")
// we will be using the accessor method of this field everywhere
val fsymAsMethod = fsym
val fd = defineFieldFunDef(fsymAsMethod, false, Some(cd))(defCtx)
@@ -589,7 +593,8 @@ trait CodeExtraction extends ASTExtractors {
cd.registerMethod(fd)
- case _ =>
+ case other =>
+
}
cd
@@ -1483,7 +1488,6 @@ trait CodeExtraction extends ASTExtractors {
//println(s"symbol $sym with id ${sym.id}")
//println(s"isMethod($sym) == ${isMethod(sym)}")
-
(rrec, sym.name.decoded, rargs) match {
case (null, _, args) =>
val fd = getFunDef(sym, c.pos)
--
GitLab