From cacee995b3b13b28672c96a6646216905408634c Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 25 Feb 2016 18:21:43 +0100
Subject: [PATCH] Refactor Terminating to be more modular
---
.../scala/leon/purescala/Definitions.scala | 3 +++
src/main/scala/leon/purescala/ExprOps.scala | 22 -------------------
src/main/scala/leon/repair/Repairman.scala | 2 +-
.../scala/leon/synthesis/SourceInfo.scala | 2 +-
src/main/scala/leon/synthesis/Witnesses.scala | 9 ++++----
.../leon/synthesis/rules/CEGISLike.scala | 4 ++--
.../synthesis/rules/IntroduceRecCalls.scala | 4 +---
.../scala/leon/synthesis/utils/Helpers.scala | 2 +-
8 files changed, 13 insertions(+), 35 deletions(-)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index b52e7e6b9..753e92360 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 801bc8c7c..c632a6d69 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 0ec09cbf1..49f9c0ff2 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 af78f2275..ca689cca0 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 6e040e7c4..ed33df173 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 128d7299d..b8a41fdf7 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 0a4c32f74..8fdb03c55 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 493e166a8..14b7e2fb3 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);
--
GitLab