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

package stainless
package extraction

import scala.language.existentials

package object oo {

  object trees extends oo.Trees with ClassSymbols {
    case class Symbols(
      functions: Map[Identifier, FunDef],
      sorts: Map[Identifier, ADTSort],
      classes: Map[Identifier, ClassDef]
    ) extends ClassSymbols

    object printer extends Printer { val trees: oo.trees.type = oo.trees }
  }

  object methods extends MethodLifting {
    val s: trees.type = trees
    val t: trees.type = trees
  }

  object adts extends AdtSpecialization {
    val s: trees.type = trees
    val t: trees.type = trees
  }

  object refinements extends RefinementLifting {
    val s: trees.type = trees
    val t: trees.type = trees
  }

  object encoding extends CoqTypeEncoding {
    val s: trees.type = trees
    val t: trees.type = trees
  }

  val checker = inox.ast.SymbolTransformer(new CheckingTransformer {
    val s: trees.type = trees
    val t: holes.trees.type = holes.trees
  })

  val extractor = methods andThen adts andThen refinements andThen encoding andThen checker
}<commit_msg>Removed encoding phase, needs to be replaced by a phase that eliminates IsInstanceOf/AsInstanceOf<commit_after>/* Copyright 2009-2018 EPFL, Lausanne */

package stainless
package extraction

import scala.language.existentials

package object oo {

  object trees extends oo.Trees with ClassSymbols {
    case class Symbols(
      functions: Map[Identifier, FunDef],
      sorts: Map[Identifier, ADTSort],
      classes: Map[Identifier, ClassDef]
    ) extends ClassSymbols

    object printer extends Printer { val trees: oo.trees.type = oo.trees }
  }

  object methods extends MethodLifting {
    val s: trees.type = trees
    val t: trees.type = trees
  }

  object adts extends AdtSpecialization {
    val s: trees.type = trees
    val t: trees.type = trees
  }

  object refinements extends RefinementLifting {
    val s: trees.type = trees
    val t: trees.type = trees
  }

  object encoding extends CoqTypeEncoding {
    val s: trees.type = trees
    val t: trees.type = trees
  }

  val checker = inox.ast.SymbolTransformer(new CheckingTransformer {
    val s: trees.type = trees
    val t: holes.trees.type = holes.trees
  })

  val extractor = methods andThen adts andThen refinements /* andThen encoding */ andThen checker
}
{'fraction_non_alphanumeric': 0.07556675062972293, 'fraction_numerical': 0.006717044500419815, 'mean_word_length': 3.225177304964539, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, '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': '4820721', 'n_tokens_mistral': 746, 'n_tokens_neox': 699, 'n_words': 238}