diff --git a/library/lang/synthesis/package.scala b/library/lang/synthesis/package.scala
index 540054899b37dc540f0c359f51fe6e32dc553c82..fe87f4eb0bbe514e8d9a6be97b8b29f2278a686e 100644
--- a/library/lang/synthesis/package.scala
+++ b/library/lang/synthesis/package.scala
@@ -4,6 +4,9 @@ package leon.lang
import leon.annotation._
+import scala.language.implicitConversions
+import scala.annotation.implicitNotFound
+
package object synthesis {
@ignore
private def noImpl = throw new RuntimeException("Implementation not supported")
@@ -19,15 +22,16 @@ package object synthesis {
@ignore
def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean): (A, B, C, D, E) = noImpl
- @library
- def ???[T](implicit o: Oracle[T]): T = o.head
+ @ignore
+ def ???[T]: T = noImpl
- @library
- def ?[T](e1: T)(implicit o1: Oracle[Boolean], o2: Oracle[T]): T = if(???[Boolean](o1)) e1 else ???[T](o2)
+ @ignore
+ def ?[T](e1: T): T = if(???[Boolean]) e1 else ???[T]
@ignore
- def ?[T](e1: T, es: T*)(implicit o: Oracle[Boolean]): T = noImpl
+ def ?[T](e1: T, es: T*): T = noImpl
@ignore
def withOracle[A, R](body: Oracle[A] => R): R = noImpl
+
}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index f387182d8257e30a433db9aa3c314054b9498202..e444d225de8427ebbce9890d030274a2879a96ec 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -278,11 +278,11 @@ trait ASTExtractors {
}
object ExHoleExpression {
- def unapply(tree: Tree) : Option[(Tree, List[Tree], List[Tree])] = tree match {
- case a @ Apply(Apply(TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark"), List(tpt)), args1), args2) =>
- Some((tpt, args1, args2))
- case a @ Apply(TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark$qmark$qmark"), List(tpt)), List(o)) =>
- Some((tpt, Nil, List(o)))
+ def unapply(tree: Tree) : Option[(Tree, List[Tree])] = tree match {
+ case a @ Apply(TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark"), List(tpt)), args1) =>
+ Some((tpt, args1))
+ case TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark$qmark$qmark"), List(tpt)) =>
+ Some((tpt, Nil))
case _ => None
}
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9826e01a013efb4b7b495303f7df115b606da4fa..51338cb30628baaee0f5b9f03873deb818fd3b22 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -964,38 +964,10 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(tr, "Unidentified variable "+sym+" "+sym.id+".")
}
- case hole @ ExHoleExpression(tpt, exprs, os) =>
+ case hole @ ExHoleExpression(tpt, exprs) =>
val leonExprs = exprs.map(extractTree)
- val leonOracles = os.map(extractTree)
- def rightOf(o: LeonExpr): LeonExpr = {
- val Some((cl, fd)) = libraryMethod("Oracle", "right")
- MethodInvocation(o, cl, fd.typed(Nil), Nil)
- }
-
- def valueOf(o: LeonExpr): LeonExpr = {
- val Some((cl, fd)) = libraryMethod("Oracle", "head")
- MethodInvocation(o, cl, fd.typed(Nil), Nil)
- }
-
-
- leonExprs match {
- case Nil =>
- valueOf(leonOracles(0))
-
- case List(e) =>
- IfExpr(valueOf(leonOracles(0)), e, valueOf(leonOracles(1)))
-
- case exs =>
- val l = exs.last
- var o = leonOracles(0)
-
- exs.init.foldRight(l)({ (e: LeonExpr, r: LeonExpr) =>
- val res = IfExpr(valueOf(leonOracles(0)), e, r)
- o = rightOf(o)
- res
- })
- }
+ Hole(extractType(tpt), exprs.map(extractTree))
case ops @ ExWithOracleExpression(oracles, body) =>
val newOracles = oracles map { case (tpt, sym) =>
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 7873fbaa138fb09dafc4d4bd3ba27b1f056896a4..0973edddbcf4ccc981309c841f7c3f447c1b2001 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -174,6 +174,13 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
| $pred
|}"""
+ case h @ Hole(tpe, es) =>
+ if (es.isEmpty) {
+ p"""|???[$tpe]"""
+ } else {
+ p"""|?($es)"""
+ }
+
case CaseClass(cct, args) =>
if (cct.classDef.isCaseObject) {
p"$cct"
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index fd0b1f4d0cf8ccec5dc2cace3c9ffa6ba66a3b84..387b085f18b4b8b0d66a58b450667214c6c51422 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -64,6 +64,13 @@ object Trees {
}
}
+ case class Hole(fixedType: TypeTree, alts: Seq[Expr]) extends Expr with FixedType with NAryExtractable {
+
+ def extract = {
+ Some((alts, (es: Seq[Expr]) => Hole(fixedType, es).setPos(this)))
+ }
+ }
+
/* Like vals */
case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr with FixedType {
val fixedType = body.getType
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
new file mode 100644
index 0000000000000000000000000000000000000000..60a6f8ea0bf1e4b2346c98085699fa7a8b9d228c
--- /dev/null
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -0,0 +1,120 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package synthesis
+
+import purescala.Common._
+import purescala.Trees._
+import purescala.TypeTrees._
+import purescala.TreeOps._
+import purescala.Definitions._
+
+object ConvertHoles extends LeonPhase[Program, Program] {
+ val name = "Convert Holes to Choose"
+ val description = "Convert Holes found in bodies to equivalent Choose"
+
+ /**
+ * This phase converts a body with "withOracle{ .. }" into a choose construct:
+ *
+ * def foo(a: T) = {
+ * require(..a..)
+ * expr(a, ???)
+ * } ensuring { x => post(x) }
+ *
+ * gets converted into:
+ *
+ * def foo(a: T) {
+ * require(..a..)
+ * val h = choose { (h) => {
+ * val res = expr(a, ???)
+ * post(res)
+ * }
+ * expr(a, h)
+ * } ensuring { res =>
+ * post(res)
+ * }
+ *
+ */
+ def run(ctx: LeonContext)(pgm: Program): Program = {
+
+ pgm.definedFunctions.foreach(fd => {
+ if (fd.hasBody) {
+
+ var holes = List[Identifier]()
+
+ val newBody = preMap {
+ case h @ Hole(tpe, es) =>
+ val (expr, ids) = toExpr(h)
+
+ holes ++= ids
+
+ Some(expr)
+ case _ =>
+ None
+ }(fd.body.get)
+
+ if (holes.nonEmpty) {
+ val cids = holes.map(_.freshen)
+ val pred = fd.postcondition match {
+ case Some((id, post)) =>
+ replaceFromIDs((holes zip cids.map(_.toVariable)).toMap, Let(id, newBody, post))
+ case None =>
+ BooleanLiteral(true)
+ }
+
+ val withChoose = if (holes.size > 1) {
+ LetTuple(holes, Choose(cids, pred), newBody)
+ } else {
+ Let(holes.head, Choose(cids, pred), newBody)
+ }
+
+ fd.body = Some(withChoose)
+ }
+
+ }
+
+ // Ensure that holes are not found in pre and/or post conditions
+ fd.precondition.foreach {
+ preTraversal{
+ case _: Hole =>
+ ctx.reporter.error("Holes are not supported in preconditions. (function "+fd.id.asString(ctx)+")")
+ case _ =>
+ }
+ }
+
+ fd.postcondition.foreach { case (id, post) =>
+ preTraversal{
+ case _: Hole =>
+ ctx.reporter.error("Holes are not supported in postconditions. (function "+fd.id.asString(ctx)+")")
+ case _ =>
+ }(post)
+ }
+
+ })
+
+ pgm
+ }
+
+ def toExpr(h: Hole): (Expr, List[Identifier]) = {
+ h.alts match {
+ case Seq() =>
+ val h1 = FreshIdentifier("hole", true).setType(h.getType)
+ (h1.toVariable, List(h1))
+
+ case Seq(v) =>
+ val h1 = FreshIdentifier("hole", true).setType(BooleanType)
+ val h2 = FreshIdentifier("hole", true).setType(h.getType)
+ (IfExpr(h1.toVariable, h2.toVariable, v), List(h1, h2))
+
+ case exs =>
+ var ids: List[Identifier] = Nil
+ val ex = exs.init.foldRight(exs.last)({ (e: Expr, r: Expr) =>
+ val h = FreshIdentifier("hole", true).setType(BooleanType)
+ ids ::= h
+ IfExpr(h.toVariable, e, r)
+ })
+
+ (ex, ids.reverse)
+ }
+ }
+}
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index d5719090ec749321821eef874e9b612aef525880..9d1c277e9a81c69dcb968275c03e0febcb201ed3 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -6,7 +6,7 @@ package utils
import purescala.Definitions.Program
import purescala.{MethodLifting, CompleteAbstractDefinitions}
-import synthesis.{ConvertWithOracle}
+import synthesis.{ConvertWithOracle, ConvertHoles}
object PreprocessingPhase extends TransformationPhase {
@@ -19,6 +19,7 @@ object PreprocessingPhase extends TransformationPhase {
MethodLifting andThen
TypingPhase andThen
ConvertWithOracle andThen
+ ConvertHoles andThen
CompleteAbstractDefinitions andThen
InjectAsserts
diff --git a/src/test/resources/regression/synthesis/Holes/Hole1.scala b/src/test/resources/regression/synthesis/Holes/Hole1.scala
deleted file mode 100644
index 084185b0efcb96208163158049ebfac429a6a116..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/synthesis/Holes/Hole1.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.lang._
-import leon.annotation._
-import leon.lang.synthesis._
-import leon.collection._
-import leon._
-
-object Hole1 {
- def largestInt(a: Int, b: Int)(implicit o: Oracle[Boolean]) = {
- ?(a, b)
- } ensuring { r => r >= b && r >= a }
-}
diff --git a/src/test/resources/regression/synthesis/Holes/Hole2.scala b/src/test/resources/regression/synthesis/Holes/Hole2.scala
deleted file mode 100644
index 3a10748eb70d48aab7a46cc8379dfb3bbaacbfca..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/synthesis/Holes/Hole2.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.lang._
-import leon.annotation._
-import leon.lang.synthesis._
-import leon.collection._
-import leon._
-
-object Hole2 {
- def genList()(implicit o: Oracle[Boolean]): List[Int] = ?(Nil[Int](), Cons[Int](0, genList()(o.right)))
-
- def listOfSize2(implicit o: Oracle[Boolean]) = {
- genList()
- } ensuring {
- _.size == 2
- }
-}