From bf148faec00b2acd657ac79f63a46cf908ef9aca Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 26 Aug 2015 15:30:17 +0200
Subject: [PATCH] Ok, now we extract correctly
---
.../leon/frontends/scalac/ASTExtractors.scala | 7 ++++---
.../frontends/scalac/CodeExtraction.scala | 21 ++++++++++++-------
2 files changed, 18 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index bfc097c37..d8910012f 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -445,12 +445,13 @@ trait ASTExtractors {
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
+ case df@DefDef(_, name, _, _, tpt, _) if (
+ sym.isStable && sym.isAccessor && sym.name != nme.CONSTRUCTOR &&
+ sym.accessed == NoSymbol // This is to exclude fields with implementation
) =>
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 87418d2dd..62627f8c8 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -290,11 +290,16 @@ trait CodeExtraction extends ASTExtractors {
case ExFieldDef(sym, _, _) =>
Some(defineFieldFunDef(sym, false)(DefContext()))
- case ExCaseClassSyntheticJunk() => None
- case ExConstructorDef() => None
- case ExLazyFieldDef() => None
- case ExFieldAccessorFunction() => None
- case d if (d.symbol.isImplicit && d.symbol.isSynthetic) => None
+ // All these are expected, but useless
+ case ExCaseClassSyntheticJunk()
+ | ExConstructorDef()
+ | ExLazyFieldDef()
+ | ExFieldAccessorFunction() =>
+ None
+ case d if (d.symbol.isImplicit && d.symbol.isSynthetic) =>
+ None
+
+ // Everything else is unexpected
case tree =>
println(tree)
outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
@@ -302,9 +307,11 @@ trait CodeExtraction extends ASTExtractors {
Some(LeonModuleDef(id, leonDefs, id.name == "package"))
- case ExCaseClassSyntheticJunk() => None
- case ExConstructorDef() => None
+ // Expected, but useless
+ case ExCaseClassSyntheticJunk() | ExConstructorDef() => None
case d if (d.symbol.isImplicit && d.symbol.isSynthetic) => None
+
+ // Unexpected
case tree =>
println(tree)
outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
--
GitLab