diff --git a/src/main/scala/inox/transformers/ScopeSimplifier.scala b/src/main/scala/inox/transformers/ScopeSimplifier.scala
index e4a2404bf61c03424f2ee3987db4fb8bddbf0cc9..a74653eea5abf1034afb5b47bb8673e950bc3d01 100644
--- a/src/main/scala/inox/transformers/ScopeSimplifier.scala
+++ b/src/main/scala/inox/transformers/ScopeSimplifier.scala
@@ -6,6 +6,7 @@ package transformers
/** Simplifies variable ids in scope */
trait ScopeSimplifier extends Transformer {
import trees._
+
case class Scope(inScope: Set[ValDef] = Set(), oldToNew: Map[ValDef, ValDef] = Map(), funDefs: Map[Identifier, Identifier] = Map()) {
def register(oldNew: (ValDef, ValDef)): Scope = {
@@ -36,49 +37,6 @@ trait ScopeSimplifier extends Transformer {
val sb = rec(b, scope.register(i -> si))
Let(si, se, sb)
- case MatchExpr(scrut, cases) =>
- val rs = rec(scrut, scope)
-
- def trPattern(p: Pattern, scope: Scope): (Pattern, Scope) = {
- val (newBinder, newScope) = p.binder match {
- case Some(id) =>
- val newId = genId(id, scope)
- val newScope = scope.register(id -> newId)
- (Some(newId), newScope)
- case None =>
- (None, scope)
- }
-
- var curScope = newScope
- val newSubPatterns = for (sp <- p.subPatterns) yield {
- val (subPattern, subScope) = trPattern(sp, curScope)
- curScope = subScope
- subPattern
- }
-
- val newPattern = p match {
- case InstanceOfPattern(b, ctd) =>
- InstanceOfPattern(newBinder, ctd)
- case WildcardPattern(b) =>
- WildcardPattern(newBinder)
- case CaseClassPattern(b, ccd, sub) =>
- CaseClassPattern(newBinder, ccd, newSubPatterns)
- case TuplePattern(b, sub) =>
- TuplePattern(newBinder, newSubPatterns)
- case UnapplyPattern(b, fd, obj, sub) =>
- UnapplyPattern(newBinder, fd, obj, newSubPatterns)
- case LiteralPattern(_, lit) =>
- LiteralPattern(newBinder, lit)
- }
-
- (newPattern, curScope)
- }
-
- MatchExpr(rs, cases.map { c =>
- val (newP, newScope) = trPattern(c.pattern, scope)
- MatchCase(newP, c.optGuard map {rec(_, newScope)}, rec(c.rhs, newScope))
- })
-
case v: Variable =>
val vd = v.toVal
scope.oldToNew.getOrElse(vd, vd).toVariable
diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala
index 8161240c7adb0f740f519c9838fc82c010c7a02f..cb00e5ac16b3031d27a65e1164f9ee1d302f68ac 100644
--- a/src/main/scala/inox/transformers/SimplifierWithPC.scala
+++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala
@@ -7,7 +7,7 @@ package transformers
trait SimplifierWithPC extends TransformerWithPC {
import trees._
- import symbols.{Path, matchExpr, matchExprCaseConditions}
+ import symbols.Path
implicit protected val s = symbols
@@ -18,9 +18,6 @@ trait SimplifierWithPC extends TransformerWithPC {
protected def sat(e: Expr) : Boolean
protected override def rec(e: Expr, path: Path) = e match {
- case Require(pre, body) if impliedBy(pre, path) =>
- body
-
case IfExpr(cond, thenn, _) if impliedBy(cond, path) =>
rec(thenn, path)
@@ -47,47 +44,13 @@ trait SimplifierWithPC extends TransformerWithPC {
case Implies(lhs, rhs) if contradictedBy(lhs, path) =>
BooleanLiteral(true).copiedFrom(e)
- case me @ MatchExpr(scrut, cases) =>
- val rs = rec(scrut, path)
-
- var stillPossible = true
-
- val conds = matchExprCaseConditions(me, path)
-
- val newCases = cases.zip(conds).flatMap { case (cs, cond) =>
- if (stillPossible && sat(cond.toClause)) {
-
- if (valid(cond.toClause)) {
- stillPossible = false
- }
-
- Seq((cs match {
- case SimpleCase(p, rhs) =>
- SimpleCase(p, rec(rhs, cond))
- case GuardedCase(p, g, rhs) =>
- val newGuard = rec(g, cond)
- if (valid(newGuard))
- SimpleCase(p, rec(rhs,cond))
- else
- GuardedCase(p, newGuard, rec(rhs, cond withCond newGuard))
- }).copiedFrom(cs))
- } else {
- Seq()
- }
- }
-
- newCases match {
- case List() =>
- Error(e.getType, "Unreachable code").copiedFrom(e)
- case _ =>
- matchExpr(rs, newCases).copiedFrom(e)
- }
-
- case a @ Assert(pred, _, body) if impliedBy(pred, path) =>
+ case a @ Assume(pred, body) if impliedBy(pred, path) =>
body
- case a @ Assert(pred, msg, body) if contradictedBy(pred, path) =>
+ /* @nv TODO. what are we supposed to do here!?
+ case a @ Assume(pred, body) if contradictedBy(pred, path) =>
Error(body.getType, s"Assertion failed: $msg").copiedFrom(a)
+ */
case b if b.getType == BooleanType && impliedBy(b, path) =>
BooleanLiteral(true).copiedFrom(b)
diff --git a/src/main/scala/inox/transformers/Transformer.scala b/src/main/scala/inox/transformers/Transformer.scala
index 1faa3275561a4657e73450428c8c7437c473697d..79f317710d758c07cf07b87046fe6e678b231536 100644
--- a/src/main/scala/inox/transformers/Transformer.scala
+++ b/src/main/scala/inox/transformers/Transformer.scala
@@ -29,6 +29,6 @@ trait Transformer {
/** Transform an [[Expr]] with the initial environment */
def transform(e: Expr): Expr = transform(e, initEnv)
/** Transform the body of a [[FunDef]] */
- def transform(fd: FunDef): Expr = transform(fd.fullBody)
+ def transform(fd: FunDef): Option[Expr] = fd.body.map(transform)
}
diff --git a/src/main/scala/inox/transformers/TransformerWithPC.scala b/src/main/scala/inox/transformers/TransformerWithPC.scala
index ecda40920e7e754d9d4cc058d5184fdc4fcdcafe..8ee56a8121d2a29afb26b9e4e8583358ad86757b 100644
--- a/src/main/scala/inox/transformers/TransformerWithPC.scala
+++ b/src/main/scala/inox/transformers/TransformerWithPC.scala
@@ -17,51 +17,10 @@ trait TransformerWithPC extends Transformer {
val sb = rec(b, path withBinding (i -> se))
Let(i, se, sb).copiedFrom(e)
- case Ensuring(req @ Require(pre, body), lam @ Lambda(Seq(arg), post)) =>
- val spre = rec(pre, path)
- val sbody = rec(body, path withCond spre)
- val spost = rec(post, path withCond spre withBinding (arg -> sbody))
- Ensuring(
- Require(spre, sbody).copiedFrom(req),
- Lambda(Seq(arg), spost).copiedFrom(lam)
- ).copiedFrom(e)
-
- case Ensuring(body, lam @ Lambda(Seq(arg), post)) =>
- val sbody = rec(body, path)
- val spost = rec(post, path withBinding (arg -> sbody))
- Ensuring(
- sbody,
- Lambda(Seq(arg), spost).copiedFrom(lam)
- ).copiedFrom(e)
-
- case Require(pre, body) =>
- val sp = rec(pre, path)
- val sb = rec(body, path withCond pre)
- Require(sp, sb).copiedFrom(e)
-
- //@mk: TODO Discuss if we should include asserted predicates in the pc
- //case Assert(pred, err, body) =>
- // val sp = rec(pred, path)
- // val sb = rec(body, register(sp, path))
- // Assert(sp, err, sb).copiedFrom(e)
-
- case MatchExpr(scrut, cases) =>
- val rs = rec(scrut, path)
-
- var soFar = path
-
- MatchExpr(rs, cases.map { c =>
- val patternPathPos = conditionForPattern(rs, c.pattern, includeBinders = true)
- val patternPathNeg = conditionForPattern(rs, c.pattern, includeBinders = false)
- val map = mapForPattern(rs, c.pattern)
- val guardOrTrue = c.optGuard.getOrElse(BooleanLiteral(true))
- val guardMapped = replaceFromSymbols(map, guardOrTrue)
-
- val subPath = soFar merge (patternPathPos withCond guardOrTrue)
- soFar = soFar merge (patternPathNeg withCond guardMapped).negate
-
- MatchCase(c.pattern, c.optGuard, rec(c.rhs, subPath)).copiedFrom(c)
- }).copiedFrom(e)
+ case Assume(pred, body) =>
+ val sp = rec(pred, path)
+ val sb = rec(body, path withCond sp)
+ Assume(sp, sb).copiedFrom(e)
case IfExpr(cond, thenn, elze) =>
val rc = rec(cond, path)