diff --git a/library/lang/package.scala b/library/lang/package.scala
index b19ec529bdb3975956de00a7da8e8ad39bcf34e4..ab713a588e5451ba8ab61533d6037bd2bd572de8 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -20,16 +20,7 @@ package object lang {
if (underlying) that else true
}
}
-
- implicit class SpecsDecorations[A](val underlying: A) {
- @inline
- def computes(target: A) = {
- underlying
- } ensuring {
- res => res == target
- }
- }
-
+
@ignore def forall[A](p: A => Boolean): Boolean = sys.error("Can't execute quantified proposition")
@ignore def forall[A,B](p: (A,B) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
@ignore def forall[A,B,C](p: (A,B,C) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
@@ -56,6 +47,27 @@ package object lang {
def passes(tests : A => B ) : Boolean =
try { tests(in) == out } catch { case _ : MatchError => true }
}
+
+ @ignore
+ def byExample[A, B](in: A, out: B): Boolean = {
+ sys.error("Can't execute by example proposition")
+ }
+
+ implicit class SpecsDecorations[A](val underlying: A) {
+ @ignore
+ def computes(target: A) = {
+ underlying
+ } ensuring {
+ res => res == target
+ }
+
+ @ignore // Programming by example: ???[String] ask input
+ def ask[I](input : I) = {
+ underlying
+ } ensuring {
+ (res: A) => byExample(input, res)
+ }
+ }
@ignore
object BigInt {
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 67e5c4502ad1810b323616916e3edfab9c05a8ea..f8509be9c4d678b10a52f7736a406bb078b6bfbc 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -210,6 +210,37 @@ trait ASTExtractors {
case _ => None
}
}
+
+
+ /** Matches the `A computes B` expression at the end of any expression A, and returns (A, B).*/
+ object ExComputesExpression {
+ def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
+ case Apply(Select(
+ Apply(TypeApply(ExSelected("leon", "lang", "package", "SpecsDecorations"), List(_)), realExpr :: Nil),
+ ExNamed("computes")), expected::Nil)
+ => Some((realExpr, expected))
+ case _ => None
+ }
+ }
+
+ /** Matches the `O ask I` expression at the end of any expression O, and returns (I, O).*/
+ object ExAskExpression {
+ def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
+ case Apply(TypeApply(Select(
+ Apply(TypeApply(ExSelected("leon", "lang", "package", "SpecsDecorations"), List(_)), output :: Nil),
+ ExNamed("ask")), List(_)), input::Nil)
+ => Some((input, output))
+ case _ => None
+ }
+ }
+
+ object ExByExampleExpression {
+ def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
+ case Apply(TypeApply(ExSelected("leon", "lang", "package", "byExample"), List(_, _)), input :: res_output :: Nil)
+ => Some((input, res_output))
+ case _ => None
+ }
+ }
/** Extracts the `(input, output) passes { case In => Out ...}` and returns (input, output, list of case classes) */
object ExPasses {
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 55ab79460e296e2b37c026261e29621488f6fa46..0451b4c08603fb1b10ae91e2e38cc8902cd1649d 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1066,6 +1066,30 @@ trait CodeExtraction extends ASTExtractors {
Ensuring(b, post)
+ case t @ ExComputesExpression(body, expected) =>
+ val b = extractTreeOrNoTree(body).setPos(body.pos)
+ val expected_expr = extractTreeOrNoTree(expected).setPos(expected.pos)
+
+ val resId = FreshIdentifier("res", b.getType).setPos(current.pos)
+ val post = Lambda(Seq(LeonValDef(resId)), Equals(Variable(resId), expected_expr)).setPos(current.pos)
+
+ Ensuring(b, post)
+
+ case t @ ExByExampleExpression(input, output) =>
+ val input_expr = extractTreeOrNoTree(input).setPos(input.pos)
+ val output_expr = extractTreeOrNoTree(output).setPos(output.pos)
+ Passes(input_expr, output_expr, MatchCase(WildcardPattern(None), Some(BooleanLiteral(false)), NoTree(output_expr.getType))::Nil)
+
+ case t @ ExAskExpression(input, output) =>
+ val input_expr = extractTreeOrNoTree(input).setPos(input.pos)
+ val output_expr = extractTreeOrNoTree(output).setPos(output.pos)
+
+ val resId = FreshIdentifier("res", output_expr.getType).setPos(current.pos)
+ val post = Lambda(Seq(LeonValDef(resId)),
+ Passes(input_expr, Variable(resId), MatchCase(WildcardPattern(None), Some(BooleanLiteral(false)), NoTree(output_expr.getType))::Nil)).setPos(current.pos)
+
+ Ensuring(output_expr, post)
+
case ExAssertExpression(contract, oerr) =>
val const = extractTree(contract)
val b = rest.map(extractTreeOrNoTree).getOrElse(UnitLiteral())
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 67296c3dc4f2cc130915d7adfdb3cc186447d7df..20502a13640e1ab3fd5820a9bcfc38de46ece0f5 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -114,11 +114,17 @@ class PrettyPrinter(opts: PrinterOptions,
|}"""
case p@Passes(in, out, tests) =>
- optP {
- p"""|($in, $out) passes {
- | ${nary(tests, "\n")}
- |}"""
+ tests match {
+ case Seq(MatchCase(_, Some(BooleanLiteral(false)), NoTree(_))) =>
+ p"""|byExample($in, $out)"""
+ case _ =>
+ optP {
+ p"""|($in, $out) passes {
+ | ${nary(tests, "\n")}
+ |}"""
+ }
}
+
case c @ WithOracle(vars, pred) =>
p"""|withOracle { (${typed(vars)}) =>
diff --git a/src/main/scala/leon/synthesis/ConversionPhase.scala b/src/main/scala/leon/synthesis/ConversionPhase.scala
index 0252a40c44e1def779265563b19161aefc676060..ce9f1525f5e012800400c7b9c0776914d989b43b 100644
--- a/src/main/scala/leon/synthesis/ConversionPhase.scala
+++ b/src/main/scala/leon/synthesis/ConversionPhase.scala
@@ -99,7 +99,7 @@ object ConversionPhase extends UnitPhase[Program] {
(pre ++ post).foreach {
preTraversal{
case h : Hole =>
- ctx.reporter.error(s"Holes are not supported in pre- or postconditions. @ ${h.getPos}")
+ ctx.reporter.error(s"Holes like $h 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 _ =>
diff --git a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
index 9303b4d1ef9813a38109b35c17adadf546297252..e5071b9b4ecbdcde1d1b5a339b486c7820d20bfc 100644
--- a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
@@ -51,8 +51,10 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
addToFunDef(fd, Seq((newIn, newOut)))
}
+ private def filterCases(cases: Seq[MatchCase]) = cases.filter(c => c.optGuard != Some(BooleanLiteral(false)))
+
/** Adds the given input/output examples to the function definitions */
- def addToFunDef(fd: FunDef, examples: Seq[(Expr, Expr)]) = {
+ def addToFunDef(fd: FunDef, examples: Seq[(Expr, Expr)]): Unit = {
val params = if(_removeFunctionParameters) fd.params.filter(x => !x.getType.isInstanceOf[FunctionType]) else fd.params
val inputVariables = tupleWrap(params.map(p => Variable(p.id): Expr))
val newCases = examples.map{ case (in, out) => exampleToCase(in, out) }
@@ -71,7 +73,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
} else {
val newPasses = exprs(i) match {
case Passes(in, out, cases) =>
- Passes(in, out, (cases ++ newCases).distinct )
+ Passes(in, out, (filterCases(cases) ++ newCases).distinct )
case _ => ???
}
val newPost = and(exprs.updated(i, newPasses) : _*)
diff --git a/testcases/stringrender/ModularRender.scala b/testcases/stringrender/ModularRender.scala
index 4757e3cc3135fa5818abf1ee34fd4b8a072a00fe..cf46ab0ab81162d9bf13fd2cfd89c1ca842f262c 100644
--- a/testcases/stringrender/ModularRender.scala
+++ b/testcases/stringrender/ModularRender.scala
@@ -31,12 +31,6 @@ object ModularRender {
case class Configuration(flags: List[Boolean])
// We want to write Config:[Up,Down,Up....]
- def ConfigToString(config : Configuration): String = {
- ???
- } ensuring {
- (res : String) => (config, res) passes {
- case _ if false =>
- ""
- }
- }
+ def ConfigToString(config : Configuration): String =
+ ???[String] ask config
}
diff --git a/testcases/stringrender/SymbolGrammarRender.scala b/testcases/stringrender/SymbolGrammarRender.scala
index 5998e6b3895f59c4cff518f74e0ca860a59b2b4e..af03bdbbfc4ced66729e03171a1c633cb267d672 100644
--- a/testcases/stringrender/SymbolGrammarRender.scala
+++ b/testcases/stringrender/SymbolGrammarRender.scala
@@ -49,12 +49,6 @@ object GrammarRender {
}
}
- def grammarToString(p : Grammar): String = {
- ???[String]
- } ensuring {
- (res : String) => (p, res) passes {
- case _ if false =>
- ""
- }
- }
+ def grammarToString(p : Grammar): String =
+ ???[String] ask p
}
\ No newline at end of file
diff --git a/testcases/web/synthesis/26_Modular_Render.scala b/testcases/web/synthesis/26_Modular_Render.scala
index 54a5cc3fbf9f4af852d4de797307af8e84278c4f..d180d7e4c8ac4b217136b023afe9bd9c0d833005 100644
--- a/testcases/web/synthesis/26_Modular_Render.scala
+++ b/testcases/web/synthesis/26_Modular_Render.scala
@@ -11,31 +11,22 @@ import leon.collection.ListOps._
import leon.lang.synthesis._
object ModularRender {
- def customToString[T](l : List[T], f : (T) => String): String = {
- ???
- } ensuring {
- (res : String) => (l, res) passes {
- case _ if false => ""
- }
- }
def booleanToString(b: Boolean) = if(b) "Up" else "Down"
+
def intToString(b: BigInt) = b.toString
+ def customToString[T](l : List[T], f : (T) => String): String =
+ ???[String] ask l
+
case class Configuration(flags: List[Boolean], strokes: List[BigInt])
// We want to write
// Solution:
// [Up, Down, Up....]
// [1, 2, 5, ...]
- def ConfigToString(config : Configuration): String = {
- ???
- } ensuring {
- (res : String) => (config, res) passes {
- case _ if false =>
- ""
- }
- }
+ def ConfigToString(config : Configuration): String =
+ ???[String] ask config
/** Wrong lemma for demonstration */
def configurationsAreSimple(c: Configuration) =