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

package stainless
package ast

trait TreeDeconstructor extends inox.ast.TreeDeconstructor {
  protected val s: Trees
  protected val t: Trees

  /** Rebuild a pattern from the given set of identifiers, variables, expressions, types and subpatterns */
  protected type PatternBuilder = (Seq[Identifier], Seq[t.Variable], Seq[t.Expr], Seq[t.Type], Seq[t.Pattern]) => t.Pattern

  /** Extracted subtrees from a pattern as well as a "builder" */
  protected type DeconstructedPattern = (Seq[Identifier], Seq[s.Variable], Seq[s.Expr], Seq[s.Type], Seq[s.Pattern], PatternBuilder)

  def deconstruct(pattern: s.Pattern): DeconstructedPattern = pattern match {
    case s.WildcardPattern(binder) =>
      (Seq(), binder.map(_.toVariable).toSeq, Seq(), Seq(), Seq(), (_, vs, _, _, _) => {
        t.WildcardPattern(vs.headOption.map(_.toVal))
      })
    case s.ADTPattern(binder, id, tps, subs) =>
      (Seq(id), binder.map(_.toVariable).toSeq, Seq(), tps, subs, (ids, vs, _, tps, pats) => {
        t.ADTPattern(vs.headOption.map(_.toVal), ids.head, tps, pats)
      })
    case s.TuplePattern(binder, subs) =>
      (Seq(), binder.map(_.toVariable).toSeq, Seq(), Seq(), subs, (_, vs, _, _, pats) => {
        t.TuplePattern(vs.headOption.map(_.toVal), pats)
      })
    case s.LiteralPattern(binder, lit) =>
      (Seq(), binder.map(_.toVariable).toSeq, Seq(lit), Seq(), Seq(), (_, vs, es, _, _) => {
        t.LiteralPattern(vs.headOption.map(_.toVal), es.head.asInstanceOf[t.Literal[_]])
      })
    case s.UnapplyPattern(binder, recs, id, tps, subs) =>
      (Seq(id), binder.map(_.toVariable).toSeq, recs, tps, subs, (ids, vs, es, tps, pats) => {
        t.UnapplyPattern(vs.headOption.map(_.toVal), es, ids.head, tps, pats)
      })
  }

  /** Rebuild a match case from the given set of identifiers, variables, expressions and types */
  protected type CasesBuilder = (Seq[Identifier], Seq[t.Variable], Seq[t.Expr], Seq[t.Type]) => Seq[t.MatchCase]

  /** Extracted subtrees from a match case as well as a "builder" */
  protected type DeconstructedCases = (Seq[Identifier], Seq[s.Variable], Seq[s.Expr], Seq[s.Type], CasesBuilder)

  protected def deconstructCases(cases: Seq[s.MatchCase]): DeconstructedCases = {
    def rec(p: s.Pattern): (
      Seq[Identifier], Seq[s.Variable], Seq[s.Expr], Seq[s.Type],
      (Seq[Identifier], Seq[t.Variable], Seq[t.Expr], Seq[t.Type]) => t.Pattern
    ) = {
      val (ids, vs, es, tps, pats, reconsP) = deconstruct(p)
      val prec = pats.map(pat => (pat, rec(pat)))
      (
        ids ++ prec.flatMap(_._2._1),
        vs ++ prec.flatMap(_._2._2),
        es ++ prec.flatMap(_._2._3),
        tps ++ prec.flatMap(_._2._4),
        (nids, nvs, nes, ntps) => {
          val (outerIds, innerIds) = nids.splitAt(ids.size)
          val (outerVs, innerVs) = nvs.splitAt(vs.size)
          val (outerEs, innerEs) = nes.splitAt(es.size)
          val (outerTps, innerTps) = ntps.splitAt(tps.size)

          var rids = innerIds
          var rvs = innerVs
          var res = innerEs
          var rtps = innerTps
          val newPats = for ((pat, (ids, vs, es, tps, reconsPat)) <- prec) yield {
            val (currIds, nextIds) = rids.splitAt(ids.size)
            rids = nextIds

            val (currVs, nextVs) = rvs.splitAt(vs.size)
            rvs = nextVs

            val (currEs, nextEs) = res.splitAt(es.size)
            res = nextEs

            val (currTps, nextTps) = rtps.splitAt(tps.size)
            rtps = nextTps

            reconsPat(currIds, currVs, currEs, currTps).setPos(pat)
          }

          reconsP(outerIds, outerVs, outerEs, outerTps, newPats).setPos(p)
        }
      )
    }

    val recCases = for (caze <- cases) yield {
      val (pids, pvs, pes, ptps, precons) = rec(caze.pattern)
      (caze, caze.optGuard.isDefined, pids, pvs, caze.optGuard.toSeq ++ (caze.rhs +: pes), ptps, precons)
    }

    (
      recCases.flatMap(_._3),
      recCases.flatMap(_._4),
      recCases.flatMap(_._5),
      recCases.flatMap(_._6),
      (ids, vs, es, tps) => {
        var rids = ids
        var rvs = vs
        var res = es
        var rtps = tps
        for ((caze, hasGuard, ids, vs, es, tps, reconsCaze) <- recCases) yield {
          val (currIds, nextIds) = rids.splitAt(ids.size)
          rids = nextIds

          val (currVs, nextVs) = rvs.splitAt(vs.size)
          rvs = nextVs

          val (currEs, nextEs) = res.splitAt(es.size)
          res = nextEs

          val (currTps, nextTps) = rtps.splitAt(tps.size)
          rtps = nextTps

          if (hasGuard) {
            val guard +: rhs +: pes = currEs
            t.MatchCase(reconsCaze(currIds, currVs, pes, currTps).setPos(caze), Some(guard), rhs).setPos(caze)
          } else {
            val rhs +: pes = currEs
            t.MatchCase(reconsCaze(currIds, currVs, pes, currTps).setPos(caze), None, rhs).setPos(caze)
          }
        }
      }
    )
  }

