From bd41adafc0aab8a1e33550338d486f864b3e5e8d Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 12 Apr 2016 16:57:55 +0200
Subject: [PATCH] Tree and def Transformers handle letdef and letvar
---
.../purescala/DefinitionTransformer.scala | 6 ++++++
.../leon/purescala/TreeTransformer.scala | 4 ++++
.../scala/leon/xlang/AntiAliasingPhase.scala | 1 +
.../xlang/valid/ExpressionOrder1.scala | 19 +++++++++++++++++++
4 files changed, 30 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/valid/ExpressionOrder1.scala
diff --git a/src/main/scala/leon/purescala/DefinitionTransformer.scala b/src/main/scala/leon/purescala/DefinitionTransformer.scala
index d0008e5b6..abe08fa34 100644
--- a/src/main/scala/leon/purescala/DefinitionTransformer.scala
+++ b/src/main/scala/leon/purescala/DefinitionTransformer.scala
@@ -34,6 +34,12 @@ class DefinitionTransformer(
idMap += id -> nid
nid
})
+
+ case LetDef(fds, body) =>
+ val rFds = fds map transform
+ val rBody = transform(body)
+ LetDef(rFds, rBody).copiedFrom(e)
+
case _ => super.transform(e)
}
diff --git a/src/main/scala/leon/purescala/TreeTransformer.scala b/src/main/scala/leon/purescala/TreeTransformer.scala
index 77a5659f1..d74da4f8f 100644
--- a/src/main/scala/leon/purescala/TreeTransformer.scala
+++ b/src/main/scala/leon/purescala/TreeTransformer.scala
@@ -6,6 +6,7 @@ package purescala
import Common._
import Definitions._
import Expressions._
+import xlang.Expressions._
import Extractors._
import Types._
@@ -34,6 +35,9 @@ trait TreeTransformer {
case Let(a, expr, body) =>
val newA = transform(a)
Let(newA, transform(expr), transform(body)(bindings + (a -> newA))).copiedFrom(e)
+ case LetVar(a, expr, body) =>
+ val newA = transform(a)
+ LetVar(newA, transform(expr), transform(body)(bindings + (a -> newA))).copiedFrom(e)
case CaseClass(cct, args) =>
CaseClass(transform(cct).asInstanceOf[CaseClassType], args map transform).copiedFrom(e)
case CaseClassSelector(cct, caseClass, selector) =>
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index b721a9472..063694add 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -84,6 +84,7 @@ object AntiAliasingPhase extends TransformationPhase {
} {
updatedFunctions += (fd -> updateFunDef(fd, effects)(ctx))
}
+ //println(updatedFunctions.filter(p => p._1.id != p._2.id).mkString("\n"))
for {
fd <- fds
diff --git a/src/test/resources/regression/verification/xlang/valid/ExpressionOrder1.scala b/src/test/resources/regression/verification/xlang/valid/ExpressionOrder1.scala
new file mode 100644
index 000000000..c34d2057e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ExpressionOrder1.scala
@@ -0,0 +1,19 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+import leon.lang._
+
+object NestedFunState8 {
+
+ def test1 = {
+ var x = 0
+
+ def bar(y: Int) = {
+ def fun(z: Int) = 1 * x * (y + z)
+
+ fun(3)
+ }
+
+ bar(2) == 0
+ }.holds
+
+}
--
GitLab