Removed matchExpr in transformers

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

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)

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)
 }
 

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)