From cfc07840a39350bfa2a7db999db41f8db859da93 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 22 Mar 2012 23:14:08 +0000
Subject: [PATCH] nested def are correctly extracted
---
src/main/scala/leon/plugin/CodeExtraction.scala | 7 ++-----
src/main/scala/leon/plugin/Extractors.scala | 6 +++---
src/main/scala/leon/purescala/PrettyPrinter.scala | 2 ++
3 files changed, 7 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index eb5191189..f723b2d7f 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -394,13 +394,10 @@ trait CodeExtraction extends Extractors {
varSubsts.remove(vs)
Let(newID, valTree, restTree)
}
- case dd @ ExLocalFunctionDef(n, p, t, b, rest) => {
+ case dd @ ExLocalFunctionDef(sy,n, p, t, b, rest) => {
val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
val funDefWithBody = extractFunDef(funDef, b)
- println("got let def: " + funDefWithBody)
- println(funDef)
- defsToDefs += (dd.symbol -> funDefWithBody)
- println(defsToDefs)
+ defsToDefs += (sy -> funDefWithBody)
val letRest = rec(rest)
defsToDefs.remove(dd.symbol)
val res = LetDef(funDefWithBody, letRest)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 8b55cf10d..26096444c 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -152,12 +152,12 @@ trait Extractors {
}
object ExLocalFunctionDef {
- def unapply(tree: Block): Option[(String,Seq[ValDef],Tree,Tree,Tree)] = tree match {
+ def unapply(tree: Block): Option[(Symbol,String,Seq[ValDef],Tree,Tree,Tree)] = tree match {
case Block((dd @ DefDef(_, name, tparams, vparamss, tpt, rhs)) :: rest, expr) if(tparams.isEmpty && vparamss.size == 1 && name != nme.CONSTRUCTOR) => {
if(rest.isEmpty)
- Some((name.toString, vparamss(0), tpt, rhs, expr))
+ Some((dd.symbol,name.toString, vparamss(0), tpt, rhs, expr))
else
- Some((name.toString, vparamss(0), tpt, rhs, Block(rest, expr)))
+ Some((dd.symbol,name.toString, vparamss(0), tpt, rhs, Block(rest, expr)))
}
case _ => None
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 98cbee885..b16515c4a 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -74,6 +74,8 @@ object PrettyPrinter {
case LetDef(fd,e) => {
sb.append("{")
pp(fd, sb, lvl)
+ sb.append("\n")
+ ind(sb, lvl)
pp(e, sb, lvl)
sb.append("}")
sb
--
GitLab