From 476a18f482380971dce8620b9a09b2d1c318ac37 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Mon, 18 Jan 2016 17:55:27 +0100
Subject: [PATCH] Corrected ScopeSimplifier.scala (wrong nested definition of
argument identifiers) Corrected bug when using string and escape Added a
comment about application simplification.
---
.../scala/leon/purescala/Constructors.scala | 7 +++++++
.../leon/purescala/ScopeSimplifier.scala | 20 ++++++++++++-------
.../leon/synthesis/rules/StringRender.scala | 3 +--
3 files changed, 21 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index f0b2a975b..c188491b4 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -306,6 +306,13 @@ object Constructors {
}
/** $encodingof simplified `fn(realArgs)` (function application).
+ * Transforms
+ * {{{ ((x: A, y: B) => g(x, y))(c, d) }}}
+ * into
+ * {{{val x0 = c
+ * val y0 = d
+ * g(x0, y0)}}}
+ * and further simplifies it.
* @see [[purescala.Expressions.Lambda Lambda]]
* @see [[purescala.Expressions.Application Application]]
*/
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 7bae40c5b..d2b4686b6 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -3,6 +3,7 @@
package leon
package purescala
+import collection.mutable.ListBuffer
import Common._
import Definitions._
import Expressions._
@@ -10,11 +11,15 @@ import Extractors._
class ScopeSimplifier extends Transformer {
case class Scope(inScope: Set[Identifier] = Set(), oldToNew: Map[Identifier, Identifier] = Map(), funDefs: Map[FunDef, FunDef] = Map()) {
-
+
def register(oldNew: (Identifier, Identifier)): Scope = {
val newId = oldNew._2
copy(inScope = inScope + newId, oldToNew = oldToNew + oldNew)
}
+
+ def register(oldNews: Seq[(Identifier, Identifier)]): Scope = {
+ (this /: oldNews){ case (oldScope, oldNew) => oldScope.register(oldNew) }
+ }
def registerFunDef(oldNew: (FunDef, FunDef)): Scope = {
copy(funDefs = funDefs + oldNew)
@@ -37,27 +42,28 @@ class ScopeSimplifier extends Transformer {
case LetDef(fds, body: Expr) =>
var newScope: Scope = scope
// First register all functions
- val fds_newIds = for(fd <- fds) yield {
+ val fds_newIds = for(fd <- fds) yield { // Problem if some functions use the same ID for a ValDef
val newId = genId(fd.id, scope)
newScope = newScope.register(fd.id -> newId)
(fd, newId)
}
val fds_mapping = for((fd, newId) <- fds_newIds) yield {
+ val localScopeToRegister = ListBuffer[(Identifier, Identifier)]() // We record the mapping of these variables only for the function.
val newArgs = for(ValDef(id, tpe) <- fd.params) yield {
- val newArg = genId(id, newScope)
- newScope = newScope.register(id -> newArg)
+ val newArg = genId(id, newScope.register(localScopeToRegister))
+ localScopeToRegister += (id -> newArg) // This should happen only inside the function.
ValDef(newArg, tpe)
}
val newFd = fd.duplicate(id = newId, params = newArgs)
newScope = newScope.registerFunDef(fd -> newFd)
- (newFd, fd)
+ (newFd, localScopeToRegister, fd)
}
- for((newFd, fd) <- fds_mapping) {
- newFd.fullBody = rec(fd.fullBody, newScope)
+ for((newFd, localScopeToRegister, fd) <- fds_mapping) {
+ newFd.fullBody = rec(fd.fullBody, newScope.register(localScopeToRegister))
}
LetDef(fds_mapping.map(_._1), rec(body, newScope))
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index e8a78e143..b32394922 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -476,8 +476,7 @@ case object StringRender extends Rule("StringRender") {
gatherInputs(ctx, q, result +=
mergeResults(Stream((input, Nil),
(functionInvocation(
- hctx.program.library.escape.get,
- input::ctx.provided_functions.toList.map(Variable)): Expr, Nil))))
+ hctx.program.library.escape.get, List(input)): Expr, Nil))))
case BooleanType =>
val (bTemplate, vs) = booleanTemplate(input).instantiateWithVars
gatherInputs(ctx, q, result += mergeResults(Stream((BooleanToString(input), Nil), (bTemplate, vs))))
--
GitLab