<commit_before>/* Copyright 2009-2018 EPFL, Lausanne */

package stainless
package transformers

trait SimplifierWithPC extends TransformerWithPC with inox.transformers.SimplifierWithPC {
  import trees._
  import symbols._
  import exprOps.replaceFromSymbols

  def pp = implicitly[PathProvider[CNFPath]]

  override protected def simplify(e: Expr, path: CNFPath): (Expr, Boolean) = e match {
    case Assert(pred, oerr, body) => simplify(pred, path) match {
      case (BooleanLiteral(true), true) => simplify(body, path)
      case (BooleanLiteral(false), true) =>
        val (rb, _) = simplify(body, path)
        (Assert(BooleanLiteral(false).copiedFrom(e), oerr, rb).copiedFrom(e), opts.assumeChecked)
      case (rp, _) =>
        val (rb, _) = simplify(body, path withCond rp)
        (Assert(rp, oerr, rb).copiedFrom(e), opts.assumeChecked)
    }

    case MatchExpr(scrut, cases) =>
      val (rs, ps) = simplify(scrut, path)
      val (_, stop, purity, newCases) = cases.foldLeft((path, false, ps, Seq[MatchCase]())) {
        case (p @ (_, true, _, _), _) => p
        case ((soFar, _, purity, newCases), MatchCase(pattern, guard, rhs)) =>
          simplify(conditionForPattern[Path](rs, pattern, includeBinders = false).fullClause, soFar) match {
            case (BooleanLiteral(false), true) => (soFar, false, purity, newCases)
            case (rc, pc) =>
              val path = conditionForPattern[CNFPath](rs, pattern, includeBinders = true)
              val (rg, pg) = guard.map(simplify(_, soFar merge path)).getOrElse((BooleanLiteral(true), true))
              (and(rc, rg), pc && pg) match {
                case (BooleanLiteral(false), true) => (soFar, false, purity, newCases)
                case (BooleanLiteral(true), true) =>
                  // We know path withCond rg is true here but we need the binders
                  val (rr, pr) = simplify(rhs, soFar merge path)
                  (soFar, true, purity && pr, newCases :+ MatchCase(pattern, None, rr))

                case (_, _) =>
                  val (rr, pr) = simplify(rhs, soFar merge (path withCond rg))
                  val newGuard = if (rg == BooleanLiteral(true)) None else Some(rg)
                  (
                    soFar merge (path withCond rg).negate,
                    false,
                    purity && pc && pg && pr,
                    newCases :+ MatchCase(pattern, newGuard, rr)
                  )
              }
          }
      }

      newCases match {
        case Seq(MatchCase(pattern, guard, rhs)) if stop =>
          val map = mapForPattern(rs, pattern)
          simplify(replaceFromSymbols(map, rhs), guard map (path withCond _) getOrElse path)
        case _ =>
        (MatchExpr(rs, newCases), purity)
      }

    case _ => super.simplify(e, path)
  }
}<commit_msg>Small fixes in match simplifier<commit_after>/* Copyright 2009-2018 EPFL, Lausanne */

package stainless
package transformers

trait SimplifierWithPC extends TransformerWithPC with inox.transformers.SimplifierWithPC {
  import trees._
  import symbols._
  import exprOps.replaceFromSymbols

  def pp = implicitly[PathProvider[CNFPath]]

  override protected def simplify(e: Expr, path: CNFPath): (Expr, Boolean) = e match {
    case Assert(pred, oerr, body) => simplify(pred, path) match {
      case (BooleanLiteral(true), true) => simplify(body, path)
      case (BooleanLiteral(false), true) =>
        val (rb, _) = simplify(body, path)
        (Assert(BooleanLiteral(false).copiedFrom(e), oerr, rb).copiedFrom(e), opts.assumeChecked)
      case (rp, _) =>
        val (rb, _) = simplify(body, path withCond rp)
        (Assert(rp, oerr, rb).copiedFrom(e), opts.assumeChecked)
    }

    case MatchExpr(scrut, cases) =>
      val (rs, ps) = simplify(scrut, path)
      val (_, stop, purity, newCases) = cases.foldLeft((path, false, ps, Seq[MatchCase]())) {
        case (p @ (_, true, _, _), _) => p
        case ((soFar, _, purity, newCases), MatchCase(pattern, guard, rhs)) =>
          simplify(conditionForPattern[Path](rs, pattern, includeBinders = false).fullClause, soFar) match {
            case (BooleanLiteral(false), true) => (soFar, false, purity, newCases)
            case (rc, pc) =>
              val path = conditionForPattern[CNFPath](rs, pattern, includeBinders = true)
              val (rg, pg) = guard.map(simplify(_, soFar merge path)).getOrElse((BooleanLiteral(true), true))
              (and(rc, rg), pc && pg) match {
                case (BooleanLiteral(false), true) => (soFar, false, purity, newCases)
                case (BooleanLiteral(true), true) =>
                  // We know path withCond rg is true here but we need the binders
                  val bindings = conditionForPattern[Path](rs, pattern, includeBinders = true).bindings
                  val (rr, pr) = simplify(bindings.foldRight(rhs) { case ((i, e), b) => Let(i, e, b) }, soFar)
                  (soFar, true, purity && pr, newCases :+ MatchCase(WildcardPattern(None).copiedFrom(pattern), None, rr))

                case (_, _) =>
                  val (rr, pr) = simplify(rhs, soFar merge (path withCond rg))
                  val newGuard = if (rg == BooleanLiteral(true)) None else Some(rg)
                  (
                    soFar merge (path withCond rg).negate,
                    false,
                    purity && pc && pg && pr,
                    newCases :+ MatchCase(pattern, newGuard, rr)
                  )
              }
          }
      }

      newCases match {
        case Seq() => (
          Assert(
            BooleanLiteral(false).copiedFrom(e),
            Some("No valid case"),
            Choose(
              ValDef(FreshIdentifier("res"), e.getType, Set.empty).copiedFrom(e),
              BooleanLiteral(true).copiedFrom(e)
            ).copiedFrom(e)
          ).copiedFrom(e),
          opts.assumeChecked
        )

        case Seq(MatchCase(WildcardPattern(None), None, rhs)) if stop => (rhs, purity)
        case _ => (MatchExpr(rs, newCases).copiedFrom(e), purity)
      }

    case _ => super.simplify(e, path)
  }
}
{'fraction_non_alphanumeric': 0.12723690691183714, 'fraction_numerical': 0.0026268264652766376, 'mean_word_length': 2.292972972972973, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 35, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7059276', 'n_tokens_mistral': 1908, 'n_tokens_neox': 1789, 'n_words': 478}