diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala index 29ff5341da5b97ae45c6940c1a4575103a506cd6..47c0be1391b1f799a1a45ccfb9cc9b30351678c8 100644 --- a/src/main/scala/leon/FunctionClosure.scala +++ b/src/main/scala/leon/FunctionClosure.scala @@ -112,7 +112,7 @@ object FunctionClosure extends Pass { pathConstraints = pathConstraints.tail IfExpr(rCond, rThen, rElze).setType(i.getType) } - case m @ MatchExpr(scrut,cses) => { + case m @ MatchExpr(scrut,cses) => { //TODO: will not work if there are actual nested function in cases //val rScrut = functionClosure(scrut, bindedVars) m } diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala index 26e3b586d0f7e96972016b6f818e310a35d967f6..d0753ec6580919ca8764859771ed406ce1faf0a4 100644 --- a/src/main/scala/leon/plugin/CodeExtraction.scala +++ b/src/main/scala/leon/plugin/CodeExtraction.scala @@ -359,7 +359,14 @@ trait CodeExtraction extends Extractors { if(cd.guard == EmptyTree) { SimpleCase(pat2pat(cd.pat), rec(cd.body)) } else { - GuardedCase(pat2pat(cd.pat), rec(cd.guard), rec(cd.body)) + val recPattern = pat2pat(cd.pat) + val recGuard = rec(cd.guard) + val recBody = rec(cd.body) + if(!isPure(recGuard)) { + unit.error(cd.guard.pos, "Guard expression must be pure") + throw ImpureCodeEncounteredException(cd) + } + GuardedCase(recPattern, recGuard, recBody) } } diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala index c05bdaf549f099a5606f72653782efaffa26596a..bb90f60c3e63267734ecbfe29d8e6ce15dcf90c9 100644 --- a/src/main/scala/leon/purescala/Trees.scala +++ b/src/main/scala/leon/purescala/Trees.scala @@ -35,8 +35,6 @@ object Trees { def setInvariant(inv: Option[Expr]) = { invariant = inv; this } } - - /* This describes computational errors (unmatched case, taking min of an * empty set, division by zero, etc.). It should always be typed according to * the expected type. */ @@ -764,6 +762,24 @@ object Trees { searchAndReplaceDFS(applyToTree)(expr) } + //checking whether the expr is pure, that is do not contains any non-pure construct: assign, while and blocks + def isPure(expr: Expr): Boolean = { + def convert(t: Expr) : Boolean = t match { + case Block(_, _) => false + case Assignment(_, _) => false + case While(_, _) => false + case _ => true + } + def combine(b1: Boolean, b2: Boolean) = b1 && b2 + def compute(e: Expr, b: Boolean) = e match { + case Block(_, _) => false + case Assignment(_, _) => false + case While(_, _) => false + case _ => true + } + treeCatamorphism(convert, combine, compute, expr) + } + def variablesOf(expr: Expr) : Set[Identifier] = { def convert(t: Expr) : Set[Identifier] = t match { case Variable(i) => Set(i)