diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index b52e7e6b93e76e53e97dd9e483785ffcc0c0f40a..753e9236064a4ee3eaedbe13647de85a133dcd5f 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -524,6 +524,9 @@ object Definitions {
def isRecursive(p: Program) = p.callGraph.transitiveCallees(this) contains this
def paramIds = params map { _.id }
+
+ def applied(args: Seq[Expr]): FunctionInvocation = Constructors.functionInvocation(this, args)
+ def applied = FunctionInvocation(this.typed, this.paramIds map Variable)
}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 801bc8c7cdc5f4e98150b7ee716fe48e26fedd07..c632a6d6999e2e9ada259d6041b4e041178fe527 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1436,10 +1436,6 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
else (m: Apriori) => None} &&
(args1 zip args2).mergeall{ case (a1, a2) => isHomo(a1, a2) }
- case (Terminating(tfd1, args1), Terminating(tfd2, args2)) =>
- idHomo(tfd1.fd.id, tfd2.fd.id)(apriori) && tfd1.tps.zip(tfd2.tps).mergeall{ case (t1, t2) => if(t1 == t2) (m: Apriori) => Option(m) else (m: Apriori) => None} &&
- (args1 zip args2).mergeall{ case (a1, a2) => isHomo(a1, a2) }
-
case (Lambda(defs, body), Lambda(defs2, body2)) =>
// We remove variables introduced by lambdas.
((defs zip defs2).mergeall{ case (ValDef(a1), ValDef(a2)) =>
@@ -1558,8 +1554,6 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
}
- import synthesis.Witnesses.Terminating
-
val res = (t1, t2) match {
case (Variable(i1), Variable(i2)) =>
idHomo(i1, i2)
@@ -1589,14 +1583,6 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
fdHomo(tfd1.fd, tfd2.fd) &&
(args1 zip args2).forall{ case (a1, a2) => isHomo(a1, a2) }
- case (Terminating(tfd1, args1), Terminating(tfd2, args2)) =>
- // TODO: Check type params
- fdHomo(tfd1.fd, tfd2.fd) &&
- (args1 zip args2).forall{ case (a1, a2) => isHomo(a1, a2) }
-
- case (v1, v2) if isValue(v1) && isValue(v2) =>
- v1 == v2
-
case Same(Deconstructor(es1, _), Deconstructor(es2, _)) =>
(es1.size == es2.size) &&
(es1 zip es2).forall{ case (e1, e2) => isHomo(e1, e2) }
@@ -2050,7 +2036,6 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
def liftClosures(e: Expr): (Set[FunDef], Expr) = {
var fds: Map[FunDef, FunDef] = Map()
- import synthesis.Witnesses.Terminating
val res1 = preMap({
case LetDef(lfds, b) =>
val nfds = lfds.map(fd => fd -> fd.duplicate())
@@ -2066,13 +2051,6 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
None
}
- case Terminating(tfd, args) =>
- if (fds contains tfd.fd) {
- Some(Terminating(fds(tfd.fd).typed(tfd.tps), args))
- } else {
- None
- }
-
case _ =>
None
})(e)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 0ec09cbf1bdc30f77e11201a751312c16f1bbabc..49f9c0ff2fbe318d303f0c9e2f2719c0da60bf75 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -179,7 +179,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val origBody = fd.body.get
- val term = Terminating(fd.typed, fd.params.map(_.id.toVariable))
+ val term = Terminating(fd.applied)
val guide = Guide(origBody)
val pre = fd.precOrTrue
diff --git a/src/main/scala/leon/synthesis/SourceInfo.scala b/src/main/scala/leon/synthesis/SourceInfo.scala
index af78f227531217a1fbd3411130ecf4243df80add..ca689cca02a138c7562c517a1dccad108f2f4a3d 100644
--- a/src/main/scala/leon/synthesis/SourceInfo.scala
+++ b/src/main/scala/leon/synthesis/SourceInfo.scala
@@ -47,7 +47,7 @@ object SourceInfo {
def extractFromFunction(ctx: LeonContext, prog: Program, fd: FunDef): Seq[SourceInfo] = {
- val term = Terminating(fd.typed, fd.params.map(_.id.toVariable))
+ val term = Terminating(fd.applied)
val eFinder = new ExamplesFinder(ctx, prog)
diff --git a/src/main/scala/leon/synthesis/Witnesses.scala b/src/main/scala/leon/synthesis/Witnesses.scala
index 6e040e7c4f82b982ca4428dc875ea8e9fc679621..ed33df1736d8247416a6bebbc67e57f3f3317ef5 100644
--- a/src/main/scala/leon/synthesis/Witnesses.scala
+++ b/src/main/scala/leon/synthesis/Witnesses.scala
@@ -4,7 +4,6 @@ package leon.synthesis
import leon.purescala._
import Types._
-import Definitions.TypedFunDef
import Extractors._
import Expressions.Expr
import PrinterHelpers._
@@ -23,12 +22,12 @@ object Witnesses {
p"⊙{$e}"
}
}
-
- case class Terminating(tfd: TypedFunDef, args: Seq[Expr]) extends Witness {
- def extract: Option[(Seq[Expr], Seq[Expr] => Expr)] = Some((args, Terminating(tfd, _)))
+
+ case class Terminating(fi: Expr) extends Witness {
+ def extract: Option[(Seq[Expr], Seq[Expr] => Expr)] = Some(( Seq(fi), { case Seq(fi) => Terminating(fi) }))
override def printWith(implicit pctx: PrinterContext): Unit = {
- p"↓${tfd.id}($args)"
+ p"↓$fi"
}
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 128d7299da70987e1a408f100619b8a42a46b92a..b8a41fdf7309e1cd05274055d3eca3cf4795bc41 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -343,7 +343,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
val e = builder(cs.map { c =>
val fd = cToFd(c)
- FunctionInvocation(fd.typed, fd.params.map(_.toVariable))
+ fd.applied
})
outerExprToInnerExpr(e)
@@ -371,7 +371,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
// Top-level expression for rootC
val expr = {
val fd = cToFd(rootC)
- FunctionInvocation(fd.typed, fd.params.map(_.toVariable))
+ fd.applied
}
(expr, cToFd.values.toSeq)
diff --git a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala b/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
index 0a4c32f7467414bac5d897bd6f4c309478193ad5..8fdb03c55967b875a6b02382fc1c842ed85e1382 100644
--- a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
+++ b/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
@@ -75,9 +75,7 @@ case object IntroduceRecCalls extends NormalizingRule("Introduce rec. calls") {
}) else Nil
}
- val newWs = calls map {
- case FunctionInvocation(tfd, args) => Terminating(tfd, args)
- }
+ val newWs = calls map Terminating
val TopLevelAnds(ws) = p.ws
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index 493e166a80a9f26cafaba104d8062c3504f8cea5..14b7e2fb362b119c5f250e3f6e2752380e9add9c 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -79,7 +79,7 @@ object Helpers {
}
val res = gs.flatMap {
- case term@Terminating(tfd, args) if tpe forall (isSubtypeOf(tfd.returnType, _)) =>
+ case term@Terminating(FunctionInvocation(tfd, args)) if tpe forall (isSubtypeOf(tfd.returnType, _)) =>
val ids = tfd.params.map(vd => FreshIdentifier("<hole>", vd.getType, true)).toList
for (((a, i), tpe) <- args.zipWithIndex zip tfd.params.map(_.getType);