Skip to content
Snippets Groups Projects
  • Etienne Kneuss's avatar
    8f2438cc
    All-seeing synthesis with Oracles, library reorganisation · 8f2438cc
    Etienne Kneuss authored
    - NormalizationRule becomes priorities, so that we can have multiple
      distinct layers
    
    - Use the @library annotation, move synthesis stuff to synthesis,
      Oracles.
    
    - Make sure tests use PreprocessingPhase and import synthesis when
      adequate
    
    - Extract proper package objects fix patternRecons and simplifiers
    
    - Reorganize library:
      - leon.{choose,???} -> leon.lang.synthesis
      - leon.{waypoint,epsilon} -> leon.lang.xlang
    8f2438cc
    History
    All-seeing synthesis with Oracles, library reorganisation
    Etienne Kneuss authored
    - NormalizationRule becomes priorities, so that we can have multiple
      distinct layers
    
    - Use the @library annotation, move synthesis stuff to synthesis,
      Oracles.
    
    - Make sure tests use PreprocessingPhase and import synthesis when
      adequate
    
    - Extract proper package objects fix patternRecons and simplifiers
    
    - Reorganize library:
      - leon.{choose,???} -> leon.lang.synthesis
      - leon.{waypoint,epsilon} -> leon.lang.xlang
OracleTraverser.scala 736 B
/* Copyright 2009-2014 EPFL, Lausanne */

package leon
package utils

import purescala.Trees._
import purescala.TypeTrees._
import purescala.Definitions._
import utils._

case class OracleTraverser(oracle: Expr, tpe: TypeTree, program: Program) {
  private def call(name: String) = {
    program.definedFunctions.find(_.id.name == "Oracle."+name) match {
      case Some(fd) =>
        FunctionInvocation(fd.typed(List(tpe)), List(oracle))
      case None =>
        sys.error("Unable to find Oracle."+name)
    }
  }

  def value: Expr = {
    call("head")
  }

  def left: OracleTraverser = {
    OracleTraverser(call("left"), tpe, program)
  }

  def right: OracleTraverser = {
    OracleTraverser(call("right"), tpe, program)
  }
}