diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 689b87fe995aee858c6ff7a229bf48bdcc9f4ec4..ce64bbadb6b26273d42f76dbae8f324e48e1a327 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -108,43 +108,6 @@ object Extractors {
MatchExpr(es(0), newcases)
}))
- case LetDef(fd, body) =>
- fd.body match {
- case Some(b) =>
- (fd.precondition, fd.postcondition) match {
- case (None, None) =>
- Some((Seq(b, body), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.body = Some(as(0))
- LetDef(nfd, as(1))
- }))
- case (Some(pre), None) =>
- Some((Seq(b, body, pre), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.body = Some(as(0))
- nfd.precondition = Some(as(2))
- LetDef(nfd, as(1))
- }))
- case (None, Some(post)) =>
- Some((Seq(b, body, post), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.body = Some(as(0))
- nfd.postcondition = Some(as(2))
- LetDef(nfd, as(1))
- }))
- case (Some(pre), Some(post)) =>
- Some((Seq(b, body, pre, post), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.body = Some(as(0))
- nfd.precondition = Some(as(2))
- nfd.postcondition = Some(as(3))
- LetDef(nfd, as(1))
- }))
- }
-
- case _ =>
- None
- }
case (ex: NAryExtractable) => ex.extract
case _ => None
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 360b1306193074649e2b38a2e1b46ba2d3bcefd2..27d1b6e74b33f65b9ebae069ff41d85afdbc99f1 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -88,15 +88,6 @@ object PrettyPrinter {
sb.append(")")
sb
}
- case LetDef(fd,e) => {
- sb.append("\n")
- pp(fd, sb, lvl+1)
- sb.append("\n")
- sb.append("\n")
- ind(sb, lvl)
- pp(e, sb, lvl)
- sb
- }
case And(exprs) => ppNary(sb, exprs, "(", " \u2227 ", ")", lvl) // \land
case Or(exprs) => ppNary(sb, exprs, "(", " \u2228 ", ")", lvl) // \lor
case Not(Equals(l, r)) => ppBinary(sb, l, r, " \u2260 ", lvl) // \neq
@@ -358,13 +349,17 @@ object PrettyPrinter {
nsb
}
- case (expr: PrettyPrintable) => expr.pp(sb, lvl, pp)
+ case (expr: PrettyPrintable) => expr.pp(sb, lvl, pp, pp, pp)
case _ => sb.append("Expr?")
}
trait PrettyPrintable {
- def pp(sb: StringBuffer, lvl: Int, rp: (Expr, StringBuffer, Int) => StringBuffer): StringBuffer
+ def pp(sb: StringBuffer, lvl: Int,
+ ep: (Expr, StringBuffer, Int) => StringBuffer,
+ tp: (TypeTree, StringBuffer, Int) => StringBuffer,
+ dp: (Definition, StringBuffer, Int) => StringBuffer
+ ): StringBuffer
}
// TYPE TREES
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 11672b7d87529824ac1f2900db060a7833204a45..d2059302ce109fd389b82647afa80b91919c29c7 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -1,7 +1,5 @@
package leon.purescala
-import leon.xlang.Trees._
-
/** This pretty-printer only print valid scala syntax */
object ScalaPrinter {
import Common._
@@ -98,27 +96,6 @@ object ScalaPrinter {
sb.append("}\n")
ind(sb, lvl)
}
- case LetVar(b,d,e) => {
- sb.append("locally {\n")
- ind(sb, lvl+1)
- sb.append("var " + b + " = ")
- pp(d, sb, lvl+1)
- sb.append("\n")
- ind(sb, lvl+1)
- pp(e, sb, lvl+1)
- sb.append("\n")
- ind(sb, lvl)
- sb.append("}\n")
- ind(sb, lvl)
- }
- case LetDef(fd,e) => {
- sb.append("\n")
- pp(fd, sb, lvl+1)
- sb.append("\n")
- sb.append("\n")
- ind(sb, lvl)
- pp(e, sb, lvl)
- }
case And(exprs) => ppNary(sb, exprs, "(", " && ", ")", lvl) // \land
case Or(exprs) => ppNary(sb, exprs, "(", " || ", ")", lvl) // \lor
case Not(Equals(l, r)) => ppBinary(sb, l, r, " != ", lvl) // \neq
@@ -130,36 +107,6 @@ object ScalaPrinter {
case BooleanLiteral(v) => sb.append(v)
case StringLiteral(s) => sb.append("\"" + s + "\"")
case UnitLiteral => sb.append("()")
- case Block(exprs, last) => {
- sb.append("{\n")
- (exprs :+ last).foreach(e => {
- ind(sb, lvl+1)
- pp(e, sb, lvl+1)
- sb.append("\n")
- })
- ind(sb, lvl)
- sb.append("}\n")
- }
- case Assignment(lhs, rhs) => ppBinary(sb, lhs.toVariable, rhs, " = ", lvl)
- case wh@While(cond, body) => {
- wh.invariant match {
- case Some(inv) => {
- sb.append("\n")
- ind(sb, lvl)
- sb.append("@invariant: ")
- pp(inv, sb, lvl)
- sb.append("\n")
- ind(sb, lvl)
- }
- case None =>
- }
- sb.append("while(")
- pp(cond, sb, lvl)
- sb.append(")\n")
- ind(sb, lvl+1)
- pp(body, sb, lvl+1)
- sb.append("\n")
- }
case t@Tuple(exprs) => ppNary(sb, exprs, "(", ", ", ")", lvl)
case s@TupleSelect(t, i) => {
@@ -167,9 +114,6 @@ object ScalaPrinter {
sb.append("._" + i)
}
- case e@Epsilon(pred) => sys.error("Not Scala Code")
- case Waypoint(i, expr) => pp(expr, sb, lvl)
-
case OptionSome(a) => {
sb.append("Some(")
pp(a, sb, lvl)
@@ -278,13 +222,6 @@ object ScalaPrinter {
pp(i, sb, lvl)
sb.append(")")
}
- case up@ArrayUpdate(ar, i, v) => {
- pp(ar, sb, lvl)
- sb.append("(")
- pp(i, sb, lvl)
- sb.append(") = ")
- pp(v, sb, lvl)
- }
case up@ArrayUpdated(ar, i, v) => {
pp(ar, sb, lvl)
sb.append(".updated(")
@@ -398,7 +335,6 @@ object ScalaPrinter {
}
case ResultVariable() => sb.append("res")
- case EpsilonVariable((row, col)) => sb.append("x" + row + "_" + col)
case Not(expr) => ppUnary(sb, expr, "!(", ")", lvl) // \neg
case e @ Error(desc) => {
@@ -407,6 +343,7 @@ object ScalaPrinter {
sb.append("](\"" + desc + "\")")
}
+ case (expr: ScalaPrintable) => expr.ppScala(sb, lvl, pp, pp, pp)
case _ => sb.append("Expr?")
}
@@ -596,4 +533,12 @@ object ScalaPrinter {
case _ => sb.append("Defn?")
}
}
+
+ trait ScalaPrintable {
+ def ppScala(sb: StringBuffer, lvl: Int,
+ ep: (Expr, StringBuffer, Int) => Unit,
+ tp: (TypeTree, StringBuffer, Int) => Unit,
+ dp: (Definition, StringBuffer, Int) => Unit
+ ): StringBuffer
+ }
}
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 25985b4b6776c254998b0b2c459ea45822137a6f..a38c557ae03445754a25db9ecc85e1410c62e90e 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -57,13 +57,13 @@ object TreeOps {
else
l
}
- case l @ LetDef(fd, b) => {
- //TODO, not sure, see comment for the next LetDef
- fd.body = fd.body.map(rec(_))
- fd.precondition = fd.precondition.map(rec(_))
- fd.postcondition = fd.postcondition.map(rec(_))
- LetDef(fd, rec(b)).setType(l.getType)
- }
+ //case l @ LetDef(fd, b) => {
+ // //TODO, not sure, see comment for the next LetDef
+ // fd.body = fd.body.map(rec(_))
+ // fd.precondition = fd.precondition.map(rec(_))
+ // fd.postcondition = fd.postcondition.map(rec(_))
+ // LetDef(fd, rec(b)).setType(l.getType)
+ //}
case lt @ LetTuple(ids, expr, body) => {
val re = rec(expr)
@@ -176,14 +176,14 @@ object TreeOps {
l
})
}
- case l @ LetDef(fd,b) => {
- //TODO: Not sure: I actually need the replace to occurs even in the pre/post condition, hope this is correct
- fd.body = fd.body.map(rec(_))
- fd.precondition = fd.precondition.map(rec(_))
- fd.postcondition = fd.postcondition.map(rec(_))
- val rl = LetDef(fd, rec(b)).setType(l.getType)
- applySubst(rl)
- }
+ //case l @ LetDef(fd,b) => {
+ // //TODO: Not sure: I actually need the replace to occurs even in the pre/post condition, hope this is correct
+ // fd.body = fd.body.map(rec(_))
+ // fd.precondition = fd.precondition.map(rec(_))
+ // fd.postcondition = fd.postcondition.map(rec(_))
+ // val rl = LetDef(fd, rec(b)).setType(l.getType)
+ // applySubst(rl)
+ //}
case n @ NAryOperator(args, recons) => {
var change = false
val rargs = args.map(a => {
@@ -317,10 +317,10 @@ object TreeOps {
def treeCatamorphism[A](convert: Expr=>A, combine: (A,A)=>A, compute: (Expr,A)=>A, expression: Expr) : A = {
def rec(expr: Expr) : A = expr match {
case l @ Let(_, e, b) => compute(l, combine(rec(e), rec(b)))
- case l @ LetDef(fd, b) => {//TODO, still not sure about the semantic
- val exprs: Seq[Expr] = fd.precondition.toSeq ++ fd.body.toSeq ++ fd.postcondition.toSeq ++ Seq(b)
- compute(l, exprs.map(rec(_)).reduceLeft(combine))
- }
+ //case l @ LetDef(fd, b) => {//TODO, still not sure about the semantic
+ // val exprs: Seq[Expr] = fd.precondition.toSeq ++ fd.body.toSeq ++ fd.postcondition.toSeq ++ Seq(b)
+ // compute(l, exprs.map(rec(_)).reduceLeft(combine))
+ //}
case n @ NAryOperator(args, _) => {
if(args.size == 0)
compute(n, convert(n))
@@ -340,18 +340,6 @@ object TreeOps {
rec(expression)
}
- def containsLetDef(expr: Expr): Boolean = {
- def convert(t : Expr) : Boolean = t match {
- case (l : LetDef) => true
- case _ => false
- }
- def combine(c1 : Boolean, c2 : Boolean) : Boolean = c1 || c2
- def compute(t : Expr, c : Boolean) = t match {
- case (l : LetDef) => true
- case _ => c
- }
- treeCatamorphism(convert, combine, compute, expr)
- }
def containsIfExpr(expr: Expr): Boolean = {
def convert(t : Expr) : Boolean = t match {
case (i: IfExpr) => true
@@ -444,9 +432,9 @@ object TreeOps {
def allIdentifiers(expr: Expr) : Set[Identifier] = expr match {
case l @ Let(binder, e, b) => allIdentifiers(e) ++ allIdentifiers(b) + binder
- //TODO: Cannot have LetVar here, should not be visible at this point
+ //TODO: Cannot have LetVar nor LetDef here, should not be visible at this point
//case l @ LetVar(binder, e, b) => allIdentifiers(e) ++ allIdentifiers(b) + binder
- case l @ LetDef(fd, b) => allIdentifiers(fd.getBody) ++ allIdentifiers(b) + fd.id
+ //case l @ LetDef(fd, b) => allIdentifiers(fd.getBody) ++ allIdentifiers(b) + fd.id
case n @ NAryOperator(args, _) =>
(args map (TreeOps.allIdentifiers(_))).foldLeft(Set[Identifier]())((a, b) => a ++ b)
case b @ BinaryOperator(a1,a2,_) => allIdentifiers(a1) ++ allIdentifiers(a2)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 195b58e83f1040b0a5519ce0f60ea2c99c01b8a4..c2f47b7f9fb521069752190f9f79176746e682d7 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -42,12 +42,6 @@ object Trees {
setType(et)
}
- case class LetDef(value: FunDef, body: Expr) extends Expr {
- val et = body.getType
- if(et != Untyped)
- setType(et)
- }
-
/* Control flow */
case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr with FixedType with ScalacPositional {
val fixedType = funDef.returnType
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 602b5f7716c66b99c25ba660befe9549ce7130d7..945e9796b01eed0b990cae2c1963acb508eb0314 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -4,6 +4,7 @@ package synthesis
import leon.purescala.Trees._
import leon.purescala.Definitions._
import leon.purescala.TreeOps._
+import leon.xlang.Trees.LetDef
// Defines a synthesis solution of the form:
// ⟨ P | T ⟩
diff --git a/src/main/scala/leon/xlang/TreeOps.scala b/src/main/scala/leon/xlang/TreeOps.scala
index 0259b8e68d2f335f682bd27c8a144cd33141c93c..c567a85dcc98959c00c4821de45dbcf3ac8ffc85 100644
--- a/src/main/scala/leon/xlang/TreeOps.scala
+++ b/src/main/scala/leon/xlang/TreeOps.scala
@@ -75,4 +75,17 @@ object TreeOps {
searchAndReplaceDFS(applyToTree)(expr)
}
+ def containsLetDef(expr: Expr): Boolean = {
+ def convert(t : Expr) : Boolean = t match {
+ case (l : LetDef) => true
+ case _ => false
+ }
+ def combine(c1 : Boolean, c2 : Boolean) : Boolean = c1 || c2
+ def compute(t : Expr, c : Boolean) = t match {
+ case (l : LetDef) => true
+ case _ => c
+ }
+ treeCatamorphism(convert, combine, compute, expr)
+ }
+
}