diff --git a/src/main/scala/leon/laziness/ClosurePreAsserter.scala b/src/main/scala/leon/laziness/ClosurePreAsserter.scala
index c0324fe7677c8007441bc65c4ed7ac3843f4b41a..a55cbbc00e7747835a9751e9c9140c1ebd761188 100644
--- a/src/main/scala/leon/laziness/ClosurePreAsserter.scala
+++ b/src/main/scala/leon/laziness/ClosurePreAsserter.scala
@@ -61,8 +61,12 @@ class ClosurePreAsserter(p: Program) {
case ((CaseClass(CaseClassType(ccd, _), argsRet), st), path) =>
anchorfd = Some(fd)
val target = lookupOp(ccd) //find the target corresponding to the closure
+
val pre = target.precondition.get
- val args = argsRet.dropRight(1) // drop the return value which is the right-most field
+ val args =
+ if (!isMemoized(target))
+ argsRet.dropRight(1) // drop the return value which is the right-most field
+ else argsRet
val nargs =
if (target.params.size > args.size) // target takes state ?
args :+ st
@@ -93,7 +97,7 @@ class ClosurePreAsserter(p: Program) {
val monoLemmas = {
var exprsProcessed = Set[ExprStructure]()
ccToOp.values.flatMap {
- case op if op.hasPrecondition =>
+ case op if op.hasPrecondition && !isMemoized(op) => // ignore memoized functions which are always evaluated at the time of creation
// get the state param
op.paramIds.find(isStateParam) match {
case Some(stparam) =>
@@ -122,7 +126,7 @@ class ClosurePreAsserter(p: Program) {
val fieldSelect = (id: Identifier) => CaseClassSelector(stType, id.toVariable, fld.id)
SubsetOf(fieldSelect(stparam), fieldSelect(superSt))
})
- // create a function for each pre-disjunct that is not processed
+ // create a function for each pre-disjunct that is not processed
preDisjs.map(new ExprStructure(_)).collect {
case preStruct if !exprsProcessed(preStruct) =>
exprsProcessed += preStruct
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index c8121446f28971e9e6a8ba5f63b52346fe941b53..88ef5bda269629ae924219647f4ba8ab1d4c923b 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -57,6 +57,9 @@ object LazinessEliminationPhase extends TransformationPhase {
// options that control behavior
val optRefEquality = LeonFlagOptionDef("refEq", "Uses reference equality for comparing closures", false)
+ /**
+ * TODO: add inlining annotations for optimization.
+ */
def apply(ctx: LeonContext, prog: Program): Program = {
if (dumpInputProg)
@@ -113,6 +116,7 @@ object LazinessEliminationPhase extends TransformationPhase {
}
/**
+ * TODO: enforce that lazy and nested types do not overlap
* TODO: we are forced to make an assumption that lazy ops takes as type parameters only those
* type parameters of their return type and not more. (This is checked in the closureFactory,\
* but may be check this upfront)
@@ -155,7 +159,16 @@ object LazinessEliminationPhase extends TransformationPhase {
if (nestedCheckFailed) {
failMsg = "Nested suspension creation in the body: " + fd.id
false
- } else true
+ } else {
+ // arguments or return types of memoized functions cannot be lazy because we do not know how to compare them for equality
+ if (isMemoized(fd)) {
+ val argCheckFailed = (fd.params.map(_.getType) :+ fd.returnType).exists(LazinessUtil.isLazyType)
+ if (argCheckFailed) {
+ failMsg = "Memoized function has a lazy argument or return type: " + fd.id
+ false
+ } else true
+ } else true
+ }
}
}
case _ => true
@@ -172,6 +185,11 @@ object LazinessEliminationPhase extends TransformationPhase {
"lazyarg" + globalId
}
+ /**
+ * (a) The functions lifts arguments of '$' to functions
+ * (b) lifts eager computations to lazy computations if necessary
+ * (c) converts memoization to lazy evaluation
+ */
def liftLazyExpressions(prog: Program): Program = {
var newfuns = Map[ExprStructure, (FunDef, ModuleDef)]()
val fdmap = prog.definedFunctions.collect {
@@ -180,43 +198,60 @@ object LazinessEliminationPhase extends TransformationPhase {
fd.flags.foreach(nfd.addFlag(_))
(fd -> nfd)
}.toMap
+
+ lazy val lazyFun = ProgramUtil.functionByFullName("leon.lazyeval.$.apply", prog).get
+ lazy val valueFun = ProgramUtil.functionByFullName("leon.lazyeval.$.value", prog).get
+
prog.modules.foreach { md =>
- md.definedFunctions.foreach {
- case fd if fd.hasBody && !fd.isLibrary =>
- val nbody = simplePostTransform {
- // is the arugment of lazy invocation not a function ?
- case finv @ FunctionInvocation(lazytfd, Seq(arg)) if isLazyInvocation(finv)(prog) && !arg.isInstanceOf[FunctionInvocation] =>
- val freevars = variablesOf(arg).toList
- val tparams = freevars.map(_.getType) flatMap getTypeParameters distinct
- val argstruc = new ExprStructure(arg)
- val argfun =
- if (newfuns.contains(argstruc)) {
- newfuns(argstruc)._1
- } else {
- //construct type parameters for the function
- // note: we should make the base type of arg as the return type
- val nfun = new FunDef(FreshIdentifier(freshFunctionNameForArg, Untyped, true), tparams map TypeParameterDef.apply,
- freevars.map(ValDef(_)), bestRealType(arg.getType))
- nfun.body = Some(arg)
- newfuns += (argstruc -> (nfun, md))
- nfun
- }
- FunctionInvocation(lazytfd, Seq(FunctionInvocation(TypedFunDef(argfun, tparams),
- freevars.map(_.toVariable))))
+ def exprLifter(inspec: Boolean)(expr: Expr) = expr match {
+ // is the arugment of lazy invocation not a function ?
+ case finv @ FunctionInvocation(lazytfd, Seq(arg)) if isLazyInvocation(finv)(prog) && !arg.isInstanceOf[FunctionInvocation] =>
+ val freevars = variablesOf(arg).toList
+ val tparams = freevars.map(_.getType).flatMap(getTypeParameters).distinct
+ val argstruc = new ExprStructure(arg)
+ val argfun =
+ if (newfuns.contains(argstruc)) {
+ newfuns(argstruc)._1
+ } else {
+ //construct type parameters for the function
+ // note: we should make the base type of arg as the return type
+ val nfun = new FunDef(FreshIdentifier(freshFunctionNameForArg, Untyped, true), tparams map TypeParameterDef.apply,
+ freevars.map(ValDef(_)), bestRealType(arg.getType))
+ nfun.body = Some(arg)
+ newfuns += (argstruc -> (nfun, md))
+ nfun
+ }
+ FunctionInvocation(lazytfd, Seq(FunctionInvocation(TypedFunDef(argfun, tparams),
+ freevars.map(_.toVariable))))
- // is the argument of eager invocation not a variable ?
- case finv @ FunctionInvocation(TypedFunDef(fd, _), Seq(arg)) if isEagerInvocation(finv)(prog) && !arg.isInstanceOf[Variable] =>
- val rootType = bestRealType(arg.getType)
- val freshid = FreshIdentifier("t", rootType)
- Let(freshid, arg, FunctionInvocation(TypedFunDef(fd, Seq(rootType)), Seq(freshid.toVariable)))
+ // is the argument of eager invocation not a variable ?
+ case finv @ FunctionInvocation(TypedFunDef(fd, _), Seq(arg)) if isEagerInvocation(finv)(prog) && !arg.isInstanceOf[Variable] =>
+ val rootType = bestRealType(arg.getType)
+ val freshid = FreshIdentifier("t", rootType)
+ Let(freshid, arg, FunctionInvocation(TypedFunDef(fd, Seq(rootType)), Seq(freshid.toVariable)))
- case FunctionInvocation(TypedFunDef(fd, targs), args) if fdmap.contains(fd) =>
- FunctionInvocation(TypedFunDef(fdmap(fd), targs), args)
- case e => e
+ case FunctionInvocation(TypedFunDef(fd, targs), args) if isMemoized(fd) && !inspec =>
+ // calling a memoized function is modeled as creating a lazy closure and forcing it
+ val tfd = TypedFunDef(fdmap.getOrElse(fd, fd), targs)
+ val finv = FunctionInvocation(tfd, args)
+ // enclose the call within the $ and force it
+ val susp = FunctionInvocation(TypedFunDef(lazyFun, Seq(tfd.returnType)), Seq(finv))
+ FunctionInvocation(TypedFunDef(valueFun, Seq(tfd.returnType)), Seq(susp))
- }(fd.fullBody) // TODO: specs should not create lazy closures. enforce this
+ case FunctionInvocation(TypedFunDef(fd, targs), args) if fdmap.contains(fd) =>
+ FunctionInvocation(TypedFunDef(fdmap(fd), targs), args)
+ case e => e
+ }
+ md.definedFunctions.foreach {
+ case fd if fd.hasBody && !fd.isLibrary =>
+ val nbody = simplePostTransform(exprLifter(false))(fd.body.get)
+ val npre = fd.precondition.map(simplePostTransform(exprLifter(true)))
+ val npost = fd.postcondition.map(simplePostTransform(exprLifter(true)))
//println(s"New body of $fd: $nbody")
- fdmap(fd).fullBody = nbody
+ val nfd = fdmap(fd)
+ nfd.body = Some(nbody)
+ nfd.precondition = npre
+ nfd.postcondition = npost
case _ => ;
}
}
diff --git a/src/main/scala/leon/laziness/LazyClosureConverter.scala b/src/main/scala/leon/laziness/LazyClosureConverter.scala
index b30eca6874241456b9cad3114e647a8f3d05edcd..c86ec021f87ccfb08a2a3a41b95ddfe2fe69dbb1 100644
--- a/src/main/scala/leon/laziness/LazyClosureConverter.scala
+++ b/src/main/scala/leon/laziness/LazyClosureConverter.scala
@@ -49,7 +49,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val consCallers = funsManager.callersOfLazyCons // transitive constructors of closures
val starCallers = funsManager.funsNeedStateTps
val fvFactory = new FreeVariableFactory()
- val tnames = closureFactory.lazyTypeNames
+ val lazyTnames = closureFactory.lazyTypeNames
val lazyops = closureFactory.lazyops
val funMap = p.definedFunctions.collect {
@@ -178,7 +178,8 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
* Note that by using 'assume-pre' we can also assume the preconditions of closures at
* the call-sites.
*/
- val evalFunctions = tnames.map { tname =>
+ val evalFunctions = lazyTnames.map { tname =>
+ val ismem = closureFactory.isMemType(tname)
val tpe = /*freshenTypeArguments(*/ closureFactory.lazyType(tname) //)
val absdef = closureFactory.absClosureType(tname)
val cdefs = closureFactory.closures(tname)
@@ -204,8 +205,11 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val binder = FreshIdentifier("t", ctype)
val pattern = InstanceOfPattern(Some(binder), ctype)
// create a body of the match
- // the last field represents the result
- val args = cdef.fields.dropRight(1) map { fld =>
+ // the last field represents the result (only if the type is a susp type)
+ val flds =
+ if (!ismem) cdef.fields.dropRight(1)
+ else cdef.fields
+ val args = flds map { fld =>
CaseClassSelector(ctype, binder.toVariable, fld.id)
}
val op = closureFactory.caseClassToOp(cdef)
@@ -231,17 +235,18 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val rhs = Let(invokeRes, invoke, Tuple(Seq(valPart, stPart)))
MatchCase(pattern, None, rhs)
}
- // create a new match case for eager evaluation
- val eagerCase = {
- val eagerDef = closureFactory.eagerClosure(tname)
+ val cases = if (!ismem) {
+ // create a new match case for eager evaluation
+ val eagerDef = closureFactory.eagerClosure(tname).get
val ctype = CaseClassType(eagerDef, recvTparams)
val binder = FreshIdentifier("t", ctype)
// create a body of the match
val valPart = CaseClassSelector(ctype, binder.toVariable, eagerDef.fields(0).id)
val rhs = Tuple(Seq(valPart, param2.toVariable)) // state doesn't change for eager closure
- MatchCase(InstanceOfPattern(Some(binder), ctype), None, rhs)
- }
- dfun.body = Some(MatchExpr(param1.toVariable, eagerCase +: bodyMatchCases))
+ MatchCase(InstanceOfPattern(Some(binder), ctype), None, rhs) +: bodyMatchCases
+ } else
+ bodyMatchCases
+ dfun.body = Some(MatchExpr(param1.toVariable, cases))
dfun.addFlag(Annotation("axiom", Seq()))
(tname -> dfun)
}.toMap
@@ -272,7 +277,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
* They are defined for each lazy class since it avoids generics and
* simplifies the type inference (which is not full-fledged in Leon)
*/
- val closureCons = tnames.map { tname =>
+ val closureCons = lazyTnames.map { tname =>
val adt = closureFactory.absClosureType(tname)
val param1Type = AbstractClassType(adt, adt.tparams.map(_.tp))
val param1 = FreshIdentifier("cc", param1Type)
@@ -283,7 +288,6 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val fun = new FunDef(FreshIdentifier(closureConsName(tname)), tparamdefs,
Seq(ValDef(param1), ValDef(param2)), param1Type)
fun.body = Some(param1.toVariable)
-
// assert that the closure in unevaluated if useRefEquality is enabled
// not supported as of now
/*if (refEq) {
@@ -295,21 +299,25 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
(tname -> fun)
}.toMap
- def mapBody(body: Expr)(implicit stTparams: Seq[TypeParameter]): (Option[Expr] => Expr, Boolean) = body match {
+ def mapExpr(expr: Expr)(implicit stTparams: Seq[TypeParameter], inSpec: Boolean): (Option[Expr] => Expr, Boolean) = expr match {
case finv @ FunctionInvocation(_, Seq(FunctionInvocation(TypedFunDef(argfd, tparams), args))) // lazy construction ?
- if isLazyInvocation(finv)(p) =>
+ if isLazyInvocation(finv)(p) && !inSpec =>
val op = (nargs: Seq[Expr]) => ((st: Option[Expr]) => {
val adt = closureFactory.closureOfLazyOp(argfd)
// create lets to bind the nargs to variables
- val (flatArgs, letCons) = nargs.foldRight((Seq[Variable](), (e : Expr) => e)){
+ val (flatArgs, letCons) = nargs.foldRight((Seq[Variable](), (e: Expr) => e)) {
case (narg, (fargs, lcons)) =>
val id = FreshIdentifier("a", narg.getType, true)
(id.toVariable +: fargs, e => Let(id, narg, lcons(e)))
}
- // construct a value for the result (an uninterpreted function)
- val resval = FunctionInvocation(TypedFunDef(uiFuncs(argfd)._1, tparams), flatArgs)
- val cc = CaseClass(CaseClassType(adt, tparams), flatArgs :+ resval)
+ val ccArgs = if (!isMemoized(argfd)) {
+ // construct a value for the result (an uninterpreted function)
+ val resval = FunctionInvocation(TypedFunDef(uiFuncs(argfd)._1, tparams), flatArgs)
+ flatArgs :+ resval
+ } else
+ flatArgs
+ val cc = CaseClass(CaseClassType(adt, tparams), ccArgs)
val baseLazyTypeName = closureFactory.lazyTypeNameOfClosure(adt)
val fi = FunctionInvocation(TypedFunDef(closureCons(baseLazyTypeName), tparams ++ stTparams),
Seq(cc, st.get))
@@ -317,13 +325,29 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
}, false)
mapNAryOperator(args, op)
+ // TODO: we don't have to create a dummy return value for memoized functions, as they wouldn't be stored in other structures
+ case finv @ FunctionInvocation(_, Seq(FunctionInvocation(TypedFunDef(argfd, tparams), args))) // invocation in spec ?
+ if isLazyInvocation(finv)(p) && inSpec =>
+ // in this case argfd is a memoized function
+ val op = (nargs: Seq[Expr]) => ((st: Option[Expr]) => {
+ val adt = closureFactory.closureOfLazyOp(argfd)
+ /*// create lets to bind the nargs to variables
+ val (flatArgs, letCons) = nargs.foldRight((Seq[Variable](), (e : Expr) => e)){
+ case (narg, (fargs, lcons)) =>
+ val id = FreshIdentifier("a", narg.getType, true)
+ (id.toVariable +: fargs, e => Let(id, narg, lcons(e)))
+ }*/
+ CaseClass(CaseClassType(adt, tparams), nargs)
+ }, false)
+ mapNAryOperator(args, op)
+
case finv @ FunctionInvocation(_, Seq(arg)) if isEagerInvocation(finv)(p) =>
// here arg is guaranteed to be a variable
((st: Option[Expr]) => {
val rootType = bestRealType(arg.getType)
val tname = typeNameWOParams(rootType)
val tparams = getTypeArguments(rootType)
- val eagerClosure = closureFactory.eagerClosure(tname)
+ val eagerClosure = closureFactory.eagerClosure(tname).get
CaseClass(CaseClassType(eagerClosure, tparams), Seq(arg))
}, false)
@@ -336,9 +360,13 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val stType = CaseClassType(closureFactory.state, stTparams)
val cls = closureFactory.selectFieldOfState(tname, st, stType)
val memberTest = ElementOfSet(narg, cls)
- val subtypeTest = IsInstanceOf(narg,
- CaseClassType(closureFactory.eagerClosure(tname), getTypeArguments(baseType)))
- Or(memberTest, subtypeTest)
+ if(closureFactory.isMemType(tname)) {
+ memberTest
+ } else {
+ val subtypeTest = IsInstanceOf(narg,
+ CaseClassType(closureFactory.eagerClosure(tname).get, getTypeArguments(baseType)))
+ Or(memberTest, subtypeTest)
+ }
}, false)
mapNAryOperator(args, op)
@@ -366,8 +394,8 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
throw new IllegalStateException("The arguments to `withState` should equal the number of states: "+numStates)
val CaseClass(_, Seq(exprNeedingState)) = recvr
- val (nexprCons, exprReturnsState) = mapBody(exprNeedingState)
- val nstConses = stArgs map mapBody
+ val (nexprCons, exprReturnsState) = mapExpr(exprNeedingState)
+ val nstConses = stArgs map mapExpr
if(nstConses.exists(_._2)) // any 'stArg' returning state
throw new IllegalStateException("One of the arguments to `withState` returns a new state, which is not supported: "+finv)
else {
@@ -398,13 +426,6 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val dispFun = evalFunctions(tname)
val tparams = (getTypeParameters(baseType) ++ stTparams).distinct
FunctionInvocation(TypedFunDef(dispFun, tparams), nargs :+ st)
- //val dispRes = FreshIdentifier("dres", dispFun.returnType, true)
- /*val nstates = tnames map {
- case `tname` =>
- TupleSelect(dispRes.toVariable, 2)
- case other => st(other)
- }*/
- //Let(dispRes, dispFunInv, Tuple(TupleSelect(dispRes.toVariable, 1) +: nstates))
}, true)
mapNAryOperator(args, op)
@@ -433,14 +454,13 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
}, funsRetStates(fd)))
case Let(id, value, body) =>
- val (valCons, valUpdatesState) = mapBody(value)
- val (bodyCons, bodyUpdatesState) = mapBody(body)
+ val (valCons, valUpdatesState) = mapExpr(value)
+ val (bodyCons, bodyUpdatesState) = mapExpr(body)
((st: Option[Expr]) => {
val nval = valCons(st)
if (valUpdatesState) {
val freshid = FreshIdentifier(id.name, nval.getType, true)
val nextState = TupleSelect(freshid.toVariable, 2)
- //val nsMap = (tnames zip nextStates).toMap
val transBody = replace(Map(id.toVariable -> TupleSelect(freshid.toVariable, 1)),
bodyCons(Some(nextState)))
if (bodyUpdatesState)
@@ -452,9 +472,9 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
}, valUpdatesState || bodyUpdatesState)
case IfExpr(cond, thn, elze) =>
- val (condCons, condState) = mapBody(cond)
- val (thnCons, thnState) = mapBody(thn)
- val (elzeCons, elzeState) = mapBody(elze)
+ val (condCons, condState) = mapExpr(cond)
+ val (thnCons, thnState) = mapExpr(thn)
+ val (elzeCons, elzeState) = mapExpr(elze)
((st: Option[Expr]) => {
val (ncondCons, nst) =
if (condState) {
@@ -479,10 +499,10 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
}, condState || thnState || elzeState)
case MatchExpr(scr, cases) =>
- val (scrCons, scrUpdatesState) = mapBody(scr)
+ val (scrCons, scrUpdatesState) = mapExpr(scr)
val casesRes = cases.foldLeft(Seq[(Option[Expr] => Expr, Boolean)]()) {
case (acc, MatchCase(pat, None, rhs)) =>
- acc :+ mapBody(rhs)
+ acc :+ mapExpr(rhs)
case mcase =>
throw new IllegalStateException("Match case with guards are not supported yet: " + mcase)
}
@@ -525,12 +545,12 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
case t: Terminal => (_ => t, false)
}
- def mapNAryOperator(args: Seq[Expr], op: Seq[Expr] => (Option[Expr] => Expr, Boolean))(implicit stTparams: Seq[TypeParameter]) = {
+ def mapNAryOperator(args: Seq[Expr], op: Seq[Expr] => (Option[Expr] => Expr, Boolean))(implicit stTparams: Seq[TypeParameter], inSpec: Boolean) = {
// create n variables to model n lets
val letvars = args.map(arg => FreshIdentifier("arg", arg.getType, true).toVariable)
(args zip letvars).foldRight(op(letvars)) {
case ((arg, letvar), (accCons, stUpdatedBefore)) =>
- val (argCons, stUpdateFlag) = mapBody(arg)
+ val (argCons, stUpdateFlag) = mapExpr(arg)
val cl = if (!stUpdateFlag) {
// here arg does not affect the newstate
(st: Option[Expr]) => replace(Map(letvar -> argCons(st)), accCons(st))
@@ -541,13 +561,6 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val narg = argCons(st)
val argres = FreshIdentifier("a", narg.getType, true).toVariable
val nstate = Some(TupleSelect(argres, 2))
- /*val nstateSeq = tnames.zipWithIndex.map {
- // states start from index 2
- case (tn, i) => TupleSelect(argres, i + 2)
- }
- val nstate = (tnames zip nstateSeq).map {
- case (tn, st) => (tn -> st)
- }.toMap[String, Expr]*/
val letbody =
if (stUpdatedBefore) accCons(nstate) // here, 'acc' already returns a superseeding state
else Tuple(Seq(accCons(nstate), nstate.get)) // here, 'acc; only returns the result
@@ -568,7 +581,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
def assignBodiesToFunctions = funMap foreach {
case (fd, nfd) =>
//println("Considering function: "+fd)
- // Here, using name to identify 'state' parameters
+ // Here, using name to identify 'state' parameters
val stateParam = nfd.params.collectFirst {
case vd if isStateParam(vd.id) =>
vd.id.toVariable
@@ -578,7 +591,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val stTparams = nfd.tparams.collect{
case tpd if isPlaceHolderTParam(tpd.tp) => tpd.tp
}
- val (nbodyFun, bodyUpdatesState) = mapBody(fd.body.get)(stTparams)
+ val (nbodyFun, bodyUpdatesState) = mapExpr(fd.body.get)(stTparams, false)
val nbody = nbodyFun(stateParam)
val bodyWithState =
if (!bodyUpdatesState && funsRetStates(fd))
@@ -593,7 +606,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
// This guarantees their observational purity/transparency
// collect class invariants that need to be added
if (fd.hasPrecondition) {
- val (npreFun, preUpdatesState) = mapBody(fd.precondition.get)(stTparams)
+ val (npreFun, preUpdatesState) = mapExpr(fd.precondition.get)(stTparams, true)
nfd.precondition =
if (preUpdatesState)
Some(TupleSelect(npreFun(stateParam), 1)) // ignore state updated by pre
@@ -657,7 +670,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
case e => e
}(post)
// thread state through postcondition
- val (npostFun, postUpdatesState) = mapBody(tpost)(stTparams)
+ val (npostFun, postUpdatesState) = mapExpr(tpost)(stTparams, true)
val resval =
if (bodyUpdatesState || funsRetStates(fd))
TupleSelect(newres.toVariable, 1)
@@ -678,6 +691,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
def assignContractsForEvals = evalFunctions.foreach {
case (tname, evalfd) =>
+ val ismem = closureFactory.isMemType(tname)
val cdefs = closureFactory.closures(tname)
val recvTparams = getTypeParameters(evalfd.params.head.getType)
val postres = FreshIdentifier("res", evalfd.returnType)
@@ -689,12 +703,18 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val binder = FreshIdentifier("t", ctype)
val pattern = InstanceOfPattern(Some(binder), ctype)
// t.clres == res._1
- val clresField = cdef.fields.last
- val clause1 = Equals(TupleSelect(postres.toVariable, 1),
- CaseClassSelector(ctype, binder.toVariable, clresField.id))
+ val clause1 = if(ismem) {
+ val clresField = cdef.fields.last
+ Equals(TupleSelect(postres.toVariable, 1),
+ CaseClassSelector(ctype, binder.toVariable, clresField.id))
+ } else
+ Util.tru
//res._1 == uifun(args)
val clause2 = if (takesStateButIndep(op)) {
- val args = cdef.fields.dropRight(1) map {
+ val flds =
+ if (!ismem) cdef.fields.dropRight(1)
+ else cdef.fields
+ val args = flds map {
fld => CaseClassSelector(ctype, binder.toVariable, fld.id)
}
Some(Equals(TupleSelect(postres.toVariable, 1),
diff --git a/src/main/scala/leon/laziness/LazyClosureFactory.scala b/src/main/scala/leon/laziness/LazyClosureFactory.scala
index 91a33252161cad2187f75ab24086d039aa9c2aaf..49151ed151946c50fc984aefc834672d9a6f410b 100644
--- a/src/main/scala/leon/laziness/LazyClosureFactory.scala
+++ b/src/main/scala/leon/laziness/LazyClosureFactory.scala
@@ -32,39 +32,49 @@ import LazinessUtil._
class LazyClosureFactory(p: Program) {
val debug = false
implicit val prog = p
+
+ /**
+ * all the operations that could be lazily evaluated
+ */
+ val lazyopsList = p.definedFunctions.flatMap {
+ case fd if (fd.hasBody) =>
+ filter(isLazyInvocation)(fd.body.get) map {
+ case FunctionInvocation(_, Seq(FunctionInvocation(tfd, _))) => tfd.fd
+ }
+ case _ => Seq()
+ }.distinct
+
+ if (debug) {
+ println("Lazy operations found: \n" + lazyopsList.map(_.id).mkString("\n"))
+ }
+
/**
- * Create a mapping from types to the lazyops that may produce a value of that type
+ * Create a mapping from types to the lazy/mem ops that may produce a value of that type
* TODO: relax the requirement that type parameters of return type of a function
- * lazy evaluated should include all of its type parameters
+ * lazy evaluated/memoized should include all of its type parameters.
*/
- private val (tpeToADT, opToCaseClass) = {
- // collect all the operations that could be lazily evaluated.
- val lazyops = p.definedFunctions.flatMap {
- case fd if (fd.hasBody) =>
- filter(isLazyInvocation)(fd.body.get) map {
- case FunctionInvocation(_, Seq(FunctionInvocation(tfd, _))) => tfd.fd
- }
- case _ => Seq()
- }.distinct
- if (debug) {
- println("Lazy operations found: \n" + lazyops.map(_.id).mkString("\n"))
- }
+ private def closuresForOps(ops: List[FunDef]) = {
// using tpe name below to avoid mismatches due to type parameters
- val tpeToLazyops = lazyops.groupBy(lops => typeNameWOParams(lops.returnType))
- if(debug) {
- println("Type to lazy ops: "+tpeToLazyops.map{
- case (k,v) => s"$k --> ${v.map(_.id).mkString(",")}" }.mkString("\n"))
+ val tpeToLazyops = ops.groupBy(lop => typeNameWOParams(lop.returnType))
+ if (debug) {
+ println("Type to Ops: " + tpeToLazyops.map {
+ case (k, v) => s"$k --> ${v.map(_.id).mkString(",")}"
+ }.mkString("\n"))
}
val tpeToAbsClass = tpeToLazyops.map {
case (tpename, ops) =>
val tpcount = getTypeParameters(ops(0).returnType).size
- // check that tparams of all ops should match and should be equal to the tparams of return type
- // a safety check
+ //Safety check:
+ // (a) check that tparams of all ops should match and should be equal to the tparams of return type
+ // (b) all are either memoized or all are lazy
ops.foreach { op =>
if (op.tparams.size != tpcount)
- throw new IllegalStateException(s"Type parameters of the lazy operation ${op.id.name}" +
+ throw new IllegalStateException(s"Type parameters of the lazy/memoized operation ${op.id.name}" +
"should match the type parameters of the return type of the operation")
}
+ if(ops.size >= 2) {
+ ops.tail.forall(op => isMemoized(op) == isMemoized(ops.head))
+ }
val absTParams = (1 to tpcount).map(i => TypeParameterDef(TypeParameter.fresh("T" + i)))
tpename -> AbstractClassDef(FreshIdentifier(typeNameToADTName(tpename), Untyped),
absTParams, None)
@@ -72,6 +82,7 @@ class LazyClosureFactory(p: Program) {
var opToAdt = Map[FunDef, CaseClassDef]()
val tpeToADT = tpeToLazyops map {
case (tpename, ops) =>
+ val ismem = isMemoized(ops(0))
val baseT = ops(0).returnType //TODO: replace targs here i.e, use clresType ?
val absClass = tpeToAbsClass(tpename)
val absTParamsDef = absClass.tparams
@@ -92,26 +103,32 @@ class LazyClosureFactory(p: Program) {
val btname = typeNameWOParams(btype)
val baseAbs = tpeToAbsClass(btname)
ValDef(FreshIdentifier(vd.id.name,
- AbstractClassType(baseAbs, getTypeParameters(btype))))
+ AbstractClassType(baseAbs, getTypeParameters(btype))))
}
}
- // add a result field as well
- val resField = ValDef(FreshIdentifier("clres", opfd.returnType))
- cdef.setFields(nfields :+ resField)
+ if (!ismem) {
+ // add a result field as well
+ val resField = ValDef(FreshIdentifier("clres", opfd.returnType))
+ cdef.setFields(nfields :+ resField)
+ } else
+ cdef.setFields(nfields)
absClass.registerChild(cdef)
opToAdt += (opfd -> cdef)
cdef
}
- // create a case class to represent eager evaluation
- val clresType = ops(0).returnType match {
- case NAryType(tparams, tcons) => tcons(absTParams)
- }
- val eagerid = FreshIdentifier("Eager"+TypeUtil.typeNameWOParams(clresType))
- val eagerClosure = CaseClassDef(eagerid, absTParamsDef,
+ if (!ismem) {
+ // create a case class to represent eager evaluation (when handling lazy ops)
+ val clresType = ops(0).returnType match {
+ case NAryType(tparams, tcons) => tcons(absTParams)
+ }
+ val eagerid = FreshIdentifier("Eager" + TypeUtil.typeNameWOParams(clresType))
+ val eagerClosure = CaseClassDef(eagerid, absTParamsDef,
Some(AbstractClassType(absClass, absTParams)), isCaseObject = false)
- eagerClosure.setFields(Seq(ValDef(FreshIdentifier("a", clresType))))
- absClass.registerChild(eagerClosure)
- (tpename -> (baseT, absClass, cdefs, eagerClosure))
+ eagerClosure.setFields(Seq(ValDef(FreshIdentifier("a", clresType))))
+ absClass.registerChild(eagerClosure)
+ (tpename -> (baseT, absClass, cdefs, Some(eagerClosure), ismem))
+ } else
+ (tpename -> (baseT, absClass, cdefs, None, ismem))
}
/*tpeToADT.foreach {
case (k, v) => println(s"$k --> ${ (v._2 +: v._3).mkString("\n\t") }")
@@ -119,38 +136,31 @@ class LazyClosureFactory(p: Program) {
(tpeToADT, opToAdt)
}
+ private val (tpeToADT, opToCaseClass) = closuresForOps(lazyopsList)
+
// this fixes an ordering on lazy types
val lazyTypeNames = tpeToADT.keys.toSeq
-
val lazyops = opToCaseClass.keySet
-
- val allClosuresAndParents : Seq[ClassDef] = tpeToADT.values.flatMap(v => v._2 +: v._3 :+ v._4).toSeq
-
+ lazy val caseClassToOp = opToCaseClass map { case (k, v) => v -> k }
+ val allClosuresAndParents: Seq[ClassDef] = tpeToADT.values.flatMap(v => (v._2 +: v._3) ++ v._4.toList).toSeq
val allClosureSet = allClosuresAndParents.toSet
+ // lazy operations
def lazyType(tn: String) = tpeToADT(tn)._1
-
+ def isMemType(tn: String) = tpeToADT(tn)._5
def absClosureType(tn: String) = tpeToADT(tn)._2
-
def closures(tn: String) = tpeToADT(tn)._3
-
def eagerClosure(tn: String) = tpeToADT(tn)._4
-
- lazy val caseClassToOp = opToCaseClass map { case (k, v) => v -> k }
-
def lazyopOfClosure(cl: CaseClassDef) = caseClassToOp(cl)
-
def closureOfLazyOp(op: FunDef) = opToCaseClass(op)
-
def isLazyOp(op: FunDef) = opToCaseClass.contains(op)
-
def isClosureType(cd: ClassDef) = allClosureSet.contains(cd)
/**
* Here, the lazy type name is recovered from the closure's name.
* This avoids the use of additional maps.
*/
- def lazyTypeNameOfClosure(cl: CaseClassDef) = adtNameToTypeName(cl.parent.get.classDef.id.name)
+ def lazyTypeNameOfClosure(cl: CaseClassDef) = adtNameToTypeName(cl.parent.get.classDef.id.name)
/**
* Define a state as an ADT whose fields are sets of closures.
@@ -162,7 +172,7 @@ class LazyClosureFactory(p: Program) {
def freshTParams(n: Int): Seq[TypeParameter] = {
val start = i + 1
i += n // create 'n' fresh ids
- val nparams = (start to i).map(index => TypeParameter.fresh("T"+index))
+ val nparams = (start to i).map(index => TypeParameter.fresh("T" + index))
tparams ++= nparams
nparams
}
@@ -180,7 +190,7 @@ class LazyClosureFactory(p: Program) {
def selectFieldOfState(tn: String, st: Expr, stType: CaseClassType) = {
val selName = typeToFieldName(tn)
- stType.classDef.fields.find{ fld => fld.id.name == selName} match {
+ stType.classDef.fields.find { fld => fld.id.name == selName } match {
case Some(fld) =>
CaseClassSelector(stType, st, fld.id)
case _ =>
@@ -188,22 +198,22 @@ class LazyClosureFactory(p: Program) {
}
}
- val stateUpdateFuns : Map[String, FunDef] =
- lazyTypeNames.map{ tn =>
+ val stateUpdateFuns: Map[String, FunDef] =
+ lazyTypeNames.map { tn =>
val fldname = typeToFieldName(tn)
val tparams = state.tparams.map(_.tp)
val stType = CaseClassType(state, tparams)
val param1 = FreshIdentifier("st@", stType)
- val SetType(baseT) = stType.classDef.fields.find{ fld => fld.id.name == fldname}.get.getType
+ val SetType(baseT) = stType.classDef.fields.find { fld => fld.id.name == fldname }.get.getType
val param2 = FreshIdentifier("cl", baseT)
// TODO: as an optimization we can mark all these functions as inline and inline them at their callees
- val updateFun = new FunDef(FreshIdentifier("updState"+tn),
- state.tparams, Seq(ValDef(param1), ValDef(param2)), stType)
+ val updateFun = new FunDef(FreshIdentifier("updState" + tn),
+ state.tparams, Seq(ValDef(param1), ValDef(param2)), stType)
// create a body for the updateFun:
- val nargs = state.fields.map{ fld =>
+ val nargs = state.fields.map { fld =>
val fldSelect = CaseClassSelector(stType, param1.toVariable, fld.id)
- if(fld.id.name == fldname) {
+ if (fld.id.name == fldname) {
SetUnion(fldSelect, FiniteSet(Set(param2.toVariable), baseT)) // st@.tn + Set(param2)
} else {
fldSelect
diff --git a/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala b/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala
index 385c1498feb848fe4905eea2b859142c572fc009..786c392b6f1f87410025fb25d63c048ea50934a9 100644
--- a/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala
+++ b/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala
@@ -4,28 +4,25 @@ import leon.lazyeval._
import leon.lang._
import leon.annotation._
import leon.instrumentation._
-import scala.math.BigInt.int2bigInt
//import leon.invariant._
object FibMem {
-
- /**
- * A simple non-lazy list of integers
- */
sealed abstract class IList
case class Cons(x: BigInt, tail: IList) extends IList
case class Nil() extends IList
+ @memoize
def fibRec(n: BigInt): BigInt = {
- require(n <= 2 || ($(fibRec(n-1)).isEvaluated && // previous two values have been evaluated
- $(fibRec(n-2)).isEvaluated))
+ require(n >= 0)
if(n <= 2)
BigInt(1)
else
- fibRec(n-1) + fibRec(n-2)
- } ensuring(_ => time <= 50)
+ fibRec(n-1) + fibRec(n-2) // postcondition implies that the second call would be cached
+ } ensuring(_ =>
+ (n <= 2 || ($(fibRec(n-1)).isEvaluated &&
+ $(fibRec(n-2)).isEvaluated)) && time <= 40*n + 10)
- def fibRange(i: BigInt, k: BigInt): IList = {
+ /*def fibRange(i: BigInt, k: BigInt): IList = {
require(k >= 1 && i <= k &&
(i <= 1 ||
(($(fibRec(i-1)).isEvaluated) &&
@@ -33,7 +30,7 @@ object FibMem {
if(i == k)
Cons(fibRec(i), Nil())
else {
- val x = $(fibRec(i)).value
+ val x = fibRec(i)
Cons(x, fibRange(i + 1, k))
}
} ensuring(_ => time <= (k - i + 1) * 60)
@@ -41,5 +38,5 @@ object FibMem {
def kfibs(k: BigInt) = {
require(k >= 1)
fibRange(1, k)
- } ensuring(_ => time <= 70 * k)
+ } ensuring(_ => time <= 70 * k)*/
}