Revert "Focus removes input variables to not depend on EquivalentInputs"

This reverts commit 4da35a7a.

src/main/scala/leon/repair/rules/Focus.scala

@@ -4,6 +4,9 @@ package leon
 package repair
 package rules
 
+import synthesis._
+import leon.evaluators._
+
 import purescala.Path
 import purescala.Expressions._
 import purescala.Common._
@@ -12,11 +15,8 @@ import purescala.ExprOps._
 import purescala.Constructors._
 import purescala.Extractors._
 
-import utils.fixpoint
-import evaluators._
-
-import synthesis._
 import Witnesses._
+
 import graph.AndNode
 
 case object Focus extends PreprocessingRule("Focus") {
@@ -146,64 +146,33 @@ case object Focus extends PreprocessingRule("Focus") {
           val map  = mapForPattern(scrut, c.pattern)
 
           val thisCond = matchCaseCondition(scrut, c)
-          val prevPCSoFar = pcSoFar
           val cond = pcSoFar merge thisCond
           pcSoFar = pcSoFar merge thisCond.negate
 
           val subP = if (existsFailing(cond.toClause, map, evaluator)) {
-
             val vars = map.toSeq.map(_._1)
 
-            val (p2e, _) = patternToExpression(c.pattern, scrut.getType)
-
-            val substAs = ((scrut, p2e) match {
-              case (Variable(i), _) if p.as.contains(i) => Seq(i -> p2e)
-              case (Tuple(as), Tuple(tos)) =>
-                val res = as.zip(tos) collect {
-                  case (Variable(i), to) if p.as.contains(i) => i -> to
-                }
-                if (res.size == as.size) res else Nil
-            }).toMap
-
-            if (substAs.nonEmpty) {
-              val subst: Expr => Expr = { e =>
-                replaceFromIDs(substAs, e)
-              }
-              // FIXME intermediate binders??
-              val newAs = (p.as diff substAs.keys.toSeq) ++ vars
-              val newPc = (p.pc merge prevPCSoFar) map subst
-              val newWs = subst(ws(c.rhs))
-              val newPhi = subst(p.phi)
-              val eb2 = qeb.filterIns(cond.toClause).removeIns(substAs.keySet)
-              val ebF: Seq[Expr] => List[Seq[Expr]] = { (ins: Seq[Expr]) =>
-                val eval = evaluator.eval(tupleWrap(vars map Variable), p.as.zip(ins).toMap ++ map)
-                eval.result.map( r => ins ++ unwrapTuple(r, vars.size)).toList
-              }
-              val newEb = eb2 flatMapIns ebF
-              Some(Problem(newAs, newWs, newPc, newPhi, p.xs, newEb))
-            } else {
-              // Filter tests by the path-condition
-              val eb2 = qeb.filterIns(cond.toClause)
+            // Filter tests by the path-condition
+            val eb2 = qeb.filterIns(cond.toClause)
 
-              // Augment test with the additional variables and their valuations
-              val ebF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
-                val emap = (p.as zip e).toMap
+            // Augment test with the additional variables and their valuations
+            val ebF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
+              val emap = (p.as zip e).toMap
 
-                evaluator.eval(tupleWrap(vars.map(map)), emap).result.map { r =>
-                  e ++ unwrapTuple(r, vars.size)
-                }.toList
-              }
+              evaluator.eval(tupleWrap(vars.map(map)), emap).result.map { r =>
+                e ++ unwrapTuple(r, vars.size)
+              }.toList
+            }
 
-              val eb3 = if (vars.nonEmpty) {
-                eb2.flatMapIns(ebF)
-              } else {
-                eb2.eb
-              }
+            val eb3 = if (vars.nonEmpty) {
+              eb2.flatMapIns(ebF)
+            } else {
+              eb2.eb
+            }
 
-              val newPc = cond withBindings vars.map(id => id -> map(id))
+            val newPc = cond withBindings vars.map(id => id -> map(id))
 
-              Some(Problem(p.as, ws(c.rhs), p.pc merge newPc, p.phi, p.xs, eb3))
-            }
+            Some(Problem(p.as, ws(c.rhs), p.pc merge newPc, p.phi, p.xs, eb3))
           } else {
             None
           }