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

package stainless
package extraction
package imperative

trait ImperativeCodeElimination
  extends oo.CachingPhase
     with SimpleFunctions
     with IdentitySorts
     with oo.IdentityClasses
     with oo.IdentityTypeDefs
     with SimplyCachedFunctions
     with SimplyCachedSorts
     with oo.SimplyCachedClasses {

  val s: Trees
  val t: s.type
  import s._

  override protected type TransformerContext = s.Symbols
  override protected def getContext(symbols: s.Symbols) = symbols

  override protected def extractFunction(symbols: s.Symbols, fd: s.FunDef): t.FunDef = {
    import symbols._
    import exprOps._

    /* varsInScope refers to variable declared in the same level scope.
     * Typically, when entering a nested function body, the scope should be
     * reset to empty */
    case class State(
      parent: FunDef,
      varsInScope: Set[Variable],
      localsMapping: Map[Identifier, (LocalFunDef, Seq[Variable])]
    ) {
      def withVar(vd: ValDef) = copy(varsInScope = varsInScope + vd.toVariable)
      def withLocal(id: Identifier, fd: LocalFunDef, vars: Seq[Variable]) =
        copy(localsMapping = localsMapping + (id -> (fd, vars)))
    }

    //return a "scope" consisting of purely functional code that defines potentially needed
    //new variables (val, not var) and a mapping for each modified variable (var, not val :) )
    //to their new name defined in the scope. The first returned valued is the value of the expression
    //that should be introduced as such in the returned scope (the val already refers to the new names)
    def toFunction(expr: Expr)(implicit state: State): (Expr, Expr => Expr, Map[Variable, Variable]) = {
      import state._
      expr match {
        case LetVar(vd, e, b) =>
          val newVd = vd.freshen
          val (rhsVal, rhsScope, rhsFun) = toFunction(e)
          val (bodyRes, bodyScope, bodyFun) = toFunction(b)(state.withVar(vd))
          val newSubst = rhsFun + (vd.toVariable -> newVd.toVariable)
          val scope = (body: Expr) => rhsScope(Let(newVd, rhsVal, replaceFromSymbols(newSubst, bodyScope(body))).copiedFrom(expr))
          (bodyRes, scope, newSubst ++ bodyFun)

        case Assignment(v, e) =>
          assert(varsInScope.contains(v))
          val newVd = v.toVal.freshen
          val (rhsVal, rhsScope, rhsFun) = toFunction(e)
          val scope = (body: Expr) => rhsScope(Let(newVd, rhsVal, body).copiedFrom(expr))
          (UnitLiteral(), scope, rhsFun + (v -> newVd.toVariable))

        case Snapshot(e) => toFunction(e)

        case ite @ IfExpr(cond, tExpr, eExpr) =>
          val (cRes, cScope, cFun) = toFunction(cond)
          val (tRes, tScope, tFun) = toFunction(tExpr)
          val (eRes, eScope, eFun) = toFunction(eExpr)

          val modifiedVars: Seq[Variable] = (tFun.keys ++ eFun.keys).toSet.intersect(varsInScope).toSeq
          val res = ValDef.fresh("res", ite.getType)
          val freshVars = modifiedVars.map(_.freshen)
          val iteType = tupleTypeWrap(res.tpe +: freshVars.map(_.tpe))

          val thenVal = tupleWrap(tRes +: modifiedVars.map(v => tFun.getOrElse(v, v)))
          val elseVal = tupleWrap(eRes +: modifiedVars.map(v => eFun.getOrElse(v, v)))
          val iteExpr = IfExpr(cRes, replaceFromSymbols(cFun, tScope(thenVal)), replaceFromSymbols(cFun, eScope(elseVal))).copiedFrom(ite)

          val scope = (body: Expr) => {
            val tupleVd = ValDef.fresh("t", iteType)
            cScope(Let(tupleVd, iteExpr, Let(
              res,
              tupleSelect(tupleVd.toVariable, 1, modifiedVars.nonEmpty),
              freshVars.zipWithIndex.foldLeft(body)((b, p) =>
                Let(p._1.toVal, tupleSelect(tupleVd.toVariable, p._2 + 2, true), b)
              ))
            ).copiedFrom(expr))
          }

          (res.toVariable, scope, cFun ++ (modifiedVars zip freshVars))

        case m @ MatchExpr(scrut, cses) =>
          val csesRhs = cses.map(_.rhs) //we can ignore pattern, and the guard is required to be pure
          val (csesRes, csesScope, csesFun) = csesRhs.map(toFunction).unzip3
          val (scrutRes, scrutScope, scrutFun) = toFunction(scrut)

          val modifiedVars: Seq[Variable] = csesFun.flatMap(_.keys).toSet.intersect(varsInScope).toSeq
          val res = ValDef.fresh("res", m.getType)
          val freshVars = modifiedVars.map(_.freshen)
          val matchType = tupleTypeWrap(res.tpe +: freshVars.map(_.tpe))

          val csesVals = csesRes.zip(csesFun).map {
            case (cRes, cFun) => tupleWrap(cRes +: modifiedVars.map(v => cFun.getOrElse(v, v)))
          }

          val newRhs = csesVals.zip(csesScope).map {
            case (cVal, cScope) => replaceFromSymbols(scrutFun, cScope(cVal))
          }

          val matchE = MatchExpr(scrutRes, cses.zip(newRhs).map {
            case (mc @ MatchCase(pat, guard, _), newRhs) =>
              //guard need to update ids (substitution of new names, and new fundef)
              //but wont have side effects
              MatchCase(pat, guard.map { g =>
                val (resGuard, scopeGuard, _) = toFunction(g)
                replaceFromSymbols(scrutFun, scopeGuard(resGuard))
              }, newRhs).copiedFrom(mc)
          }).copiedFrom(m)

          val scope = (body: Expr) => {
            val tupleVd = ValDef.fresh("t", matchType)
            scrutScope(
              Let(tupleVd, matchE,
                Let(res, tupleSelect(tupleVd.toVariable, 1, freshVars.nonEmpty),
                  freshVars.zipWithIndex.foldLeft(body)((b, p) =>
                    Let(p._1.toVal, tupleSelect(tupleVd.toVariable, p._2 + 2, true), b)
                  )
                )
              )
            )
          }

          (res.toVariable, scope, scrutFun ++ (modifiedVars zip freshVars))

        case wh @ While(cond, body, optInv) =>
          val id = FreshIdentifier(parent.id.name + "While")
          val tpe = FunctionType(Seq(), UnitType().copiedFrom(wh)).copiedFrom(wh)<commit_msg>Some positions in ImperativeCodeEliminations<commit_after>/* Copyright 2009-2018 EPFL, Lausanne */

package stainless
package extraction
package imperative

trait ImperativeCodeElimination
  extends oo.CachingPhase
     with SimpleFunctions
     with IdentitySorts
     with oo.IdentityClasses
     with oo.IdentityTypeDefs
     with SimplyCachedFunctions
     with SimplyCachedSorts
     with oo.SimplyCachedClasses {

  val s: Trees
  val t: s.type
  import s._

  override protected type TransformerContext = s.Symbols
  override protected def getContext(symbols: s.Symbols) = symbols

  override protected def extractFunction(symbols: s.Symbols, fd: s.FunDef): t.FunDef = {
    import symbols._
    import exprOps._

    /* varsInScope refers to variable declared in the same level scope.
     * Typically, when entering a nested function body, the scope should be
     * reset to empty */
    case class State(
      parent: FunDef,
      varsInScope: Set[Variable],
      localsMapping: Map[Identifier, (LocalFunDef, Seq[Variable])]
    ) {
      def withVar(vd: ValDef) = copy(varsInScope = varsInScope + vd.toVariable)
      def withLocal(id: Identifier, fd: LocalFunDef, vars: Seq[Variable]) =
        copy(localsMapping = localsMapping + (id -> (fd, vars)))
    }

    //return a "scope" consisting of purely functional code that defines potentially needed
    //new variables (val, not var) and a mapping for each modified variable (var, not val :) )
    //to their new name defined in the scope. The first returned valued is the value of the expression
    //that should be introduced as such in the returned scope (the val already refers to the new names)
    def toFunction(expr: Expr)(implicit state: State): (Expr, Expr => Expr, Map[Variable, Variable]) = {
      import state._
      expr match {
        case LetVar(vd, e, b) =>
          val newVd = vd.freshen
          val (rhsVal, rhsScope, rhsFun) = toFunction(e)
          val (bodyRes, bodyScope, bodyFun) = toFunction(b)(state.withVar(vd))
          val newSubst = rhsFun + (vd.toVariable -> newVd.toVariable)
          val scope = (body: Expr) => rhsScope(Let(newVd, rhsVal, replaceFromSymbols(newSubst, bodyScope(body))).copiedFrom(expr))
          (bodyRes, scope, newSubst ++ bodyFun)

        case Assignment(v, e) =>
          assert(varsInScope.contains(v))
          val newVd = v.toVal.freshen
          val (rhsVal, rhsScope, rhsFun) = toFunction(e)
          val scope = (body: Expr) => rhsScope(Let(newVd, rhsVal, body).copiedFrom(expr))
          (UnitLiteral(), scope, rhsFun + (v -> newVd.toVariable))

        case Snapshot(e) => toFunction(e)

        case ite @ IfExpr(cond, tExpr, eExpr) =>
          val (cRes, cScope, cFun) = toFunction(cond)
          val (tRes, tScope, tFun) = toFunction(tExpr)
          val (eRes, eScope, eFun) = toFunction(eExpr)

          val modifiedVars: Seq[Variable] = (tFun.keys ++ eFun.keys).toSet.intersect(varsInScope).toSeq
          val res = ValDef.fresh("res", ite.getType)
          val freshVars = modifiedVars.map(_.freshen)
          val iteType = tupleTypeWrap(res.tpe +: freshVars.map(_.tpe))

          val thenVal = tupleWrap(tRes +: modifiedVars.map(v => tFun.getOrElse(v, v)))
          val elseVal = tupleWrap(eRes +: modifiedVars.map(v => eFun.getOrElse(v, v)))
          val iteExpr = IfExpr(cRes, replaceFromSymbols(cFun, tScope(thenVal)), replaceFromSymbols(cFun, eScope(elseVal))).copiedFrom(ite)

          val scope = (body: Expr) => {
            val tupleVd = ValDef.fresh("t", iteType)
            cScope(Let(tupleVd, iteExpr, Let(
              res,
              tupleSelect(tupleVd.toVariable, 1, modifiedVars.nonEmpty),
              freshVars.zipWithIndex.foldLeft(body)((b, p) =>
                Let(p._1.toVal, tupleSelect(tupleVd.toVariable, p._2 + 2, true), b)
              ))
            ).copiedFrom(expr))
          }

          (res.toVariable, scope, cFun ++ (modifiedVars zip freshVars))

        case m @ MatchExpr(scrut, cses) =>
          val csesRhs = cses.map(_.rhs) //we can ignore pattern, and the guard is required to be pure
          val (csesRes, csesScope, csesFun) = csesRhs.map(toFunction).unzip3
          val (scrutRes, scrutScope, scrutFun) = toFunction(scrut)

          val modifiedVars: Seq[Variable] = csesFun.flatMap(_.keys).toSet.intersect(varsInScope).toSeq
          val res = ValDef.fresh("res", m.getType).setPos(m)
          val freshVars = modifiedVars.map(_.freshen)
          val matchType = tupleTypeWrap(res.tpe +: freshVars.map(_.tpe))

          val csesVals = csesRes.zip(csesFun).map {
            case (cRes, cFun) => tupleWrap(cRes +: modifiedVars.map(v => cFun.getOrElse(v, v)))
          }

          val newRhs = csesVals.zip(csesScope).map {
            case (cVal, cScope) => replaceFromSymbols(scrutFun, cScope(cVal), true)
          }

          val matchE = MatchExpr(scrutRes, cses.zip(newRhs).map {
            case (mc @ MatchCase(pat, guard, _), newRhs) =>
              //guard need to update ids (substitution of new names, and new fundef)
              //but wont have side effects
              MatchCase(pat, guard.map { g =>
                val (resGuard, scopeGuard, _) = toFunction(g)
                replaceFromSymbols(scrutFun, scopeGuard(resGuard))
              }, newRhs).copiedFrom(mc)
          }).copiedFrom(m)

          val scope = (body: Expr) => {
            val tupleVd = ValDef.fresh("t", matchType)
            scrutScope(
              Let(tupleVd, matchE,
                Let(res, tupleSelect(tupleVd.toVariable, 1, freshVars.nonEmpty),
                  freshVars.zipWithIndex.foldLeft(body)((b, p) =>
                    Let(p._1.toVal, tupleSelect(tupleVd.toVariable, p._2 + 2, true), b)
                  )
                )
              )
            )
          }

          (res.toVariable, scope, scrutFun ++ (modifiedVars zip freshVars))

        case wh @ While(cond, body, optInv) =>
          val id = FreshIdentifier(parent.id.name + "While")
          val tpe = FunctionType(Seq(), UnitType().copiedFrom(wh)).copiedFrom(wh)
{'fraction_non_alphanumeric': 0.11331958762886597, 'fraction_numerical': 0.0028041237113402063, 'mean_word_length': 2.480482204362801, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 49, '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': '5015868', 'n_tokens_mistral': 3828, 'n_tokens_neox': 3777, 'n_words': 957}