From 738188ea25d5e78f779b75a88422bd7484b1ef08 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 3 Feb 2016 18:27:43 +0100
Subject: [PATCH] Remove ValDef.isLazy, treat byName argument during extraction
alone
---
.../leon/frontends/scalac/CodeExtraction.scala | 14 +++++++++++---
.../invariant/engine/UnfoldingTemplateSolver.scala | 2 +-
src/main/scala/leon/invariant/util/TreeUtil.scala | 2 +-
src/main/scala/leon/purescala/Constructors.scala | 4 ++--
src/main/scala/leon/purescala/Definitions.scala | 2 +-
src/main/scala/leon/purescala/PrettyPrinter.scala | 4 ++--
.../scala/leon/purescala/ScopeSimplifier.scala | 4 ++--
src/main/scala/leon/synthesis/ExamplesFinder.scala | 2 +-
.../synthesis/disambiguation/ExamplesAdder.scala | 14 +++++++-------
.../leon/transformations/IntToRealProgram.scala | 4 ++--
.../SerialInstrumentationPhase.scala | 4 ++--
11 files changed, 32 insertions(+), 24 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index b76198f5d..3e9366400 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -625,6 +625,8 @@ trait CodeExtraction extends ASTExtractors {
}
}
+ private var isLazy = Set[LeonValDef]()
+
private var defsToDefs = Map[Symbol, FunDef]()
private def defineFunDef(sym: Symbol, within: Option[LeonClassDef] = None)(implicit dctx: DefContext): FunDef = {
@@ -638,7 +640,13 @@ trait CodeExtraction extends ASTExtractors {
val tpe = if (sym.isByNameParam) FunctionType(Seq(), ptpe) else ptpe
val newID = FreshIdentifier(sym.name.toString, tpe).setPos(sym.pos)
owners += (newID -> None)
- LeonValDef(newID, sym.isByNameParam).setPos(sym.pos)
+ val vd = LeonValDef(newID).setPos(sym.pos)
+
+ if (sym.isByNameParam) {
+ isLazy += vd
+ }
+
+ vd
}
val tparamsDef = tparams.map(t => TypeParameterDef(t._2))
@@ -1534,7 +1542,7 @@ trait CodeExtraction extends ASTExtractors {
val fd = getFunDef(sym, c.pos)
val newTps = tps.map(t => extractType(t))
- val argsByName = (fd.params zip args).map(p => if (p._1.isLazy) Lambda(Seq(), p._2) else p._2)
+ val argsByName = (fd.params zip args).map(p => if (isLazy(p._1)) Lambda(Seq(), p._2) else p._2)
FunctionInvocation(fd.typed(newTps), argsByName)
@@ -1543,7 +1551,7 @@ trait CodeExtraction extends ASTExtractors {
val cd = methodToClass(fd)
val newTps = tps.map(t => extractType(t))
- val argsByName = (fd.params zip args).map(p => if (p._1.isLazy) Lambda(Seq(), p._2) else p._2)
+ val argsByName = (fd.params zip args).map(p => if (isLazy(p._1)) Lambda(Seq(), p._2) else p._2)
MethodInvocation(rec, cd, fd.typed(newTps), argsByName)
diff --git a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
index 3fe13e7c9..d2deb1ced 100644
--- a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
@@ -42,7 +42,7 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F
def constructVC(funDef: FunDef): (Expr, Expr) = {
val body = funDef.body.get
- val Lambda(Seq(ValDef(resid, _)), _) = funDef.postcondition.get
+ val Lambda(Seq(ValDef(resid)), _) = funDef.postcondition.get
val resvar = resid.toVariable
val simpBody = matchToIfThenElse(body)
diff --git a/src/main/scala/leon/invariant/util/TreeUtil.scala b/src/main/scala/leon/invariant/util/TreeUtil.scala
index 4109e5987..26398130a 100644
--- a/src/main/scala/leon/invariant/util/TreeUtil.scala
+++ b/src/main/scala/leon/invariant/util/TreeUtil.scala
@@ -182,7 +182,7 @@ object ProgramUtil {
funDef.fullBody match {
case Ensuring(_, post) => {
post match {
- case Lambda(Seq(ValDef(fromRes, _)), _) => Some(fromRes)
+ case Lambda(Seq(ValDef(fromRes)), _) => Some(fromRes)
}
}
case _ => None
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index edcc53db2..e3ce7d1e0 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -327,9 +327,9 @@ object Constructors {
var defs: Seq[(Identifier, Expr)] = Seq()
val subst = formalArgs.zip(realArgs).map {
- case (ValDef(from, _), to:Variable) =>
+ case (ValDef(from), to:Variable) =>
from -> to
- case (ValDef(from, _), e) =>
+ case (ValDef(from), e) =>
val fresh = from.freshen
defs :+= (fresh -> e)
from -> Variable(fresh)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 792e43c56..8fb753d23 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -45,7 +45,7 @@ object Definitions {
* The optional tpe, if present, overrides the type of the underlying Identifier id
* This is useful to instantiate argument types of polymorphic functions
*/
- case class ValDef(id: Identifier, isLazy: Boolean = false) extends Definition with Typed {
+ case class ValDef(id: Identifier) extends Definition with Typed {
self: Serializable =>
val getType = id.getType
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index f2be95fb0..99663384d 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -359,8 +359,8 @@ class PrettyPrinter(opts: PrinterOptions,
case Not(expr) => p"\u00AC$expr"
- case vd @ ValDef(id, lzy) =>
- p"$id :${if (lzy) "=> " else ""} ${vd.getType}"
+ case vd @ ValDef(id) =>
+ p"$id : ${vd.getType}"
vd.defaultValue.foreach { fd => p" = ${fd.body.get}" }
case This(_) => p"this"
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 7bae40c5b..f0ff379ff 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -44,10 +44,10 @@ class ScopeSimplifier extends Transformer {
}
val fds_mapping = for((fd, newId) <- fds_newIds) yield {
- val newArgs = for(ValDef(id, tpe) <- fd.params) yield {
+ val newArgs = for(ValDef(id) <- fd.params) yield {
val newArg = genId(id, newScope)
newScope = newScope.register(id -> newArg)
- ValDef(newArg, tpe)
+ ValDef(newArg)
}
val newFd = fd.duplicate(id = newId, params = newArgs)
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 3f144d88f..5077f9467 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -27,7 +27,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
val reporter = ctx.reporter
def extractFromFunDef(fd: FunDef, partition: Boolean): ExamplesBank = fd.postcondition match {
- case Some(Lambda(Seq(ValDef(id, _)), post)) =>
+ case Some(Lambda(Seq(ValDef(id)), post)) =>
// @mk FIXME: make this more general
val tests = extractTestsOf(post)
diff --git a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
index cfe8f456a..6e9dc2376 100644
--- a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
@@ -30,7 +30,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
val inputVariables = tupleWrap(fd.params.map(p => Variable(p.id): Expr))
val newCases = examples.map{ case (in, out) => exampleToCase(in, out) }
fd.postcondition match {
- case Some(Lambda(Seq(ValDef(id, tpe)), post)) =>
+ case Some(Lambda(Seq(ValDef(id)), post)) =>
if(fd.postcondition.exists { e => purescala.ExprOps.exists(_.isInstanceOf[Passes])(e) }) {
post match {
case TopLevelAnds(exprs) =>
@@ -39,7 +39,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
case _ => false
} }
if(i == -1) {
- fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), and(post, Passes(inputVariables, Variable(id), newCases))))
+ fd.postcondition = Some(Lambda(Seq(ValDef(id)), and(post, Passes(inputVariables, Variable(id), newCases))))
//ctx0.reporter.info("No top-level passes in postcondition, adding it: " + fd)
} else {
val newPasses = exprs(i) match {
@@ -48,21 +48,21 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
case _ => ???
}
val newPost = and(exprs.updated(i, newPasses) : _*)
- fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), newPost))
+ fd.postcondition = Some(Lambda(Seq(ValDef(id)), newPost))
//ctx0.reporter.info("Adding the example to the passes postcondition: " + fd)
}
}
} else {
- fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), and(post, Passes(inputVariables, Variable(id), newCases))))
+ fd.postcondition = Some(Lambda(Seq(ValDef(id)), and(post, Passes(inputVariables, Variable(id), newCases))))
//ctx0.reporter.info("No passes in postcondition, adding it:" + fd)
}
case None =>
val id = FreshIdentifier("res", fd.returnType, false)
- fd.postcondition = Some(Lambda(Seq(ValDef(id, false)), Passes(inputVariables, Variable(id), newCases)))
+ fd.postcondition = Some(Lambda(Seq(ValDef(id)), Passes(inputVariables, Variable(id), newCases)))
//ctx0.reporter.info("No postcondition, adding it: " + fd)
}
fd.body match { // TODO: Is it correct to discard the choose construct inside the body?
- case Some(Choose(Lambda(Seq(ValDef(id, tpe)), bodyChoose))) => fd.body = Some(Hole(id.getType, Nil))
+ case Some(Choose(Lambda(Seq(ValDef(id)), bodyChoose))) => fd.body = Some(Hole(id.getType, Nil))
case _ =>
}
}
@@ -76,4 +76,4 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
MatchCase(inPattern, None, out)
}
}
- }
\ No newline at end of file
+ }
diff --git a/src/main/scala/leon/transformations/IntToRealProgram.scala b/src/main/scala/leon/transformations/IntToRealProgram.scala
index 5ab169913..0c313f2ff 100644
--- a/src/main/scala/leon/transformations/IntToRealProgram.scala
+++ b/src/main/scala/leon/transformations/IntToRealProgram.scala
@@ -140,9 +140,9 @@ abstract class ProgramTypeTransformer {
// FIXME
//add a new postcondition
newfd.fullBody = if (fd.postcondition.isDefined && newfd.body.isDefined) {
- val Lambda(Seq(ValDef(resid, lzy)), pexpr) = fd.postcondition.get
+ val Lambda(Seq(ValDef(resid)), pexpr) = fd.postcondition.get
val tempRes = mapId(resid).toVariable
- Ensuring(newfd.body.get, Lambda(Seq(ValDef(tempRes.id, lzy)), transformExpr(pexpr)))
+ Ensuring(newfd.body.get, Lambda(Seq(ValDef(tempRes.id)), transformExpr(pexpr)))
// Some(mapId(resid), transformExpr(pexpr))
} else NoTree(fd.returnType)
diff --git a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
index c4830cf40..2e2e5c832 100644
--- a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
+++ b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
@@ -111,7 +111,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
def mapPost(pred: Expr, from: FunDef, to: FunDef) = {
pred match {
- case Lambda(Seq(ValDef(fromRes, lzy)), postCond) if (instFuncs.contains(from)) =>
+ case Lambda(Seq(ValDef(fromRes)), postCond) if (instFuncs.contains(from)) =>
val toResId = FreshIdentifier(fromRes.name, to.returnType, true)
val newpost = postMap((e: Expr) => e match {
case Variable(`fromRes`) =>
@@ -124,7 +124,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
case _ =>
None
})(postCond)
- Lambda(Seq(ValDef(toResId, lzy)), mapExpr(newpost))
+ Lambda(Seq(ValDef(toResId)), mapExpr(newpost))
case _ =>
mapExpr(pred)
}
--
GitLab