diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 26fcab817fe63ef8d1e6e634cfa74e84ccedab19..e05adbf6c181c96ad69d4096cd866115b0edb6f8 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -21,7 +21,8 @@ object Main {
xlang.XlangAnalysisPhase,
synthesis.SynthesisPhase,
termination.TerminationPhase,
- verification.AnalysisPhase
+ verification.AnalysisPhase,
+ refactor.RefactorPhase
)
}
@@ -32,6 +33,7 @@ object Main {
lazy val topLevelOptions : Set[LeonOptionDef] = Set(
LeonFlagOptionDef ("termination", "--termination", "Check program termination"),
+ LeonFlagOptionDef ("refactor", "--refactor", "Refactoring/Repair"),
LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"),
LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"),
LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 (fairz3,enum,smt)"),
@@ -140,6 +142,8 @@ object Main {
for(opt <- leonOptions) opt match {
case LeonFlagOption("termination", value) =>
settings = settings.copy(termination = value)
+ case LeonFlagOption("refactor", value) =>
+ settings = settings.copy(refactor = value)
case LeonFlagOption("synthesis", value) =>
settings = settings.copy(synthesis = value)
case LeonFlagOption("xlang", value) =>
@@ -205,6 +209,7 @@ object Main {
import termination.TerminationPhase
import xlang.XlangAnalysisPhase
import verification.AnalysisPhase
+ import refactor.RefactorPhase
val pipeBegin : Pipeline[List[String],Program] =
ExtractionPhase andThen
@@ -213,6 +218,8 @@ object Main {
val pipeProcess: Pipeline[Program, Any] = {
if (settings.synthesis) {
SynthesisPhase
+ } else if (settings.refactor) {
+ RefactorPhase
} else if (settings.termination) {
TerminationPhase
} else if (settings.xlang) {
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 4ad409af285d8aaaebf72fd9d82254dcb8e94d93..31cf87ca4ecb8b93ee4a0da74377f27c8360ed3b 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -8,6 +8,7 @@ case class Settings(
val strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
val debugSections: Set[DebugSection] = Set(), // Enables debug message for the following sections
val termination: Boolean = false,
+ val refactor: Boolean = false,
val synthesis: Boolean = false,
val xlang: Boolean = false,
val verify: Boolean = true,
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 6aeda471b2cde381144e476b0313cf70254f3ff5..8dd01c3a9eaaa7c054be18ff2fb8853b98138ab0 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -32,4 +32,10 @@ object Constructors {
Tuple(Seq(ch))
}
}
+
+ def tupleWrap(es: Seq[Expr]): Expr = if (es.size > 1) {
+ Tuple(es)
+ } else {
+ es.head
+ }
}
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index c374d664a60e7cb644ec668d0d2dc90c40c6321a..1a3876714548db58912a028c489e70774137913f 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -78,6 +78,12 @@ object DefOps {
}
}
+ def funDefsFromMain(p: Program): Set[FunDef] = {
+ p.units.filter(_.isMainUnit).toSet.flatMap{ (u: UnitDef) =>
+ u.definedFunctions
+ }
+ }
+
def visibleFunDefsFromMain(p: Program): Set[FunDef] = {
p.units.filter(_.isMainUnit).toSet.flatMap{ (u: UnitDef) =>
visibleFunDefsFrom(u) ++ u.definedFunctions
@@ -188,13 +194,6 @@ object DefOps {
df <- descendDefs(startingPoint,path)
) yield df ) orElse {
- // Now starts the package nonsense
- def isPrefixOf[A](pre : List[A],l : List[A]) : Boolean = (pre,l) match {
- case (Nil, _) => true
- case (hp :: tp, hl :: tl) if hp == hl => isPrefixOf(tp,tl)
- case _ => false
- }
-
val program = inProgram(base)
val currentPack = inPackage(base)
val knownPacks = program.units map { _.pack }
@@ -209,11 +208,11 @@ object DefOps {
import scala.util.Try
val (packagePart, objectPart) = Try {
// Find the longest match, then re-attach the current package.
- val pack = subPacks filter { isPrefixOf(_,fullNameList) } maxBy(_.length)
+ val pack = subPacks filter { fullNameList.startsWith(_) } maxBy(_.length)
( currentPack ++ pack, fullNameList drop pack.length )
} orElse { Try {
// In this case, try to find a package that fits beginning from the root package
- val pack = knownPacks filter { isPrefixOf(_,fullNameList) } maxBy(_.length)
+ val pack = knownPacks filter { fullNameList.startsWith(_) } maxBy(_.length)
(pack, fullNameList drop pack.length)
}} getOrElse {
// No package matches
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index fd35346f36b2a3e16758bcf85509396feb09a400..a9e761bb0c717500d47f7243376ff7e77048541d 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -35,6 +35,15 @@ object TypeTreeOps {
}
} else {
(tpe, stpe) match {
+ case (t, tp1: TypeParameter) =>
+ if (freeParams contains tp1) {
+ Some(Map(tp1 -> t))
+ } else if (tp1 == t) {
+ Some(Map())
+ } else {
+ None
+ }
+
case (tp1: TypeParameter, t) =>
if (freeParams contains tp1) {
Some(Map(tp1 -> t))
diff --git a/src/main/scala/leon/refactor/RefactorPhase.scala b/src/main/scala/leon/refactor/RefactorPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..77e12c2d41f94a5a2bf63c263e3f98cb3694b0bc
--- /dev/null
+++ b/src/main/scala/leon/refactor/RefactorPhase.scala
@@ -0,0 +1,50 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package refactor
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Constructors._
+import purescala.DefOps._
+
+object RefactorPhase extends LeonPhase[Program, Program] {
+ val name = "Refactor"
+ val description = "Refactoring/Repairing"
+
+ implicit val debugSection = utils.DebugSectionRefactor
+
+ override val definedOptions : Set[LeonOptionDef] = Set(
+ LeonValueOptionDef("functions", "--functions=f1:f2", "Refactor functions f1,f2,...")
+ )
+
+ def run(ctx: LeonContext)(program: Program): Program = {
+ var refactorFuns: Option[Seq[String]] = None
+
+ val reporter = ctx.reporter
+
+ for(opt <- ctx.options) opt match {
+ case LeonValueOption("functions", ListValue(fs)) =>
+ refactorFuns = Some(fs)
+ case _ =>
+ }
+
+
+ val fdFilter = {
+ import OptionsHelpers._
+
+ filterInclusive(refactorFuns.map(fdMatcher), None)
+ }
+
+ val toRefactor = funDefsFromMain(program).toList.sortWith((fd1, fd2) => fd1.getPos < fd2.getPos).filter(fdFilter)
+
+ for (fd <- toRefactor) {
+ new Repairman(ctx, program, fd).repair()
+ }
+
+ program
+ }
+}
diff --git a/src/main/scala/leon/refactor/Repairman.scala b/src/main/scala/leon/refactor/Repairman.scala
new file mode 100644
index 0000000000000000000000000000000000000000..287c01db46daedc4e7859c6a975b8a4891aeacc7
--- /dev/null
+++ b/src/main/scala/leon/refactor/Repairman.scala
@@ -0,0 +1,205 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package refactor
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Constructors._
+import purescala.ScalaPrinter
+import evaluators._
+import datagen._
+import solvers._
+import utils._
+import solvers.z3._
+import codegen._
+import verification._
+import synthesis._
+
+class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
+ val reporter = ctx.reporter
+
+ var testBank = List[Example]()
+
+ var solutions: List[(Solution, Expr, List[FunDef])] = Nil
+
+ def repair(): Unit = {
+ // Gather in/out tests
+ val pre = fd.precondition.getOrElse(BooleanLiteral(true))
+ val args = fd.params.map(_.id)
+ val argsWrapped = tupleWrap(args.map(_.toVariable))
+
+ val out = fd.postcondition.map(_._1).getOrElse(FreshIdentifier("res", true).setType(fd.returnType))
+
+ val tfd = program.library.passes.get.typed(Seq(argsWrapped.getType, out.getType))
+
+ val inouts = testBank;
+
+ val testsExpr = FiniteMap(inouts.collect {
+ case InOutExample(ins, outs) =>
+ tupleWrap(ins) -> tupleWrap(outs)
+ }.toList).setType(MapType(argsWrapped.getType, out.getType))
+
+ val passes = FunctionInvocation(tfd, Seq(argsWrapped, out.toVariable, testsExpr))
+
+ val spec = And(fd.postcondition.map(_._2).getOrElse(BooleanLiteral(true)), passes)
+
+ // Synthesis from the ground up
+ val p = Problem(fd.params.map(_.id).toList, pre, spec, List(out))
+
+ val soptions = SynthesisPhase.processOptions(ctx);
+
+ val synthesizer = new Synthesizer(ctx, fd, program, p, soptions)
+
+ synthesizer.synthesize() match {
+ case (search, sols) =>
+ for (sol <- sols) {
+ val expr = sol.toSimplifiedExpr(ctx, program)
+
+ val (npr, fds) = synthesizer.solutionToProgram(sol)
+ solutions ::= (sol, expr, fds)
+
+ if (!sol.isTrusted) {
+
+ val timeoutMs = 3000l
+ val solverf = SolverFactory(() => (new FairZ3Solver(ctx, npr) with TimeoutSolver).setTimeout(timeoutMs))
+ val vctx = VerificationContext(ctx, npr, solverf, reporter)
+ val nfd = fds.head
+ val vcs = AnalysisPhase.generateVerificationConditions(vctx, Some(List(nfd.id.name)))
+
+ AnalysisPhase.checkVerificationConditions(vctx, vcs)
+
+ var unknown = false;
+ var ces = List[Seq[Expr]]()
+
+ for (vc <- vcs.getOrElse(nfd, List())) {
+ if (vc.value == Some(false)) {
+ vc.counterExample match {
+ case Some(m) =>
+ ces = nfd.params.map(vd => m(vd.id)) :: ces;
+
+ case _ =>
+ }
+ } else if (vc.value == None) {
+ unknown = true;
+ }
+ }
+
+
+ if (ces.isEmpty) {
+ if (!unknown) {
+ reporter.info("ZZUCCESS!")
+ } else {
+ reporter.info("ZZUCCESS (maybe)!")
+ }
+ } else {
+ reporter.info("Failed :(, but I learned: "+ces.map(_.mkString(",")).mkString(" | "))
+ testBank ++= ces.map(InExample(_))
+ }
+ } else {
+ reporter.info("ZZUCCESS!")
+ }
+ }
+
+
+ if (solutions.isEmpty) {
+ reporter.info("Trey aagggain")
+ repair()
+ } else {
+
+ reporter.info(ASCIIHelpers.title("Solutions"))
+ for (((sol, expr, fds), i) <- solutions.zipWithIndex) {
+ reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+":"))
+ reporter.info(ScalaPrinter(expr));
+ }
+
+ if (solutions.size > 1) {
+ reporter.info(ASCIIHelpers.title("Disambiguating..."))
+ disambiguate(p, solutions(0)._1, solutions(1)._1) match {
+ case Some((o1, o2)) =>
+ reporter.info("Solutions differ on "+o1.ins.mkString(", "))
+ reporter.info("solution A produces: "+o1.outs.mkString(", "))
+ reporter.info("solution B produces: "+o2.outs.mkString(", "))
+
+ case None =>
+ reporter.info("Solutions appear equivalent..")
+ }
+ }
+ }
+
+ case _ =>
+ reporter.error("I failed you :(")
+ }
+
+ }
+
+ def disambiguate(p: Problem, sol1: Solution, sol2: Solution): Option[(InOutExample, InOutExample)] = {
+ val s1 = sol1.toSimplifiedExpr(ctx, program)
+ val s2 = sol2.toSimplifiedExpr(ctx, program)
+
+ val e = new DefaultEvaluator(ctx, program);
+
+ def unwrap(e: Expr) = if (p.xs.size > 1) {
+ val Tuple(es) = e
+ es
+ } else {
+ Seq(e)
+ }
+
+ if (s1 == s2) {
+ None
+ } else {
+ val diff = And(p.pc, Not(Equals(s1, s2)))
+ val solver = (new FairZ3Solver(ctx, program) with TimeoutSolver).setTimeout(1000)
+
+ solver.assertCnstr(diff)
+ solver.check match {
+ case Some(true) =>
+ val m = solver.getModel
+ val inputs = p.as.map(id => m.getOrElse(id, simplestValue(id.getType)))
+ val inputsMap = (p.as zip inputs).toMap
+
+ (e.eval(s1, inputsMap), e.eval(s2, inputsMap)) match {
+ case (EvaluationResults.Successful(r1), EvaluationResults.Successful(r2)) =>
+ Some((InOutExample(inputs, unwrap(r1)), InOutExample(inputs, unwrap(r2))))
+ case _ =>
+ None
+ }
+ case Some(false) =>
+ None
+ case _ =>
+ // considered as equivalent
+ None
+ }
+ }
+ }
+
+ def classifier(ok: Seq[Example], notok: Seq[Example]): Option[Expr] = {
+ // Obtain expr that returns partitions all examples into ok/notok
+
+ None
+ }
+
+ def discoverTests() = {
+ val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams(checkContracts = true))
+ val tests = new NaiveDataGen(ctx, program, evaluator)
+
+ val pre = fd.precondition.getOrElse(BooleanLiteral(true))
+ val inputs = tests.generateFor(fd.params.map(_.id), pre, 30, 10000).toList
+
+ testBank ++= inputs.map { i =>
+ evaluator.eval(FunctionInvocation(fd.typed(fd.tparams.map(_.tp)), i)) match {
+ case EvaluationResults.Successful(res) =>
+ new InOutExample(i, List(res))
+
+ case _ =>
+ new InExample(i)
+ }
+ }
+ }
+
+ discoverTests()
+}
diff --git a/src/main/scala/leon/synthesis/InOutExample.scala b/src/main/scala/leon/synthesis/InOutExample.scala
index 8978e38ae002faf74ffc55f5528f499340c7cc0e..0e2e4faa84d51d59885b59814909428bcc30c57b 100644
--- a/src/main/scala/leon/synthesis/InOutExample.scala
+++ b/src/main/scala/leon/synthesis/InOutExample.scala
@@ -5,5 +5,6 @@ package synthesis
import purescala.Trees.Expr
-class InExample(val ins: Seq[Expr])
-class InOutExample(is: Seq[Expr], val outs: Seq[Expr]) extends InExample(is)
+class Example(val ins: Seq[Expr])
+case class InOutExample(is: Seq[Expr], val outs: Seq[Expr]) extends Example(is)
+case class InExample(is: Seq[Expr]) extends Example(is)
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 82b02486f71a5ec772327b3caf909ef8f544fb6c..cc21e87a9798a32d6a997b5efc10832317a66e55 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -12,7 +12,7 @@ import leon.purescala.Common._
case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifier]) {
override def toString = "⟦ "+as.mkString(";")+", "+(if (pc != BooleanLiteral(true)) pc+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
- def getTests(sctx: SynthesisContext): Seq[InExample] = {
+ def getTests(sctx: SynthesisContext): Seq[Example] = {
import purescala.Extractors._
import evaluators._
@@ -20,7 +20,7 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
val ev = new DefaultEvaluator(sctx.context, sctx.program)
- def isValidExample(ex: InExample): Boolean = {
+ def isValidExample(ex: Example): Boolean = {
val (mapping, cond) = ex match {
case io: InOutExample =>
(Map((as zip io.ins) ++ (xs zip io.outs): _*), And(pc, phi))
@@ -142,9 +142,9 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
val examples = consolidated.toSeq.flatMap { t =>
val ids = t.keySet
if ((ids & allIds) == allIds) {
- Some(new InOutExample(as.map(t), xs.map(t)))
+ Some(InOutExample(as.map(t), xs.map(t)))
} else if ((ids & insIds) == insIds) {
- Some(new InExample(as.map(t)))
+ Some(InExample(as.map(t)))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 5598f59b83f3e30436c75771c4785e01b824f339..0e2bff86f85aa2d69274233d79973c51b888f436 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -96,7 +96,7 @@ class Synthesizer(val context : LeonContext,
}
// Returns the new program and the new functions generated for this
- def solutionToProgram(sol: Solution): (Program, Set[FunDef]) = {
+ def solutionToProgram(sol: Solution): (Program, List[FunDef]) = {
import purescala.TypeTrees.TupleType
import purescala.Definitions.ValDef
@@ -109,12 +109,12 @@ class Synthesizer(val context : LeonContext,
Variable(id) -> TupleSelect(res, i+1)
}.toMap
- val fd = new FunDef(FreshIdentifier("finalTerm", true), Nil, ret, problem.as.map(id => ValDef(id, id.getType)), DefType.MethodDef)
+ val fd = new FunDef(FreshIdentifier(functionContext.id.name+"_final", true), Nil, ret, problem.as.map(id => ValDef(id, id.getType)), DefType.MethodDef)
fd.precondition = Some(And(problem.pc, sol.pre))
fd.postcondition = Some((res.id, replace(mapPost, problem.phi)))
fd.body = Some(sol.term)
- val newDefs = sol.defs + fd
+ val newDefs = fd +: sol.defs.toList
val npr = program.copy(units = program.units map { u =>
u.copy(modules = ModuleDef(FreshIdentifier("synthesis"), newDefs.toSeq, false) +: u.modules )
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 51e671cf57ef7a38634ca348fcb54086fdda5003..ad57f6edfdd6771a396392ff3394a3e61f563f5a 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -97,6 +97,10 @@ case object CEGIS extends Rule("CEGIS") {
alts.toList
}
+ case _: TypeParameter =>
+ { () =>
+ Nil
+ }
case _ =>
sctx.reporter.error("Can't construct generator. Unsupported type: "+t+"["+t.getClass+"]");
{ () => Nil }
diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala
index 15ac89ea9911845b21018d2895708664d2fe9f7c..0b16539aa77b1221a1a73cf31ca3d96dd71e94b7 100644
--- a/src/main/scala/leon/synthesis/rules/Tegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegis.scala
@@ -12,6 +12,7 @@ import purescala.Common._
import purescala.Definitions._
import purescala.TypeTrees._
import purescala.TreeOps._
+import purescala.DefOps._
import purescala.TypeTreeOps._
import purescala.Extractors._
import purescala.ScalaPrinter
@@ -87,7 +88,7 @@ case object TEGIS extends Rule("TEGIS") {
}
def getFcallGenerators(t: TypeTree): Seq[Generator[TypeTree, Expr]] = {
- def isCandidate(fd: FunDef): Option[TypedFunDef] = {
+ def getCandidates(fd: FunDef): Seq[TypedFunDef] = {
// Prevents recursive calls
val cfd = sctx.functionContext
@@ -107,16 +108,50 @@ case object TEGIS extends Rule("TEGIS") {
val free = fd.tparams.map(_.tp)
canBeSubtypeOf(fd.returnType, free, t) match {
case Some(tpsMap) =>
- Some(fd.typed(free.map(tp => tpsMap.getOrElse(tp, tp))))
+ val tfd = fd.typed(free.map(tp => tpsMap.getOrElse(tp, tp)))
+
+ if (tpsMap.size < free.size) {
+ /* Some type params remain free, we want to assign them:
+ *
+ * List[T] => Int, for instance, will be found when
+ * requesting Int, but we need to assign T to viable
+ * types. For that we use problem inputs as heuristic,
+ * and look for instantiations of T such that input <?:
+ * List[T].
+ */
+ p.as.map(_.getType).distinct.flatMap { (atpe: TypeTree) =>
+ var finalFree = free.toSet -- tpsMap.keySet
+ var finalMap = tpsMap
+
+ for (ptpe <- tfd.params.map(_.tpe).distinct) {
+ canBeSubtypeOf(atpe, finalFree.toSeq, ptpe) match {
+ case Some(ntpsMap) =>
+ finalFree --= ntpsMap.keySet
+ finalMap ++= ntpsMap
+ case _ =>
+ }
+ }
+
+ if (finalFree.isEmpty) {
+ List(fd.typed(free.map(tp => finalMap.getOrElse(tp, tp))))
+ } else {
+ Nil
+ }
+ }
+ } else {
+ /* All type parameters that used to be free are assigned
+ */
+ List(tfd)
+ }
case None =>
- None
+ Nil
}
} else {
- None
+ Nil
}
}
- val funcs = sctx.program.definedFunctions.flatMap(isCandidate)
+ val funcs = visibleFunDefsFromMain(sctx.program).toSeq.flatMap(getCandidates)
funcs.map{ tfd =>
Generator[TypeTree, Expr](tfd.params.map(_.tpe), { sub => FunctionInvocation(tfd, sub) })
@@ -124,7 +159,12 @@ case object TEGIS extends Rule("TEGIS") {
}
def getGenerators(t: TypeTree): Seq[Generator[TypeTree, Expr]] = {
- getBaseGenerators(t) ++ getInputGenerators(t) ++ getFcallGenerators(t)
+ val res = getBaseGenerators(t) ++ getInputGenerators(t) ++ getFcallGenerators(t)
+ //for (g <- res) {
+ // val inputs = g.subTrees.zipWithIndex.map{ case (t, i) => Variable(FreshIdentifier(t.toString).setType(t)) }
+ // println(f"$t%20s := ${g.builder(inputs)}")
+ //}
+ res
}
val enum = new MemoizedEnumerator[TypeTree, Expr](getGenerators)
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index adcfecf25140edeb2cae1bda2db8fae2d259f4b3..0e4d30a4e538e431cb8dc4315defd8c9f459e11e 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -18,6 +18,7 @@ case object DebugSectionTrees extends DebugSection("trees", 1 << 6
case object DebugSectionPositions extends DebugSection("positions", 1 << 7)
case object DebugSectionDataGen extends DebugSection("datagen", 1 << 8)
case object DebugSectionEvaluation extends DebugSection("eval", 1 << 9)
+case object DebugSectionRefactor extends DebugSection("refactor", 1 << 10)
object DebugSections {
val all = Set[DebugSection](
@@ -30,6 +31,7 @@ object DebugSections {
DebugSectionTrees,
DebugSectionPositions,
DebugSectionDataGen,
- DebugSectionEvaluation
+ DebugSectionEvaluation,
+ DebugSectionRefactor
)
}
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index 7c590125952fba53e8cc6a867d0d4298bf53a066..4899368aa217eb0e7f8c34372d9a8ef471cc6838 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -17,6 +17,10 @@ case class Library(pgm: Program) {
case fd: FunDef => fd
}
+ lazy val passes = lookup("leon.lang.passes").collect {
+ case fd: FunDef => fd
+ }
+
def lookup(name: String): Option[Definition] = {
searchByFullName(name, pgm)
}