From 07e68e9968ecaa5bb066a910cc379bd666a531dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 26 Apr 2012 21:01:50 +0200
Subject: [PATCH] Refusing nested epsilon
---
src/main/scala/leon/plugin/CodeExtraction.scala | 4 ++++
src/main/scala/leon/purescala/Trees.scala | 12 ++++++++++++
testcases/regression/Epsilon6.scala | 13 -------------
3 files changed, 16 insertions(+), 13 deletions(-)
delete mode 100644 testcases/regression/Epsilon6.scala
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index a0c757941..32e600e95 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -570,6 +570,10 @@ trait CodeExtraction extends Extractors {
case Some(f) => varSubsts(varSym) = f
case None => varSubsts.remove(varSym)
}
+ if(containsEpsilon(c1)) {
+ unit.error(epsi.pos, "Usage of nested epsilon is not allowed.")
+ throw ImpureCodeEncounteredException(epsi)
+ }
Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
}
case ExSomeConstruction(tpe, arg) => {
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index f9d0498f0..638db0c20 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -818,6 +818,18 @@ object Trees {
treeCatamorphism(convert, combine, compute, expr)
}
+ def containsEpsilon(expr: Expr): Boolean = {
+ def convert(t : Expr) : Boolean = t match {
+ case (l : Epsilon) => true
+ case _ => false
+ }
+ def combine(c1 : Boolean, c2 : Boolean) : Boolean = c1 || c2
+ def compute(t : Expr, c : Boolean) = t match {
+ case (l : Epsilon) => true
+ case _ => c
+ }
+ treeCatamorphism(convert, combine, compute, expr)
+ }
def containsLetDef(expr: Expr): Boolean = {
def convert(t : Expr) : Boolean = t match {
case (l : LetDef) => true
diff --git a/testcases/regression/Epsilon6.scala b/testcases/regression/Epsilon6.scala
deleted file mode 100644
index a0d5b959c..000000000
--- a/testcases/regression/Epsilon6.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-import leon.Utils._
-
-object Epsilon6 {
-
- def fooWrong(): Int = {
- epsilon((y: Int) => y > epsilon((z: Int) => z < y))
- } ensuring(_ >= 0)
-
- def foo(): Int = {
- epsilon((y: Int) => y > epsilon((z: Int) => z < y))
- } ensuring(res => res >= 0 || res < 0)
-
-}
--
GitLab