  override def deconstruct(expr: s.Expr): Deconstructed[t.Expr] = expr match {
    case s.NoTree(tpe) =>
      (Seq(), Seq(), Seq(), Seq(tpe), Seq(), (_, _, _, tps, _) => t.NoTree(tps.head))
    case s.Error(tpe, desc) =>
      (Seq(), Seq(), Seq(), Seq(tpe), Seq(), (_, _, _, tps, _) => t.Error(tps.head, desc))<commit_msg>Fix confusion between case and pattern positions<commit_after>/* Copyright 2009-2018 EPFL, Lausanne */

package stainless
package ast

trait TreeDeconstructor extends inox.ast.TreeDeconstructor {
  protected val s: Trees
  protected val t: Trees

  /** Rebuild a pattern from the given set of identifiers, variables, expressions, types and subpatterns */
  protected type PatternBuilder = (Seq[Identifier], Seq[t.Variable], Seq[t.Expr], Seq[t.Type], Seq[t.Pattern]) => t.Pattern

  /** Extracted subtrees from a pattern as well as a "builder" */
  protected type DeconstructedPattern = (Seq[Identifier], Seq[s.Variable], Seq[s.Expr], Seq[s.Type], Seq[s.Pattern], PatternBuilder)

  def deconstruct(pattern: s.Pattern): DeconstructedPattern = pattern match {
    case s.WildcardPattern(binder) =>
      (Seq(), binder.map(_.toVariable).toSeq, Seq(), Seq(), Seq(), (_, vs, _, _, _) => {
        t.WildcardPattern(vs.headOption.map(_.toVal))
      })
    case s.ADTPattern(binder, id, tps, subs) =>
      (Seq(id), binder.map(_.toVariable).toSeq, Seq(), tps, subs, (ids, vs, _, tps, pats) => {
        t.ADTPattern(vs.headOption.map(_.toVal), ids.head, tps, pats)
      })
    case s.TuplePattern(binder, subs) =>
      (Seq(), binder.map(_.toVariable).toSeq, Seq(), Seq(), subs, (_, vs, _, _, pats) => {
        t.TuplePattern(vs.headOption.map(_.toVal), pats)
      })
    case s.LiteralPattern(binder, lit) =>
      (Seq(), binder.map(_.toVariable).toSeq, Seq(lit), Seq(), Seq(), (_, vs, es, _, _) => {
        t.LiteralPattern(vs.headOption.map(_.toVal), es.head.asInstanceOf[t.Literal[_]])
      })
    case s.UnapplyPattern(binder, recs, id, tps, subs) =>
      (Seq(id), binder.map(_.toVariable).toSeq, recs, tps, subs, (ids, vs, es, tps, pats) => {
        t.UnapplyPattern(vs.headOption.map(_.toVal), es, ids.head, tps, pats)
      })
  }

  /** Rebuild a match case from the given set of identifiers, variables, expressions and types */
  protected type CasesBuilder = (Seq[Identifier], Seq[t.Variable], Seq[t.Expr], Seq[t.Type]) => Seq[t.MatchCase]

  /** Extracted subtrees from a match case as well as a "builder" */
  protected type DeconstructedCases = (Seq[Identifier], Seq[s.Variable], Seq[s.Expr], Seq[s.Type], CasesBuilder)

  protected def deconstructCases(cases: Seq[s.MatchCase]): DeconstructedCases = {
    def rec(p: s.Pattern): (
      Seq[Identifier], Seq[s.Variable], Seq[s.Expr], Seq[s.Type],
      (Seq[Identifier], Seq[t.Variable], Seq[t.Expr], Seq[t.Type]) => t.Pattern
    ) = {
      val (ids, vs, es, tps, pats, reconsP) = deconstruct(p)
      val prec = pats.map(pat => (pat, rec(pat)))
      (
        ids ++ prec.flatMap(_._2._1),
        vs ++ prec.flatMap(_._2._2),
        es ++ prec.flatMap(_._2._3),
        tps ++ prec.flatMap(_._2._4),
        (nids, nvs, nes, ntps) => {
          val (outerIds, innerIds) = nids.splitAt(ids.size)
          val (outerVs, innerVs) = nvs.splitAt(vs.size)
          val (outerEs, innerEs) = nes.splitAt(es.size)
          val (outerTps, innerTps) = ntps.splitAt(tps.size)

          var rids = innerIds
          var rvs = innerVs
          var res = innerEs
          var rtps = innerTps
          val newPats = for ((pat, (ids, vs, es, tps, reconsPat)) <- prec) yield {
            val (currIds, nextIds) = rids.splitAt(ids.size)
            rids = nextIds

            val (currVs, nextVs) = rvs.splitAt(vs.size)
            rvs = nextVs

            val (currEs, nextEs) = res.splitAt(es.size)
            res = nextEs

            val (currTps, nextTps) = rtps.splitAt(tps.size)
            rtps = nextTps

            reconsPat(currIds, currVs, currEs, currTps).setPos(pat)
          }

          reconsP(outerIds, outerVs, outerEs, outerTps, newPats).setPos(p)
        }
      )
    }

    val recCases = for (caze <- cases) yield {
      val (pids, pvs, pes, ptps, precons) = rec(caze.pattern)
      (
        caze.getPos,
        caze.pattern.getPos,
        caze.optGuard.isDefined,
        pids,
        pvs,
        caze.optGuard.toSeq ++ (caze.rhs +: pes),
        ptps,
        precons
      )
    }

    (
      recCases.flatMap(_._4),
      recCases.flatMap(_._5),
      recCases.flatMap(_._6),
      recCases.flatMap(_._7),
      (ids, vs, es, tps) => {
        var rids = ids
        var rvs = vs
        var res = es
        var rtps = tps
        for ((cazePos, patternPos, hasGuard, ids, vs, es, tps, precons) <- recCases) yield {
          val (currIds, nextIds) = rids.splitAt(ids.size)
          rids = nextIds

          val (currVs, nextVs) = rvs.splitAt(vs.size)
          rvs = nextVs

          val (currEs, nextEs) = res.splitAt(es.size)
          res = nextEs

          val (currTps, nextTps) = rtps.splitAt(tps.size)
          rtps = nextTps

          if (hasGuard) {
            val guard +: rhs +: pes = currEs
            t.MatchCase(precons(currIds, currVs, pes, currTps).setPos(patternPos), Some(guard), rhs).setPos(cazePos)
          } else {
            val rhs +: pes = currEs
            t.MatchCase(precons(currIds, currVs, pes, currTps).setPos(patternPos), None, rhs).setPos(cazePos)
          }
        }
      }
    )
  }

  override def deconstruct(expr: s.Expr): Deconstructed[t.Expr] = expr match {
    case s.NoTree(tpe) =>
      (Seq(), Seq(), Seq(), Seq(tpe), Seq(), (_, _, _, tps, _) => t.NoTree(tps.head))
    case s.Error(tpe, desc) =>
      (Seq(), Seq(), Seq(), Seq(tpe), Seq(), (_, _, _, tps, _) => t.Error(tps.head, desc))
{'fraction_non_alphanumeric': 0.15654357734164265, 'fraction_numerical': 0.003720584131708678, 'mean_word_length': 2.5045632333767927, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 43, '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': '6198305', 'n_tokens_mistral': 3958, 'n_tokens_neox': 3853, 'n_words': 853}