diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 9e97c6c7bfc097c811d86bc825e5082a9be7c7c1..502563f0fe0a32546ded292141430af4be31779a 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -14,7 +14,7 @@ import purescala.Extractors._
import purescala.Quantification._
import solvers.{Model, HenkinModel}
import solvers.SolverFactory
-import synthesis.ConvertHoles.convertHoles
+import synthesis.ConversionPhase.convertHoles
import leon.purescala.ExprOps
abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int) extends Evaluator(ctx, prog) {
diff --git a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
deleted file mode 100644
index db508eaf7964d394f5e11b98590beaa1532a9d5b..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package purescala
-
-import Common._
-import Definitions._
-import Expressions._
-
-object CompleteAbstractDefinitions extends UnitPhase[Program] {
-
- val name = "Materialize abstract functions"
- val description = "Inject fake choose-like body in abstract definitions"
-
- def apply(ctx: LeonContext, program: Program) = {
- for (u <- program.units; m <- u.modules; fd <- m.definedFunctions; if fd.body.isEmpty) {
- val post = fd.postcondition getOrElse (
- Lambda(Seq(ValDef(FreshIdentifier("res", fd.returnType))), BooleanLiteral(true))
- )
- fd.body = Some(Choose(post))
- }
- }
-
-}
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 7216652a427e6784142a17f69c730fa61e2ff0aa..b834eb9f1270bca728b2cdbaa63bb98a37b0dd49 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -886,7 +886,7 @@ object Expressions {
/** $encodingof a synthesizable hole in a program. Represented by `???[tpe]`
* in Leon source code.
*
- * A [[Hole]] gets transformed into a [[Choose]] construct during [[leon.synthesis.ConvertHoles the ConvertHoles phase]].
+ * A [[Hole]] gets transformed into a [[Choose]] construct during [[leon.synthesis.ConversionPhase the ConvertHoles phase]].
*/
case class Hole(tpe: TypeTree, alts: Seq[Expr]) extends Expr with Extractable {
val getType = tpe
diff --git a/src/main/scala/leon/purescala/Quantification.scala b/src/main/scala/leon/purescala/Quantification.scala
index 38fa0ae9f81190096aa4f19cbd5a5a988dbfb249..1b00ed1b41a5053fb07a94695b00f595d54453ba 100644
--- a/src/main/scala/leon/purescala/Quantification.scala
+++ b/src/main/scala/leon/purescala/Quantification.scala
@@ -19,7 +19,7 @@ object Quantification {
qargs: A => Set[B]
): Seq[Set[A]] = {
def rec(oms: Seq[A], mSet: Set[A], qss: Seq[Set[B]]): Seq[Set[A]] = {
- if (qss.exists(_ == quantified)) {
+ if (qss.contains(quantified)) {
Seq(mSet)
} else {
var res = Seq.empty[Set[A]]
@@ -126,12 +126,11 @@ object Quantification {
ctx.reporter.warning("E-matching isn't possible without matchers!")
if (matchers.exists { case (_, args) =>
- args.exists(arg => arg match {
+ args.exists{
case QuantificationMatcher(_, _) => false
case Variable(id) => false
- case _ if (variablesOf(arg) & quantified).nonEmpty => true
- case _ => false
- })
+ case arg => (variablesOf(arg) & quantified).nonEmpty
+ }
}) ctx.reporter.warning("Matcher arguments must have simple form in " + conjunct)
val freeMatchers = matchers.collect { case (Variable(id), args) if free(id) => id -> args }
@@ -143,7 +142,7 @@ object Quantification {
}))
}
- if (id2Quant.filter(_._2.nonEmpty).groupBy(_._2).size >= 1)
+ if (id2Quant.filter(_._2.nonEmpty).groupBy(_._2).nonEmpty)
ctx.reporter.warning("Multiple matchers must provide bijective matching in " + conjunct)
fold[Set[Identifier]] { case (m, children) =>
diff --git a/src/main/scala/leon/synthesis/ConversionPhase.scala b/src/main/scala/leon/synthesis/ConversionPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bab77552bf1c6cfb8d3f151aed97c66bca6904ce
--- /dev/null
+++ b/src/main/scala/leon/synthesis/ConversionPhase.scala
@@ -0,0 +1,185 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package synthesis
+
+import purescala.Common._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.ExprOps._
+import purescala.Definitions._
+import purescala.Constructors._
+
+object ConversionPhase extends UnitPhase[Program] {
+ val name = "Eliminate holes, withOracle and abstract definitions"
+ val description = "Convert Holes, withOracle found in bodies and abstract function bodies to equivalent Choose"
+
+ /**
+ * This phase does 3 things:
+ *
+ * 1) Converts a body with "withOracle{ .. }" into a choose construct:
+ *
+ * def foo(a: T) = {
+ * require(..a..)
+ * withOracle { o =>
+ * expr(a,o) ensuring { x => post(x) }
+ * }
+ * }
+ *
+ * gets converted into:
+ *
+ * def foo(a: T) {
+ * require(..a..)
+ * val o = choose { (o) => {
+ * val res = expr(a, o)
+ * pred(res)
+ * }
+ * expr(a,o)
+ * } ensuring { res =>
+ * pred(res)
+ * }
+ *
+ *
+ * 2) Converts a body with "???" 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, h')
+ * post(res)
+ * )
+ * expr(a, h)
+ * } ensuring { res =>
+ * post(res)
+ * }
+ *
+ * 3) Completes abstract definitions:
+ *
+ * def foo(a: T) = {
+ * require(..a..)
+ * ???
+ * } ensuring { res =>
+ * post(res)
+ * }
+ *
+ * gets converted to:
+ *
+ * def foo(a: T) = {
+ * require(..a..)
+ * choose(x => post(x))
+ * }
+ *
+ */
+
+ def convertHoles(e : Expr, ctx : LeonContext) : Expr = {
+ val (pre, body, post) = breakDownSpecs(e)
+
+ // Ensure that holes are not found in pre and/or post conditions
+ (pre ++ post).foreach {
+ preTraversal{
+ case h : Hole =>
+ ctx.reporter.error(s"Holes are not supported in pre- or postconditions. @ ${h.getPos}")
+ case wo: WithOracle =>
+ ctx.reporter.error(s"WithOracle expressions are not supported in pre- or postconditions: ${wo.asString(ctx)} @ ${wo.getPos}")
+ case _ =>
+ }
+ }
+
+ def toExpr(h: Hole): (Expr, List[Identifier]) = {
+ h.alts match {
+ case Seq() =>
+ val h1 = FreshIdentifier("hole", h.getType, true)
+ (h1.toVariable, List(h1))
+
+ case Seq(v) =>
+ val h1 = FreshIdentifier("hole", BooleanType, true)
+ val h2 = FreshIdentifier("hole", h.getType, true)
+ (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", BooleanType, true)
+ ids ::= h
+ IfExpr(h.toVariable, e, r)
+ })
+
+ (ex, ids.reverse)
+ }
+ }
+
+ body match {
+ case Some(body) =>
+ var holes = List[Identifier]()
+
+ val withoutHoles = preMap {
+ case h : Hole =>
+ val (expr, ids) = toExpr(h)
+
+ holes ++= ids
+
+ Some(expr)
+ case wo @ WithOracle(os, b) =>
+ withoutSpec(b) map { pred =>
+ val chooseOs = os.map(_.freshen)
+
+ val pred = post.getOrElse( // FIXME: We need to freshen variables
+ Lambda(chooseOs.map(ValDef(_)), BooleanLiteral(true))
+ )
+
+ letTuple(os, Choose(pred), b)
+ }
+ case _ =>
+ None
+ }(body)
+
+ if (holes.nonEmpty) {
+ val cids: List[Identifier] = holes.map(_.freshen)
+ val hToFresh = (holes zip cids.map(_.toVariable)).toMap
+
+ val spec = post match {
+ case Some(post: Lambda) =>
+ val asLet = letTuple(post.args.map(_.id), withoutHoles, post.body)
+
+ Lambda(cids.map(ValDef(_)), replaceFromIDs(hToFresh, asLet))
+
+ case _ =>
+ Lambda(cids.map(ValDef(_)), BooleanLiteral(true))
+ }
+
+ val choose = Choose(spec)
+
+ val newBody = if (holes.size == 1) {
+ replaceFromIDs(Map(holes.head -> choose), withoutHoles)
+ } else {
+ letTuple(holes, choose, withoutHoles)
+ }
+
+ withPostcondition(withPrecondition(newBody, pre), post)
+
+ } else {
+ e
+ }
+
+ case None =>
+ val newPost = post getOrElse Lambda(Seq(ValDef(FreshIdentifier("res", e.getType))), BooleanLiteral(true))
+ withPrecondition(Choose(newPost), pre)
+ }
+ }
+
+
+ def apply(ctx: LeonContext, pgm: Program): Unit = {
+ // TODO: remove side-effects
+ for (fd <- pgm.definedFunctions) {
+ fd.fullBody = convertHoles(fd.fullBody,ctx)
+ }
+ }
+
+}
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
deleted file mode 100644
index 8c08f05e89f6fcb133609802ffe46c686e40fa36..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ /dev/null
@@ -1,131 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package synthesis
-
-import purescala.Common._
-import purescala.Expressions._
-import purescala.Types._
-import purescala.ExprOps._
-import purescala.Definitions._
-import purescala.Constructors._
-
-object ConvertHoles extends TransformationPhase {
- val name = "Convert Holes to Choose"
- val description = "Convert Holes found in bodies to equivalent Choose"
-
- /**
- * This phase converts a body with "???" 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, h')
- * post(res)
- * )
- * expr(a, h)
- * } ensuring { res =>
- * post(res)
- * }
- *
- */
-
- def convertHoles(e : Expr, ctx : LeonContext) : Expr = {
- val (pre, body, post) = breakDownSpecs(e)
-
- // Ensure that holes are not found in pre and/or post conditions
- (pre ++ post).foreach {
- preTraversal{
- case h : Hole =>
- ctx.reporter.error("Holes are not supported in pre- or postconditions. @"+ h.getPos)
- case _ =>
- }
- }
-
- body match {
- case Some(body) =>
- var holes = List[Identifier]()
-
- val withoutHoles = preMap {
- case h : Hole =>
- val (expr, ids) = toExpr(h)
-
- holes ++= ids
-
- Some(expr)
- case _ =>
- None
- }(body)
-
- if (holes.nonEmpty) {
- val cids: List[Identifier] = holes.map(_.freshen)
- val hToFresh = (holes zip cids.map(_.toVariable)).toMap
-
- val spec = post match {
- case Some(post: Lambda) =>
- val asLet = letTuple(post.args.map(_.id), withoutHoles, post.body)
-
- Lambda(cids.map(ValDef(_)), replaceFromIDs(hToFresh, asLet))
-
- case _ =>
- Lambda(cids.map(ValDef(_)), BooleanLiteral(true))
- }
-
- val choose = Choose(spec)
-
- val newBody = if (holes.size == 1) {
- replaceFromIDs(Map(holes.head -> choose), withoutHoles)
- } else {
- letTuple(holes, choose, withoutHoles)
- }
-
- withPostcondition(withPrecondition(newBody, pre), post)
-
- } else {
- e
- }
-
- case None => e
- }
- }
-
-
- def apply(ctx: LeonContext, pgm: Program): Program = {
- // TODO: remove side-effects
- for (fd <- pgm.definedFunctions) {
- fd.fullBody = convertHoles(fd.fullBody,ctx)
- }
-
- pgm
- }
-
- def toExpr(h: Hole): (Expr, List[Identifier]) = {
- h.alts match {
- case Seq() =>
- val h1 = FreshIdentifier("hole", h.getType, true)
- (h1.toVariable, List(h1))
-
- case Seq(v) =>
- val h1 = FreshIdentifier("hole", BooleanType, true)
- val h2 = FreshIdentifier("hole", h.getType, true)
- (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", BooleanType, true)
- ids ::= h
- IfExpr(h.toVariable, e, r)
- })
-
- (ex, ids.reverse)
- }
- }
-}
diff --git a/src/main/scala/leon/synthesis/ConvertWithOracle.scala b/src/main/scala/leon/synthesis/ConvertWithOracle.scala
deleted file mode 100644
index ac3785c43e454431ebf18ecc2df4dcec78a6a16b..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/synthesis/ConvertWithOracle.scala
+++ /dev/null
@@ -1,88 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package synthesis
-
-import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Definitions._
-import purescala.Constructors._
-
-object ConvertWithOracle extends TransformationPhase {
- val name = "Convert WithOracle to Choose"
- val description = "Convert WithOracle found in bodies to equivalent Choose"
-
- /**
- * This phase converts a body with "withOracle{ .. }" into a choose construct:
- *
- * def foo(a: T) = {
- * require(..a..)
- * withOracle { o =>
- * expr(a,o) ensuring { x => post(x) }
- * }
- * }
- *
- * gets converted into:
- *
- * def foo(a: T) {
- * require(..a..)
- * val o = choose { (o) => {
- * val res = expr(a, o)
- * pred(res)
- * }
- * expr(a,o)
- * } ensuring { res =>
- * pred(res)
- * }
- *
- */
- def apply(ctx: LeonContext, pgm: Program): Program = {
- // TODO: Remove side-effects
-
- pgm.definedFunctions.foreach(fd => {
- if (fd.hasBody) {
- val body = preMap {
- case wo @ WithOracle(os, b) =>
- withoutSpec(b) match {
- case Some(pred) =>
- val chooseOs = os.map(_.freshen)
-
- val pred = postconditionOf(b) match {
- case Some(post) =>
- post // FIXME we need to freshen variables
- case None =>
- Lambda(chooseOs.map(ValDef(_)), BooleanLiteral(true))
- }
-
- Some(letTuple(os, Choose(pred), b))
- case None =>
- None
- }
- case _ => None
- }(fd.body.get)
-
- fd.body = Some(body)
- }
-
- // Ensure that holes are not found in pre and/or post conditions
- fd.precondition.foreach {
- preTraversal{
- case _: WithOracle =>
- ctx.reporter.error("WithOracle expressions are not supported in preconditions. (function "+fd.id.asString(ctx)+")")
- case _ =>
- }
- }
-
- fd.postcondition.foreach {
- preTraversal{
- case _: WithOracle =>
- ctx.reporter.error("WithOracle expressions are not supported in postconditions. (function "+fd.id.asString(ctx)+")")
- case _ =>
- }
- }
-
- })
-
- pgm
- }
-}
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 38b770ba19a468977cf8018c2ac7d438140525a5..87d1003150995eb236e5f3abb738450516c5b7f7 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -7,11 +7,10 @@ import leon.purescala._
import leon.purescala.Definitions.Program
import leon.purescala.Quantification.CheckForalls
import leon.solvers.isabelle.AdaptationPhase
-import leon.synthesis.{ConvertWithOracle, ConvertHoles}
import leon.verification.InjectAsserts
-import leon.xlang.XLangDesugaringPhase
+import leon.xlang.{NoXLangFeaturesChecking, XLangDesugaringPhase}
-class PreprocessingPhase(private val desugarXLang: Boolean = false) extends LeonPhase[Program, Program] {
+class PreprocessingPhase(desugarXLang: Boolean = false) extends LeonPhase[Program, Program] {
val name = "preprocessing"
val description = "Various preprocessings on Leon programs"
@@ -26,13 +25,18 @@ class PreprocessingPhase(private val desugarXLang: Boolean = false) extends Leon
}
}
+ val checkX = if (desugarXLang) {
+ NoopPhase[Program]()
+ } else {
+ NoXLangFeaturesChecking
+ }
+
val pipeBegin =
debugTrees("Program after extraction") andThen
+ checkX andThen
MethodLifting andThen
TypingPhase andThen
- ConvertWithOracle andThen
- ConvertHoles andThen
- CompleteAbstractDefinitions andThen
+ synthesis.ConversionPhase andThen
CheckADTFieldsTypes andThen
InjectAsserts andThen
InliningPhase andThen
@@ -42,7 +46,7 @@ class PreprocessingPhase(private val desugarXLang: Boolean = false) extends Leon
XLangDesugaringPhase andThen
debugTrees("Program after xlang desugaring")
} else {
- xlang.NoXLangFeaturesChecking
+ NoopPhase[Program]()
}
val phases =