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

package stainless
package extraction

import scala.language.existentials

object PartialFunctions extends inox.ast.SymbolTransformer {
  val s: xlang.trees.type = xlang.trees
  val t: xlang.trees.type = xlang.trees
  import xlang.trees._

  override def transform(symbols: Symbols): Symbols = symbols.transform(new oo.TreeTransformer {
    val s: xlang.trees.type = xlang.trees
    val t: xlang.trees.type = xlang.trees

    val optPFClass = symbols.lookup.get[ClassDef]("stainless.lang.$tilde$greater")

    override def transform(e: Expr): Expr = super.transform(e) match {
      case fi @ FunctionInvocation(ast.SymbolIdentifier("stainless.lang.PartialFunction.apply"), _, _) =>
        val FunctionInvocation(_, froms :+ to, Seq(fun)) = fi
        val ct = ClassType(optPFClass.get.id, Seq(tupleTypeWrap(froms), to))

        val (pre, body) = fun match {
          case Lambda(vds, body0) =>
            val (preOpt, bareBody) = body0 match {
              // Call to another function: Lift the function's definition
              case fi2: FunctionInvocation =>
                (exprOps.preconditionOf(fi2.inlined(symbols)), fi2)

              // scala.PartialFunction: Infer pattern match condition
              case m: MatchExpr =>
                (inferPrecondition(m), m)

              case _ =>
                (exprOps.preconditionOf(body0), exprOps.withPrecondition(body0, None))
            }

            val modifiedBody = preOpt match {
              case None => bareBody
              case Some(pre) => Assume(pre, bareBody).setPos(bareBody)
            }

            val (vd, funArgs) = vds match {
              case Seq(vd) => (vd, Seq(vd.toVariable))
              case _ =>
                val vd = ValDef(FreshIdentifier("p"), tupleTypeWrap(vds.map(_.tpe)))
                val funArgs = vds.indices.map(i => TupleSelect(vd.toVariable, i + 1))
                (vd, funArgs)
            }

            val subst = (vds zip funArgs).toMap
            val pre = Lambda(Seq(vd), exprOps.replaceFromSymbols(subst, preOpt getOrElse BooleanLiteral(true))).setPos(fi)
            val body = Lambda(Seq(vd), exprOps.replaceFromSymbols(subst, modifiedBody)).setPos(modifiedBody)
            (pre, body)

          case x =>
            throw new frontend.UnsupportedCodeException(
              fun.getPos,
              s"Unexpected $x [${x.getClass}] instead of a lambda when " +
              "unapply syntactic sugar for partial function creation.")
        }

        ClassConstructor(ct, Seq(pre, body)).setPos(fi)

      case other => other
    }

    /** Infer the partial function's precondition, by replacing every
     *  right-hand side of the pattern match with `true`.
     *  If there is only a single case, and it is a wildcard,
     *  we don't need to infer any precondition.
     */
    def inferPrecondition(body: MatchExpr): Option[Expr] = {
      val MatchExpr(scrut, cases) = body
      val rewrittenCases = cases map { c =>
        c.copy(rhs = BooleanLiteral(true).copiedFrom(c))
      }

      rewrittenCases match {
        case Seq(MatchCase(_: WildcardPattern, None, _)) =>
          None

        case cases =>
          val fallback = MatchCase(WildcardPattern(None), None, BooleanLiteral(false)).copiedFrom(body)
          Some(MatchExpr(scrut, cases :+ fallback).copiedFrom(body))
      }
    }

  })
}<commit_msg>Ported partial functions extractor to pipelined API<commit_after>/* Copyright 2009-2018 EPFL, Lausanne */

package stainless
package extraction

import scala.language.existentials

class PartialFunctions(val previous: ExtractionPhase { val t: xlang.trees.type })
  extends PipelinePhase
     with SimpleOOPhase {

  override final protected val s: xlang.trees.type = xlang.trees
  override final protected val t: xlang.trees.type = xlang.trees
  import xlang.trees._

  private class PartialFunctionsTransformer(symbols: s.Symbols) extends oo.TreeTransformer {
    override final val s: xlang.trees.type = xlang.trees
    override final val t: xlang.trees.type = xlang.trees

    val optPFClass = symbols.lookup.get[ClassDef]("stainless.lang.$tilde$greater")

    /** Infer the partial function's precondition, by replacing every
     *  right-hand side of the pattern match with `true`.
     *  If there is only a single case, and it is a wildcard,
     *  we don't need to infer any precondition.
     */
    def inferPrecondition(body: MatchExpr): Option[Expr] = {
      val MatchExpr(scrut, cases) = body
      val rewrittenCases = cases map { c =>
        c.copy(rhs = BooleanLiteral(true).copiedFrom(c))
      }

      rewrittenCases match {
        case Seq(MatchCase(_: WildcardPattern, None, _)) =>
          None

        case cases =>
          val fallback = MatchCase(WildcardPattern(None), None, BooleanLiteral(false)).copiedFrom(body)
          Some(MatchExpr(scrut, cases :+ fallback).copiedFrom(body))
      }
    }

    override def transform(e: Expr): Expr = super.transform(e) match {
      case fi @ FunctionInvocation(ast.SymbolIdentifier("stainless.lang.PartialFunction.apply"), _, _) =>
        val FunctionInvocation(_, froms :+ to, Seq(fun)) = fi
        val ct = ClassType(optPFClass.get.id, Seq(tupleTypeWrap(froms), to))

        val (pre, body) = fun match {
          case Lambda(vds, body0) =>
            val (preOpt, bareBody) = body0 match {
              // Call to another function: Lift the function's definition
              case fi2: FunctionInvocation =>
                (exprOps.preconditionOf(fi2.inlined(symbols)), fi2)

              // scala.PartialFunction: Infer pattern match condition
              case m: MatchExpr =>
                (inferPrecondition(m), m)

              case _ =>
                (exprOps.preconditionOf(body0), exprOps.withPrecondition(body0, None))
            }

            val modifiedBody = preOpt match {
              case None => bareBody
              case Some(pre) => Assume(pre, bareBody).setPos(bareBody)
            }

            val (vd, funArgs) = vds match {
              case Seq(vd) => (vd, Seq(vd.toVariable))
              case _ =>
                val vd = ValDef(FreshIdentifier("p"), tupleTypeWrap(vds.map(_.tpe)))
                val funArgs = vds.indices.map(i => TupleSelect(vd.toVariable, i + 1))
                (vd, funArgs)
            }

            val subst = (vds zip funArgs).toMap
            val pre = Lambda(Seq(vd), exprOps.replaceFromSymbols(subst, preOpt getOrElse BooleanLiteral(true))).setPos(fi)
            val body = Lambda(Seq(vd), exprOps.replaceFromSymbols(subst, modifiedBody)).setPos(modifiedBody)
            (pre, body)

          case x =>
            throw new frontend.UnsupportedCodeException(
              fun.getPos,
              s"Unexpected $x [${x.getClass}] instead of a lambda when " +
              "unapply syntactic sugar for partial function creation.")
        }

        ClassConstructor(ct, Seq(pre, body)).setPos(fi)

      case other => other
    }
  }

  final override protected def transformFunction(symbols: s.Symbols, fd: s.FunDef): t.FunDef = {
    new PartialFunctionsTransformer(symbols).transform(fd)
  }
}
{'fraction_non_alphanumeric': 0.10582672785426227, 'fraction_numerical': 0.004450006953135864, 'mean_word_length': 2.392452830188679, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 33, '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': '5628047', 'n_tokens_mistral': 2165, 'n_tokens_neox': 2061, 'n_words': 533}