diff --git a/leon.out/Conqueue-strategy2.scala b/leon.out/Conqueue-strategy2.scala
deleted file mode 100644
index 2cadbadd3b288637c2d20223d92033ee577b1a15..0000000000000000000000000000000000000000
--- a/leon.out/Conqueue-strategy2.scala
+++ /dev/null
@@ -1,633 +0,0 @@
-package lazybenchmarks
-import leon.lazyeval._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.lang.synthesis._
-import ConcTrees._
-import ConQ._
-import Conqueue._
-
-object ConcTrees {
- abstract class Conc[T] {
- def isEmpty: Boolean = this == Empty[T]()
-
- def level: BigInt = {
- this match {
- case Empty() =>
- BigInt(0)
- case Single(x) =>
- BigInt(0)
- case CC(l, r) =>
- BigInt(1) + max(l.level, r.level)
- }
- } ensuring {
- (x$1: BigInt) => x$1 >= BigInt(0)
- }
- }
-
- case class Empty[T]() extends Conc[T]
-
- case class Single[T](x: T) extends Conc[T]
-
- case class CC[T](left: Conc[T], right: Conc[T]) extends Conc[T]
-
- def max(x: BigInt, y: BigInt): BigInt = if (x >= y) {
- x
- } else {
- y
- }
-
- def abs(x: BigInt): BigInt = if (x < BigInt(0)) {
- -x
- } else {
- x
- }
-}
-
-object Conqueue {
- abstract class ConQ[T] {
- def isSpine: Boolean = this match {
- case Spine(_, _, _) =>
- true
- case _ =>
- false
- }
- def isTip: Boolean = !this.isSpine
- }
-
- case class Tip[T](t: Conc[T]) extends ConQ[T]
-
- case class Spine[T](head: Conc[T], createdWithSusp: Bool, rear: LazyConQ[T]) extends ConQ[T]
-
- sealed abstract class Bool
- case class True() extends Bool
- case class False() extends Bool
-
- abstract class Scheds[T]
-
- case class Cons[T](h: LazyConQ[T], tail: Scheds[T]) extends Scheds[T]
-
- case class Nil[T]() extends Scheds[T]
-
- case class Wrapper[T](queue: LazyConQ[T], schedule: Scheds[T]) {
- def valid(st: Set[LazyConQ[T]]): Boolean = zeroPreceedsLazy[T](this.queue, st) &&
- // schedulesProperty(this.queue, this.schedule, st)
- strongSchedsProp(this.queue, this.schedule, st)
- }
-
- def zeroPreceedsLazy[T](q: LazyConQ[T], st: Set[LazyConQ[T]]): Boolean = {
- if (isEvaluated(q, st)) {
- evalLazyConQS[T](q) match {
- case Spine(Empty(), _, rear) => true
- case Spine(_, _, rear) =>
- zeroPreceedsLazy[T](rear, st)
- case Tip(_) => true
- }
- } else false
- }
-
- // not used, but still interesting
- def zeroPredLazyMonotone[T](st1: Set[LazyConQ[T]], st2: Set[LazyConQ[T]], q: LazyConQ[T]): Boolean = {
- require(st1.subsetOf(st2) && zeroPreceedsLazy(q, st1))
- zeroPreceedsLazy(q, st2) &&
- //induction scheme
- (evalLazyConQS[T](q) match {
- case Spine(Empty(), _, _) =>
- true
- case Spine(h, _, rear) =>
- zeroPredLazyMonotone(st1, st2, rear)
- case Tip(_) =>
- true
- })
- } holds
-
- def weakZeroPreceedsLazy[T](q: LazyConQ[T], st: Set[LazyConQ[T]]): Boolean = {
- evalLazyConQS[T](q) match {
- case Spine(Empty(), _, rear10) =>
- true
- case Spine(h, _, rear11) =>
- zeroPreceedsLazy[T](rear11, st)
- case Tip(_) =>
- true
- }
- }
-
- def firstUnevaluated[T](l: LazyConQ[T], st: Set[LazyConQ[T]]): LazyConQ[T] = {
- if (isEvaluated(l, st)) {
- evalLazyConQS[T](l) match {
- case Spine(_, _, tail15) =>
- firstUnevaluated[T](tail15, st)
- case _ =>
- l
- }
- } else {
- l
- }
- } ensuring {
- (res65: LazyConQ[T]) =>
- (evalLazyConQS[T](res65).isTip || !st.contains(res65)) &&
- concreteUntil(l, res65, st)
- }
-
- def nextUnevaluatedLemma[T](l: LazyConQ[T], st: Set[LazyConQ[T]]): Boolean = {
- val (res, nst) = evalLazyConQ[T](firstUnevaluated(l, st), st)
- (res match {
- case Spine(_, _, tail) =>
- firstUnevaluated[T](l, nst) == firstUnevaluated[T](tail, nst)
- case _ =>
- true
- }) &&
- // induction scheme
- (evalLazyConQS[T](l) match {
- case Spine(_, _, tail) =>
- nextUnevaluatedLemma(tail, st)
- case _ => true
- })
- } holds
-
- /**
- * Everything until suf is evaluated
- */
- def concreteUntil[T](l: LazyConQ[T], suf: LazyConQ[T], st: Set[LazyConQ[T]]): Boolean = {
- if (l != suf) {
- isEvaluated(l, st) && (evalLazyConQS[T](l) match {
- case Spine(_, cws, tail15) =>
- concreteUntil(tail15, suf, st)
- case _ =>
- true
- })
- } else true
- }
-
- def isConcrete[T](l: LazyConQ[T], st: Set[LazyConQ[T]]): Boolean = isEvaluated(l, st) && (evalLazyConQS[T](l) match {
- case Spine(_, _, tail13) =>
- isConcrete[T](tail13, st)
- case _ =>
- true
- })
-
- def schedulesProperty[T](q: LazyConQ[T], schs: Scheds[T], st: Set[LazyConQ[T]]): Boolean = {
- schs match {
- case Cons(head, tail) =>
- evalLazyConQS[T](head) match {
- case Spine(Empty(), _, _) =>
- !head.isInstanceOf[Eager[T]] &&
- concreteUntil(q, head, st) && schedulesProperty[T](pushUntilZero[T](head), tail, st)
- case _ =>
- false
- }
- case Nil() =>
- isConcrete(q, st)
- }
- }
-
- def strongSchedsProp[T](q: LazyConQ[T], schs: Scheds[T], st: Set[LazyConQ[T]]) = {
- isEvaluated(q, st) && {
- val l = evalLazyConQS[T](q) match {
- case Spine(_, _, rear) =>
- rear
- case _ => q
- }
- schedulesProperty(l, schs, st)
- }
- }
-
- // pushes a carry until there is a one
- // TODO: rename this to pushUntilCarry
- def pushUntilZero[T](q: LazyConQ[T]): LazyConQ[T] = evalLazyConQS[T](q) match {
- case Spine(Empty(), _, rear12) =>
- pushUntilZero[T](rear12)
- case Spine(h, _, rear13) =>
- rear13
- case Tip(_) =>
- q
- }
-
- def pushLeft[T](ys: Single[T], xs: LazyConQ[T], st: Set[LazyConQ[T]]): (ConQ[T], Set[LazyConQ[T]]) = {
- require(zeroPreceedsLazy[T](xs, st) && ys.isInstanceOf[Single[T]])
-
- val dres5 = evalLazyConQ[T](xs, st)
- dres5._1 match {
- case Tip(CC(_, _)) =>
- (Spine[T](ys, False(), xs), dres5._2)
- case Tip(Empty()) =>
- (Tip[T](ys), dres5._2)
- case Tip(t @ Single(_)) =>
- (Tip[T](CC[T](ys, t)), dres5._2)
- case s @ Spine(Empty(), _, rear) =>
- (Spine[T](ys, False(), rear), dres5._2) // in this case firstUnevaluated[T](rear, st) == firstUnevaluated[T](xs, st)
- case s @ Spine(_, _, _) =>
- pushLeftLazy[T](ys, xs, dres5._2)
- }
- }
-
-/* def dummyFun[T]() = ???[(ConQ[T], Set[LazyConQ[T]])]
-
- @library
- def pushLeftLazyUI[T](ys: Conc[T], xs: LazyConQ[T], st: Set[LazyConQ[T]]): (ConQ[T], Set[LazyConQ[T]]) = {
- dummyFun()
- } ensuring (res => res._2 == st && (res._1 match {
- case Spine(Empty(), createdWithSusp, rear) =>
- true
- case _ => false
- }))*/
-
- def pushLeftLazy[T](ys: Conc[T], xs: LazyConQ[T], st: Set[LazyConQ[T]]): (ConQ[T], Set[LazyConQ[T]]) = {
- require(!ys.isEmpty && zeroPreceedsLazy[T](xs, st) &&
- (evalLazyConQS(xs) match {
- case Spine(h, _, _) => h != Empty[T]()
- case _ => false
- }))
- val dres = evalLazyConQ[T](xs, st)
- dres._1 match {
- case Spine(head, _, rear15) =>
- val carry = CC[T](head, ys)
- val dres2 = evalLazyConQ[T](rear15, dres._2)
- dres2._1 match {
- case s @ Spine(Empty(), _, _) =>
- (Spine[T](Empty[T](), False(), Eager(Spine(carry, False(), rear15))), dres2._2)
- case s @ Spine(_, _, _) =>
- (Spine[T](Empty[T](), True(), PushLeftLazy[T](carry, rear15 /*, suf*/ )), dres2._2)
- case t @ Tip(tree) =>
- if (tree.level > carry.level) { // can this happen ? this means tree is of level at least two greater than rear ?
- val x: ConQ[T] = t
- (Spine[T](Empty[T](), False(), Eager(Spine(carry, False(), rear15))), dres2._2)
- } else { // here tree level and carry level are equal
- val x: ConQ[T] = Tip[T](CC[T](tree, carry))
- (Spine[T](Empty[T](), False(), Eager(Spine(Empty[T](), False(), Eager[T](x)))), dres2._2)
- }
- }
- }
- } ensuring {
- (res66: (Spine[T], Set[LazyConQ[T]])) =>
- (res66._2 == st) && (res66._1 match {
- case Spine(Empty(), createdWithSusp, rear) =>
- val (rearval, _) = evalLazyConQ[T](rear, st) // this is necessary to assert properties on the state in the recursive invocation
- (!isConcrete(xs, st) || isConcrete(pushUntilZero(rear), st))
- case _ =>
- false
- })
- }
-
- def pushLeftLazyLemma[T](ys: Conc[T], xs: LazyConQ[T], suf: LazyConQ[T], st: Set[LazyConQ[T]]): Boolean = {
- require(!ys.isEmpty && zeroPreceedsLazy[T](xs, st) &&
- (evalLazyConQS(xs) match {
- case Spine(h, _, _) => h != Empty[T]()
- case _ => false
- }) &&
- (evalLazyConQS(suf) match {
- case Spine(Empty(), _, _) =>
- concreteUntil(xs, suf, st)
- case _ => false
- }))
- // property
- (pushLeftLazy(ys, xs, st)._1 match {
- case Spine(Empty(), createdWithSusp, rear) =>
- // forall suf. suf*.head == Empty() ^ concUntil(xs, suf, st) => concUntil(push(rear), suf, st)
- val p = pushUntilZero[T](rear)
- concreteUntil(p, suf, st)
- }) &&
- // induction scheme
- (evalLazyConQS(xs) match {
- case Spine(head, _, rear15) =>
- val carry = CC[T](head, ys)
- evalLazyConQS(rear15) match {
- case s @ Spine(h, _, _) if h != Empty[T]() =>
- pushLeftLazyLemma(carry, rear15, suf, st)
- case _ => true
- }
- })
- } holds
-
- def pushLeftWrapper[T](ys: Single[T], w: Wrapper[T], st: Set[LazyConQ[T]]) = {
- require(w.valid(st) && ys.isInstanceOf[Single[T]])
- val (nq, nst) = pushLeft[T](ys, w.queue, st)
- val nsched = nq match {
- case Spine(Empty(), createdWithSusp, rear18) if createdWithSusp == True() =>
- Cons[T](rear18, w.schedule) // this is the only case where we create a new lazy closure
- case _ =>
- w.schedule
- }
- (Eager(nq), nsched, nst)
- } ensuring { res =>
- strongSchedsProp(res._1, res._2, res._3) &&
- // lemma instantiations
- (w.schedule match {
- case Cons(head, tail) =>
- evalLazyConQS(w.queue) match {
- case Spine(h, _, _) if h != Empty[T]() =>
- pushLeftLazyLemma(ys, w.queue, head, st)
- case _ => true
- }
- case _ => true
- })
- }
-
- /*def PushLeftLazypushLeftLazyLem[T](rear15 : LazyConQ[T], head : Conc[T], dres : (ConQ[T], Set[LazyConQ[T]]), st : Set[LazyConQ[T]], xs : LazyConQ[T], s : Spine[T], dres : (ConQ[T], Set[LazyConQ[T]]), carry : CC[T], ys : Conc[T]): Boolean = {
- (!ys.isEmpty && zeroPreceedsLazy[T](xs, st) && evalLazyConQS[T](xs).isSpine && dres == evalLazyConQ[T](xs, st) && (!dres._1.isInstanceOf[Spine[T]] || !dres._1.head.isInstanceOf[Empty[T]]) && dres._1.isInstanceOf[Spine[T]] && head == dres._1.head && rear15 == dres._1.rear && carry == CC[T](head, ys) && dres == evalLazyConQ[T](rear15, dres._2) && (!dres._1.isInstanceOf[Spine[T]] || !dres._1.head.isInstanceOf[Empty[T]]) && dres._1.isInstanceOf[Spine[T]] && s == dres._1) ==> (!carry.isEmpty && zeroPreceedsLazy[T](rear15, dres._2) && evalLazyConQS[T](rear15).isSpine)
- } ensuring {
- (holds : Boolean) => holds
- }*/
-
- def schedMonotone[T](st1: Set[LazyConQ[T]], st2: Set[LazyConQ[T]], scheds: Scheds[T], l: LazyConQ[T]): Boolean = {
- require(st1.subsetOf(st2) && schedulesProperty(l, scheds, st1))
- schedulesProperty(l, scheds, st2) && //property
- //induction scheme
- (scheds match {
- case Cons(head, tail) =>
- evalLazyConQS[T](head) match {
- case Spine(_, _, rear) =>
- concUntilMonotone(l, head, st1, st2) &&
- schedMonotone(st1, st2, tail, pushUntilZero(head))
- case _ => true
- }
- case Nil() =>
- concreteMonotone(st1, st2, l)
- })
- } holds
-
- def concreteMonotone[T](st1: Set[LazyConQ[T]], st2: Set[LazyConQ[T]], l: LazyConQ[T]): Boolean = {
- require(isConcrete(l, st1) && st1.subsetOf(st2))
- isConcrete(l, st2) && {
- // induction scheme
- evalLazyConQS[T](l) match {
- case Spine(_, _, tail) =>
- concreteMonotone[T](st1, st2, tail)
- case _ =>
- true
- }
- }
- } holds
-
- def concUntilExtenLemma[T](q: LazyConQ[T], suf: LazyConQ[T], st: Set[LazyConQ[T]]): Boolean = {
- require(concreteUntil(q, suf, st))
- val (next, nst) = evalLazyConQ[T](suf, st)
- (next match {
- case Spine(_, _, rear) =>
- concreteUntil(q, rear, nst)
- case _ => true
- }) &&
- (if (q != suf) {
- evalLazyConQS[T](q) match {
- case Spine(_, _, tail) =>
- concUntilExtenLemma(tail, suf, st)
- case _ =>
- true
- }
- } else true)
- } holds
-
- def concUntilExtenLemma2[T](q: LazyConQ[T], suf: LazyConQ[T], st: Set[LazyConQ[T]]): Boolean = {
- require(concreteUntil(q, suf, st) && isConcrete(suf, st))
- isConcrete(q, st) &&
- (if (q != suf) {
- evalLazyConQS[T](q) match {
- case Spine(_, _, tail) =>
- concUntilExtenLemma2(tail, suf, st)
- case _ =>
- true
- }
- } else true)
- } ensuring (_ == true)
-
- def concUntilCompose[T](q: LazyConQ[T], suf1: LazyConQ[T], suf2: LazyConQ[T], st: Set[LazyConQ[T]]): Boolean = {
- require(concreteUntil(q, suf1, st) && concreteUntil(suf1, suf2, st))
- concreteUntil(q, suf2, st) &&
- (if (q != suf1) {
- evalLazyConQS[T](q) match {
- case Spine(_, _, tail) =>
- concUntilCompose(tail, suf1, suf2, st)
- case _ =>
- true
- }
- } else true)
- } ensuring (_ == true)
-
- def concUntilMonotone[T](q: LazyConQ[T], suf: LazyConQ[T], st1: Set[LazyConQ[T]], st2: Set[LazyConQ[T]]): Boolean = {
- require(concreteUntil(q, suf, st1) && st1.subsetOf(st2))
- concreteUntil(q, suf, st2) &&
- (if (q != suf) {
- evalLazyConQS[T](q) match {
- case Spine(_, _, tail) =>
- concUntilMonotone(tail, suf, st1, st2)
- case _ =>
- true
- }
- } else true)
- } ensuring (_ == true)
-
- def concUntilZeroPredLemma[T](q: LazyConQ[T], suf: LazyConQ[T], st: Set[LazyConQ[T]]): Boolean = {
- require(concreteUntil(q, suf, st) && (evalLazyConQS(suf) match {
- case Spine(Empty(), _, _) => true
- case _ => false
- }))
- val (next, nst) = evalLazyConQ[T](suf, st)
- zeroPreceedsLazy(q, nst) &&
- (if (q != suf) {
- evalLazyConQS[T](q) match {
- case Spine(_, _, tail) =>
- concUntilZeroPredLemma(tail, suf, st)
- case _ =>
- true
- }
- } else true)
- } holds
-
- def concreteZeroPredLemma[T](q: LazyConQ[T], st: Set[LazyConQ[T]]): Boolean = {
- require(isConcrete(q, st))
- zeroPreceedsLazy(q, st) && {
- // induction scheme
- evalLazyConQS[T](q) match {
- case Spine(_, _, tail) =>
- concreteZeroPredLemma[T](tail, st)
- case _ =>
- true
- }
- }
- } holds
-
- def Pay[T](q: LazyConQ[T], scheds: Scheds[T], st: Set[LazyConQ[T]]): (Scheds[T], Set[LazyConQ[T]]) = {
- require(strongSchedsProp(q, scheds, st) && isEvaluated(q, st))
- val (nschs, rst) = scheds match {
- case c @ Cons(head, rest) =>
- val (headval, st2) = evalLazyConQ(head, st)
- (headval match {
- case Spine(Empty(), createdWithSusp, rear) => // note: no other case is possible
- if (createdWithSusp == True()) {
- Cons(rear, rest)
- } else
- rest
- // In this case,
- // val prear = pushUntilZero(rear)
- // concreteUntil(q, rhead, res._2) && concreteUntil(prear, rhead, st) && concreteUntil(rear, rhead, st) && schedulesProperty(prhead, rtail, st)
- }, st2)
- case Nil() =>
- (scheds, st)
- }
- (nschs, rst)
- } ensuring { res =>
- val l = evalLazyConQS[T](q) match {
- case Spine(_, _, rear) =>
- rear
- case _ => q
- }
- strongSchedsProp(q, res._1, res._2) &&
- zeroPreceedsLazy(q, res._2) &&
- (scheds match {
- case Cons(head, rest) =>
- concUntilExtenLemma(l, head, st) &&
- (res._1 match {
- case Cons(rhead, rtail) =>
- val prhead = pushUntilZero(rhead)
- schedMonotone(st, res._2, rtail, prhead) &&
- (evalLazyConQS(head) match {
- case Spine(Empty(), cws, rear) =>
- if (cws == False()) {
- concUntilMonotone(rear, rhead, st, res._2) &&
- concUntilCompose(l, rear, rhead, res._2)
- } else true
- })
- case _ =>
- evalLazyConQS(head) match {
- case Spine(Empty(), _, rear) =>
- concreteMonotone(st, res._2, rear) &&
- concUntilExtenLemma2(l, rear, res._2)
- }
- })
- case _ => true
- }) &&
- // instantiations for zeroPreceedsLazy
- (scheds match {
- case Cons(head, rest) =>
- //concUntil(l, head, st) == head && head* == Spine(Empty(), _) && res._2.subsetOf(st ++ { head })
- concUntilZeroPredLemma(l, head, st)
- case _ =>
- concreteZeroPredLemma(q, res._2)
- })
- }
-
- def pushLeftAndPay[T](ys: Single[T], w: Wrapper[T], st: Set[LazyConQ[T]]) = {
- require(w.valid(st) && ys.isInstanceOf[Single[T]])
- val (q, scheds, nst) = pushLeftWrapper(ys, w, st)
- val (nscheds, fst) = Pay(q, scheds, nst)
- (Wrapper(q, nscheds), fst)
- } ensuring { res => res._1.valid(res._2) }
-
- def lazyarg1[T](x: ConQ[T]): ConQ[T] = x
-}
-
-object ConQ {
-
- abstract class LazyConQ[T1]
-
- case class Eager[T](x: ConQ[T]) extends LazyConQ[T]
-
- case class PushLeftLazy[T](ys: Conc[T], xs: LazyConQ[T] /*, suf: LazyConQ[T]*/ ) extends LazyConQ[T]
-
- @library
- def newConQ[T1](cc: LazyConQ[T1], st: Set[LazyConQ[T1]]): LazyConQ[T1] = {
- cc
- } ensuring {
- (res: LazyConQ[T1]) => !st.contains(res)
- }
-
- @library
- def evalLazyConQ[T](cl: LazyConQ[T], st: Set[LazyConQ[T]]): (ConQ[T], Set[LazyConQ[T]]) = {
- cl match {
- case t: Eager[T] =>
- (t.x, st)
- case t: PushLeftLazy[T] =>
- val plres = pushLeftLazy[T](t.ys, t.xs, uiState())._1
- val plst = pushLeftLazy[T](t.ys, t.xs, st)._2
- //val plres = pushLeftLazyUI[T](t.ys, t.xs, uiState())._1
- //val plst = pushLeftLazyUI[T](t.ys, t.xs, st)._2
- (plres, (plst ++ Set[LazyConQ[T]](t)))
- }
- }
-
- def isEvaluated[T](cl: LazyConQ[T], st: Set[LazyConQ[T]]) = st.contains(cl) || cl.isInstanceOf[Eager[T]]
-
- def uiState[T](): Set[LazyConQ[T]] = ???[Set[LazyConQ[T]]]
-
- def evalLazyConQS[T](cl: LazyConQ[T]): ConQ[T] = evalLazyConQ[T](cl, uiState())._1
-
-}
-
-// Cases that had to be considered for pushLeftWrapper
- /*(w.schedule match {
- case Cons(head, tail) => true
- //strongSchedsProp(res._1, res._2, res._3)
- case _ =>
- res._2 match {
- case Nil() => true
- //strongSchedsProp(res._1, res._2, res._3)
- case _ =>
- strongSchedsProp(res._1, res._2, res._3)
- }
- }) &&*/
- /*(//pushLeft(ys, w.queue, st)._1 match {
- //case Spine(Empty(), createdWithSusp, _) if createdWithSusp == True() => true
- /*(w.schedule match {
- case Cons(head, tail) =>
- schedulesProperty(res._1, res._2, res._3)
- case _ => true
- })*/
- //case Spine(Empty(), _, _) => true
- /*(w.schedule match {
- case Cons(head, tail) =>
- schedulesProperty(res._1, res._2, res._3)
- case _ => true
- })*/
- //case Spine(_, _, _) =>
- /*(w.schedule match {
- case Cons(head, tail) =>
- schedulesProperty(res._1, res._2, res._3)
- case _ => true
- })*/
- //case _ => true
- //schedulesProperty(res._1, res._2, res._3)
- })*/
-
- /*def payLemma[T](q: LazyConQ[T], scheds: Scheds[T], st: Set[LazyConQ[T]]) = {
- require(strongSchedsProp(q, scheds, st) && isEvaluated(q, st))
- val res = Pay(q, scheds, st)
- val l = evalLazyConQS[T](q) match {
- case Spine(_, _, rear) =>
- rear
- case _ => q
- }
- strongSchedsProp(q, res._1, res._2) &&
- zeroPreceedsLazy(q, res._2) &&
- (scheds match {
- case Cons(head, rest) =>
- concUntilExtenLemma(l, head, st) &&
- (res._1 match {
- case Cons(rhead, rtail) =>
- val prhead = pushUntilZero(rhead)
- schedMonotone(st, res._2, rtail, prhead) &&
- (evalLazyConQS(head) match {
- case Spine(Empty(), cws, rear) =>
- if (cws == False()) {
- concUntilMonotone(rear, rhead, st, res._2) &&
- concUntilCompose(l, rear, rhead, res._2)
- } else true
- })
- case _ =>
- evalLazyConQS(head) match {
- case Spine(Empty(), _, rear) =>
- concreteMonotone(st, res._2, rear) &&
- concUntilExtenLemma2(l, rear, res._2)
- }
- })
- case _ => true
- }) &&
- // instantiations for zeroPreceedsLazy
- (scheds match {
- case Cons(head, rest) =>
- //concUntil(l, head, st) == head && head* == Spine(Empty(), _) && res._2.subsetOf(st ++ { head })
- concUntilZeroPredLemma(l, head, st)
- case _ =>
- concreteZeroPredLemma(q, res._2)
- })
- } ensuring (_ == true)*/
\ No newline at end of file
diff --git a/src/main/scala/leon/laziness/ClosurePreAsserter.scala b/src/main/scala/leon/laziness/ClosurePreAsserter.scala
index 9938127cfcfcc1c144531c9b967ff493a1cb8ae4..af789371009b46c93c9770cfd6e57a84d7b30f89 100644
--- a/src/main/scala/leon/laziness/ClosurePreAsserter.scala
+++ b/src/main/scala/leon/laziness/ClosurePreAsserter.scala
@@ -22,7 +22,7 @@ import LazinessUtil._
/**
* Generate lemmas that ensure that preconditions hold for closures.
*/
-class ClosurePreAsserter(p: Program) {
+class ClosurePreAsserter(p: Program, funsManager: LazyFunctionsManager) {
def hasClassInvariants(cc: CaseClass): Boolean = {
val opname = ccNameToOpName(cc.ct.classDef.id.name)
@@ -43,10 +43,11 @@ class ClosurePreAsserter(p: Program) {
// Note: once we have separated normal preconditions from state preconditions
// it suffices to just consider state preconditions here
closures.map {
- case ((CaseClass(CaseClassType(ccd, _), args), st), path) =>
+ case ((CaseClass(CaseClassType(ccd, _), argsRet), st), path) =>
anchorfd = Some(fd)
val target = functionByName(ccNameToOpName(ccd.id.name), p).get //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 nargs =
if (target.params.size > args.size) // target takes state ?
args :+ st
diff --git a/src/main/scala/leon/laziness/FreeVariableFactory.scala b/src/main/scala/leon/laziness/FreeVariableFactory.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fe07ea8b9a2ed30b0c727a84342fc168c83018d9
--- /dev/null
+++ b/src/main/scala/leon/laziness/FreeVariableFactory.scala
@@ -0,0 +1,108 @@
+package leon
+package laziness
+
+import invariant.factories._
+import invariant.util.Util._
+import invariant.util._
+import invariant.structure.FunctionUtils._
+import purescala.ScalaPrinter
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.DefOps._
+import purescala.Extractors._
+import purescala.Types._
+import leon.invariant.util.TypeUtil._
+import leon.invariant.util.LetTupleSimplification._
+import java.io.File
+import java.io.FileWriter
+import java.io.BufferedWriter
+import scala.util.matching.Regex
+import leon.purescala.PrettyPrinter
+import leon.LeonContext
+import leon.LeonOptionDef
+import leon.Main
+import leon.TransformationPhase
+import LazinessUtil._
+import invariant.util.ProgramUtil._
+
+/**
+ * A class that maintains a data type that can used to
+ * create free variables at different points in the program.
+ * All free variables are of type `FreeVar` which can be mapped
+ * to a required type by applying uninterpreted functions.
+ */
+class FreeVariableFactory() {
+
+ val absClass = AbstractClassDef(FreshIdentifier("FreeVar@"), Seq(), None)
+ val absType = AbstractClassType(absClass, Seq())
+ val varCase = {
+ val cdef = CaseClassDef(FreshIdentifier("Var@"), Seq(), Some(absType), false)
+ cdef.setFields(Seq(ValDef(FreshIdentifier("fl", absType))))
+ absClass.registerChild(cdef)
+ cdef
+ }
+ val nextCase = {
+ val cdef = CaseClassDef(FreshIdentifier("NextVar@"), Seq(), Some(absType), false)
+ cdef.setFields(Seq(ValDef(FreshIdentifier("fl", absType))))
+ absClass.registerChild(cdef)
+ cdef
+ }
+ val nilCase = {
+ val cdef = CaseClassDef(FreshIdentifier("NilVar@"), Seq(), Some(absType), false)
+ absClass.registerChild(cdef)
+ cdef
+ }
+
+ class FreeVarListIterator(initRef: Variable) {
+ require(initRef.getType == absType)
+ var refExpr : Expr = initRef
+ def current = CaseClass(varCase.typed, Seq(refExpr)) // Var(refExpr)
+ def next {
+ refExpr = CaseClass(nextCase.typed, Seq(refExpr)) // Next(refExpr)
+ }
+ }
+
+ var uifuns = Map[TypeTree, FunDef]()
+ def getOrCreateUF(t: TypeTree) = {
+ uifuns.getOrElse(t, {
+ val funName = "uop@" + TypeUtil.typeNameWOParams(t)
+ val param = ValDef(FreshIdentifier("a", absType))
+ val tparams = TypeUtil.getTypeParameters(t) map TypeParameterDef.apply _
+ val uop = new FunDef(FreshIdentifier(funName), tparams, Seq(param), t)
+ uifuns += (t -> uop)
+ uop
+ })
+ }
+
+ class FreeVariableGenerator(initRef: Variable) {
+ val flIter = new FreeVarListIterator(initRef)
+
+ /**
+ * Free variables are not guaranteed to be unique.
+ * They are operations over unique references.
+ */
+ def nextFV(t: TypeTree) = {
+ val uop = getOrCreateUF(t)
+ val fv = FunctionInvocation(TypedFunDef(uop, Seq()), Seq(flIter.current))
+ flIter.next
+ fv
+ }
+
+ /**
+ * References are guaranteed to be unique.
+ */
+ def nextRef = {
+ val ref = flIter.current
+ flIter.next
+ ref
+ }
+ }
+
+ def getFreeVarGenerator(initRef: Variable) = new FreeVariableGenerator(initRef)
+
+ def createdClasses = Seq(absClass, varCase, nextCase, nilCase)
+
+ def createdFunctions = uifuns.keys.toSeq
+}
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 00031ad846c87bd9d32717c067e331dd710bb95d..b4ca0ef0091713e57493ad402be66366b2bd139d 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -39,10 +39,10 @@ import PredicateUtil._
object LazinessEliminationPhase extends TransformationPhase {
val debugLifting = false
val dumpInputProg = false
- val dumpLiftProg = true
+ val dumpLiftProg = false
val dumpProgramWithClosures = true
val dumpTypeCorrectProg = false
- val dumpProgWithPreAsserts = false
+ val dumpProgWithPreAsserts = true
val dumpProgWOInstSpecs = true
val dumpInstrumentedProgram = true
val debugSolvers = false
@@ -55,7 +55,7 @@ object LazinessEliminationPhase extends TransformationPhase {
" to a program that does not use lazy constructs"
// options that control behavior
- val optRefEquality = LeonFlagOptionDef("useRefEquality", "Uses reference equality which memoizing closures", false)
+ val optRefEquality = LeonFlagOptionDef("refEq", "Uses reference equality for comparing closures", false)
/**
* TODO: enforce that the specs do not create lazy closures
@@ -74,7 +74,9 @@ object LazinessEliminationPhase extends TransformationPhase {
prettyPrintProgramToFile(nprog, ctx, "-lifted")
}
- val progWithClosures = (new LazyClosureConverter(nprog, ctx, new LazyClosureFactory(nprog))).apply
+ val funsManager = new LazyFunctionsManager(nprog)
+ val closureFactory = new LazyClosureFactory(nprog)
+ val progWithClosures = (new LazyClosureConverter(nprog, ctx, closureFactory, funsManager)).apply
if (dumpProgramWithClosures) {
//println("After closure conversion: \n" + ScalaPrinter.apply(progWithClosures, purescala.PrinterOptions(printUniqueIds = true)))
prettyPrintProgramToFile(progWithClosures, ctx, "-closures")
@@ -85,7 +87,7 @@ object LazinessEliminationPhase extends TransformationPhase {
if (dumpTypeCorrectProg)
println("After rectifying types: \n" + ScalaPrinter.apply(typeCorrectProg))
- val progWithPre = (new ClosurePreAsserter(typeCorrectProg)).apply
+ val progWithPre = (new ClosurePreAsserter(typeCorrectProg, funsManager)).apply
if (dumpProgWithPreAsserts) {
//println("After asserting closure preconditions: \n" + ScalaPrinter.apply(progWithPre))
prettyPrintProgramToFile(progWithPre, ctx, "-withpre")
diff --git a/src/main/scala/leon/laziness/LazyClosureConverter.scala b/src/main/scala/leon/laziness/LazyClosureConverter.scala
index 4075adf96e94233c37fa761ada5efbba51d78637..35046cdb49c5cf2b7c0a905c46439d79542dfa94 100644
--- a/src/main/scala/leon/laziness/LazyClosureConverter.scala
+++ b/src/main/scala/leon/laziness/LazyClosureConverter.scala
@@ -36,26 +36,30 @@ import purescala.TypeOps._
* (d) replace isEvaluated with currentState.contains()
* (e) replace accesses to $.value with calls to dispatch with current state
*/
-class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClosureFactory) {
+class LazyClosureConverter(p: Program, ctx: LeonContext,
+ closureFactory: LazyClosureFactory,
+ funsManager : LazyFunctionsManager) {
val debug = false
// flags
//val removeRecursionViaEval = false
- val useRefEquality = ctx.findOption(LazinessEliminationPhase.optRefEquality).getOrElse(false)
+ val refEq = ctx.findOptionOrDefault(LazinessEliminationPhase.optRefEquality)
- val funsManager = new LazyFunctionsManager(p)
val funsNeedStates = funsManager.funsNeedStates
val funsRetStates = funsManager.funsRetStates
+ val transCons = funsManager.callersOfLazyCons // transitive constructors of closures
+ val fvFactory = new FreeVariableFactory()
val tnames = closureFactory.lazyTypeNames
+ val lazyops = closureFactory.lazyops
// create a mapping from functions to new functions
- lazy val funMap = p.definedFunctions.collect {
+ val funMap = p.definedFunctions.collect {
case fd if (fd.hasBody && !fd.isLibrary) =>
// replace lazy types in parameters and return values
val nparams = fd.params map { vd =>
ValDef(vd.id, Some(replaceLazyTypes(vd.getType))) // override type of identifier
}
val nretType = replaceLazyTypes(fd.returnType)
- val nfd = if (funsNeedStates(fd)) {
+ val nfd = if (funsNeedStates(fd)) { // this also includes lazy constructors
var newTParams = Seq[TypeParameterDef]()
val stTypes = tnames map { tn =>
val absClass = closureFactory.absClosureType(tn)
@@ -67,6 +71,11 @@ class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClo
val stParams = stTypes.map { stType =>
ValDef(FreshIdentifier("st@", stType, true))
}
+// val flParams =
+// if(transCons(fd)) {
+// Seq(ValDef(FreshIdentifier("fl@", fvFactory.absType, true)))
+// } else
+// Seq()
val retTypeWithState =
if (funsRetStates(fd))
TupleType(nretType +: stTypes)
@@ -92,14 +101,16 @@ class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClo
// (k -> ufd)
// }.toMap
+ //TODO: we can omit come functions whose translations will not be recursive.
+ def takesStateButIndep(fd: FunDef) =
+ funsNeedStates(fd) && funsManager.hasStateIndependentBehavior(fd)
+
/**
* A set of uninterpreted functions that are used
* in specs to ensure that value part is independent of the state
*/
- val uiFuncs = funMap.collect {
- case (k, v) if funsNeedStates(k) &&
- funsManager.hasStateIndependentBehavior(k) => //TODO: we can omit come functions whose translations will not be recursive.
-
+ val uiFuncs : Map[FunDef, (FunDef, Option[FunDef])] = funMap.collect {
+ case (k, v) if takesStateButIndep(k) =>
val params = v.params.take(k.params.size) // ignore the state params
val retType =
if (funsRetStates(k)) {
@@ -121,7 +132,18 @@ class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClo
FunctionInvocation(TypedFunDef(ufd, tparams), params.map(_.id.toVariable))), // res = funUI(..)
Lambda(Seq(ValDef(resid)), resid.toVariable)) // holds
pred.addFlag(Annotation("axiom", Seq())) // mark it as @library
- (k -> (ufd, pred))
+ (k -> (ufd, Some(pred)))
+
+ case (k, v) if lazyops(k) =>
+ // here 'v' cannot for sure take state params, otherwise it must be state indep
+ if(funsNeedStates(k))
+ throw new IllegalStateException("Lazyop that has a state dependent behavior: "+k)
+ else {
+ val tparams = (v.params.map(_.getType) :+ v.returnType).flatMap(getTypeParameters(_)).distinct
+ val tparamsDef = tparams.map(TypeParameterDef(_))
+ val ufd = new FunDef(FreshIdentifier(v.id.name + "UI"), tparamsDef, v.params, v.returnType)
+ (k -> (ufd, None))
+ }
}.toMap
/**
@@ -199,7 +221,9 @@ class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClo
val binder = FreshIdentifier("t", ctype)
val pattern = InstanceOfPattern(Some(binder), ctype)
// create a body of the match
- val args = cdef.fields map { fld => CaseClassSelector(ctype, binder.toVariable, fld.id) }
+ // the last field represents the result
+ val args = cdef.fields.dropRight(1) map { fld =>
+ CaseClassSelector(ctype, binder.toVariable, fld.id) }
val op = closureFactory.caseClassToOp(cdef)
val targetFun = funMap(op)
// invoke the target fun with appropriate values
@@ -257,7 +281,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClo
* They are defined for each lazy class since it avoids generics and
* simplifies the type inference (which is not full-fledged in Leon)
*/
- lazy val closureCons = tnames.map { tname =>
+ val closureCons = tnames.map { tname =>
val adt = closureFactory.absClosureType(tname)
val param1Type = AbstractClassType(adt, adt.tparams.map(_.tp))
val param1 = FreshIdentifier("cc", param1Type)
@@ -269,10 +293,9 @@ class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClo
fun.body = Some(param1.toVariable)
// assert that the closure in unevaluated if useRefEquality is enabled
- if (useRefEquality) {
+ if (refEq) {
val resid = FreshIdentifier("res", param1Type)
val postbody = Not(ElementOfSet(resid.toVariable, param2.toVariable))
- /*SubsetOf(FiniteSet(Set(resid.toVariable), param1Type), param2.toVariable)*/
fun.postcondition = Some(Lambda(Seq(ValDef(resid)), postbody))
fun.addFlag(Annotation("axiom", Seq()))
}
@@ -285,10 +308,21 @@ class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClo
if isLazyInvocation(finv)(p) =>
val op = (nargs: Seq[Expr]) => ((st: Map[String, Expr]) => {
val adt = closureFactory.closureOfLazyOp(argfd)
- val cc = CaseClass(CaseClassType(adt, tparams), nargs)
+ // create lets to bind the nargs to variables
+ val (flatArgs, letCons) = nargs.foldRight((Seq[Variable](), (e : Expr) => e)){
+// case (narg : Variable, (fargs, lcons)) =>
+// (narg +: fargs, lcons)
+ 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 baseLazyTypeName = closureFactory.lazyTypeNameOfClosure(adt)
- FunctionInvocation(TypedFunDef(closureCons(baseLazyTypeName), tparams),
+ val fi = FunctionInvocation(TypedFunDef(closureCons(baseLazyTypeName), tparams),
Seq(cc, st(baseLazyTypeName)))
+ letCons(fi) // this could be 'fi' wrapped into lets
}, false)
mapNAryOperator(args, op)
@@ -584,8 +618,8 @@ class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClo
// create a predicate that ensures that the value part is independent of the state
val valRel =
- if (uiFuncs.contains(fd)) { // add specs on value
- val uipred = uiFuncs(fd)._2
+ if (takesStateButIndep(fd)) { // add specs on value
+ val uipred = uiFuncs(fd)._2.get
val args = nfd.params.take(fd.params.size).map(_.id.toVariable)
val retarg =
if(funsRetStates(fd))
@@ -668,19 +702,27 @@ class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClo
val cdefs = closureFactory.closures(tname)
val tparams = evalfd.tparams.map(_.tp)
val postres = FreshIdentifier("res", evalfd.returnType)
- val postMatchCases = cdefs flatMap { cdef =>
+ val postMatchCases = cdefs map { cdef =>
// create a body of the match (which asserts that return value equals the uninterpreted function)
+ // and also that the result field equals the result
val op = closureFactory.lazyopOfClosure(cdef)
- if (uiFuncs.contains(op)) {
- val ctype = CaseClassType(cdef, tparams)
- val binder = FreshIdentifier("t", ctype)
- val pattern = InstanceOfPattern(Some(binder), ctype)
- val args = cdef.fields map { fld => CaseClassSelector(ctype, binder.toVariable, fld.id) }
- val rhs = Equals(TupleSelect(postres.toVariable, 1),
- FunctionInvocation(TypedFunDef(uiFuncs(op)._1, tparams), args)
- )
- Seq(MatchCase(pattern, None, rhs))
- } else Seq()
+ val ctype = CaseClassType(cdef, tparams)
+ 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))
+ //res._1 == uifun(args)
+ val clause2 = if (takesStateButIndep(op)) {
+ val args = cdef.fields.dropRight(1) map {
+ fld => CaseClassSelector(ctype, binder.toVariable, fld.id)
+ }
+ Some(Equals(TupleSelect(postres.toVariable, 1),
+ FunctionInvocation(TypedFunDef(uiFuncs(op)._1, tparams), args)))
+ } else None
+ val rhs = createAnd(clause1 +: clause2.toList)
+ MatchCase(pattern, None, rhs)
}
// create a default case ot match other cases
val default = MatchCase(WildcardPattern(None), None, Util.tru)
@@ -721,8 +763,10 @@ class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClo
(defs: Seq[Definition]) => defs.flatMap {
case fd: FunDef if funMap.contains(fd) =>
uiFuncs.get(fd) match {
- case Some((funui, predui)) =>
+ case Some((funui, Some(predui))) =>
Seq(funMap(fd), funui, predui)
+ case Some((funui, _)) =>
+ Seq(funMap(fd), funui)
case _ => Seq(funMap(fd))
}
case d => Seq(d)
diff --git a/src/main/scala/leon/laziness/LazyClosureFactory.scala b/src/main/scala/leon/laziness/LazyClosureFactory.scala
index 1f156b539ac20008a37b5849c7eeddf1fd47b1c0..f5fffde3112dff7cf7f547b58a586d378bdb6e8d 100644
--- a/src/main/scala/leon/laziness/LazyClosureFactory.scala
+++ b/src/main/scala/leon/laziness/LazyClosureFactory.scala
@@ -72,9 +72,11 @@ class LazyClosureFactory(p: Program) {
var opToAdt = Map[FunDef, CaseClassDef]()
val tpeToADT = tpeToLazyops map {
case (tpename, ops) =>
- val baseT = ops(0).returnType //TODO: replace targs here ?
+ val baseT = ops(0).returnType //TODO: replace targs here i.e, use clresType ?
val absClass = tpeToAbsClass(tpename)
val absTParamsDef = absClass.tparams
+ val absTParams = absTParamsDef.map(_.tp)
+
// create a case class for every operation
val cdefs = ops map { opfd =>
assert(opfd.tparams.size == absTParamsDef.size)
@@ -91,20 +93,21 @@ class LazyClosureFactory(p: Program) {
ValDef(FreshIdentifier(vd.id.name, adtType))
}
}
- cdef.setFields(nfields)
+ // add a result field as well
+ val resField = ValDef(FreshIdentifier("clres", opfd.returnType))
+ cdef.setFields(nfields :+ resField)
absClass.registerChild(cdef)
opToAdt += (opfd -> cdef)
cdef
}
// create a case class to represent eager evaluation
- val absTParams = absTParamsDef.map(_.tp)
- val fldType = ops(0).returnType match {
+ val clresType = ops(0).returnType match {
case NAryType(tparams, tcons) => tcons(absTParams)
}
- val eagerid = FreshIdentifier("Eager"+TypeUtil.typeNameWOParams(fldType))
+ val eagerid = FreshIdentifier("Eager"+TypeUtil.typeNameWOParams(clresType))
val eagerClosure = CaseClassDef(eagerid, absTParamsDef,
Some(AbstractClassType(absClass, absTParams)), isCaseObject = false)
- eagerClosure.setFields(Seq(ValDef(FreshIdentifier("a", fldType))))
+ eagerClosure.setFields(Seq(ValDef(FreshIdentifier("a", clresType))))
absClass.registerChild(eagerClosure)
(tpename -> (baseT, absClass, cdefs, eagerClosure))
}
@@ -115,7 +118,9 @@ class LazyClosureFactory(p: Program) {
}
// this fixes an ordering on lazy types
- lazy val lazyTypeNames = tpeToADT.keys.toSeq
+ val lazyTypeNames = tpeToADT.keys.toSeq
+
+ val lazyops = opToCaseClass.keySet
def allClosuresAndParents = tpeToADT.values.flatMap(v => v._2 +: v._3 :+ v._4)
diff --git a/src/main/scala/leon/laziness/LazyFunctionsManager.scala b/src/main/scala/leon/laziness/LazyFunctionsManager.scala
index 1aa4f5a4b0a627fe1f2c8f7645807560cc3622cd..b738a63db21012183141b5452f367dd8b6c9437d 100644
--- a/src/main/scala/leon/laziness/LazyFunctionsManager.scala
+++ b/src/main/scala/leon/laziness/LazyFunctionsManager.scala
@@ -114,4 +114,19 @@ class LazyFunctionsManager(p: Program) {
!callersOfIsEvalandIsSusp.contains(fd)
}
+// lazy val targetsOfLazyCons = {
+// var callees = Set[FunDef]()
+// funsNeedStates.foreach {
+// case fd if fd.hasBody =>
+// postTraversal {
+// case finv: FunctionInvocation if isLazyInvocation(finv)(p) => // this is the lazy invocation constructor
+// callees += finv.tfd.fd
+// case _ =>
+// ;
+// }(fd.body.get)
+// case _ => ;
+// }
+// callees
+// }
+
}
diff --git a/src/main/scala/leon/laziness/RefDataTypeManager.scala b/src/main/scala/leon/laziness/RefDataTypeManager.scala
deleted file mode 100644
index 6a6ac9d8ac70f2238c5d835a27db44732d95d2c2..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/laziness/RefDataTypeManager.scala
+++ /dev/null
@@ -1,42 +0,0 @@
-package leon
-package laziness
-
-import invariant.factories._
-import invariant.util.Util._
-import invariant.util._
-import invariant.structure.FunctionUtils._
-import purescala.ScalaPrinter
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.DefOps._
-import purescala.Extractors._
-import purescala.Types._
-import leon.invariant.util.TypeUtil._
-import leon.invariant.util.LetTupleSimplification._
-import java.io.File
-import java.io.FileWriter
-import java.io.BufferedWriter
-import scala.util.matching.Regex
-import leon.purescala.PrettyPrinter
-import leon.LeonContext
-import leon.LeonOptionDef
-import leon.Main
-import leon.TransformationPhase
-import LazinessUtil._
-import invariant.util.ProgramUtil._
-
-/**
- * A class that maintains a data type that can be
- * used to create unique references
- */
-/*class RefDataTypeManager(p: Program) {
-
- lazy val valueType = CaseClassType(CaseClassDef(FreshIdentifier("Unit"), Seq(), None, false), Seq())
- lazy val refStreamDef = {
- val cd = CaseClassDef(FreshIdentifier("Ref"), Seq(), None, false)
- cd.setFields(Seq(ValDef(FreshIdentifier("data", valueType)),
- ValDef(FreshIdentifier("next", valueType)))
- }
-}*/
diff --git a/src/main/scala/leon/laziness/TypeChecker.scala b/src/main/scala/leon/laziness/TypeChecker.scala
index 978c33a367b7a8e33ee7e3a004454c9e61c8c601..0319cffa3123763b6256cb4c9fc774648b171b6b 100644
--- a/src/main/scala/leon/laziness/TypeChecker.scala
+++ b/src/main/scala/leon/laziness/TypeChecker.scala
@@ -145,6 +145,7 @@ object TypeChecker {
} else (id.getType, v)
case FunctionInvocation(TypedFunDef(fd, tparams), args) =>
+ //println(s"Consider expr: $e initial type: ${e.getType}")
val nargs = args.map(arg => rec(arg)._2)
var tpmap = Map[TypeParameter, TypeTree]()
(fd.params zip nargs).foreach { x =>
diff --git a/src/main/scala/leon/laziness/TypeRectifier.scala b/src/main/scala/leon/laziness/TypeRectifier.scala
index a253e46c7ae0a4668c61489cfd0c15aa78344d3a..b0eb0edae796332aa8bb667d43b68305bf1499cd 100644
--- a/src/main/scala/leon/laziness/TypeRectifier.scala
+++ b/src/main/scala/leon/laziness/TypeRectifier.scala
@@ -153,9 +153,8 @@ class TypeRectifier(p: Program, placeHolderParameter: TypeParameter => Boolean)
}
val nbody = rec(ifd.fullBody)
val initGamma = nfd.params.map(vd => vd.id -> vd.getType).toMap
- /*if(ifd.id.name.contains("pushLeftWrapper")) {
- println(s"Inferring types for ${ifd.id}")
- }*/
+
+ //println(s"Inferring types for ${ifd.id}: "+nbody)
val typedBody = TypeChecker.inferTypesOfLocals(nbody, initGamma)
/*if(ifd.id.name.contains("pushLeftWrapper")) {
//println(s"Inferring types for ${ifd.id} new fun: $nfd \n old body: ${ifd.fullBody} \n type correct body: $typedBody")
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 4f749a96c71db74efc033ccebf52f575e40b1836..8807a7b6685229dd4518e43dd5d6b8bf538571da 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -267,7 +267,7 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
if (!hasFoundAnswer) {
reporter.debug("- We need to keep going.")
- //for (i <- 1 to 3) {
+ for (i <- 1 to 3) {
val toRelease = unrollingBank.getBlockersToUnlock
reporter.debug(" - more unrollings")
@@ -278,7 +278,7 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
for (ncl <- newClauses) {
solver.assertCnstr(ncl)
}
- //}
+ }
// finish here
reporter.debug(" - finished unrolling")
diff --git a/testcases/lazy-datastructures/Conqueue.scala b/testcases/lazy-datastructures/Conqueue.scala
index 3d5ea675fde56caee5eae3423873ec29c79cb675..349157fc39d93832d1827b573f1270502ac5a046 100644
--- a/testcases/lazy-datastructures/Conqueue.scala
+++ b/testcases/lazy-datastructures/Conqueue.scala
@@ -389,6 +389,7 @@ object Conqueue {
} holds
// suffix predicates and their properties (this should be generalizable)
+
def suffix[T](q: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
if (q == suf) true
else {
@@ -400,15 +401,50 @@ object Conqueue {
}
}
- // TODO: this should be inferable from the model
- @axiom
def properSuffix[T](l: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
l* match {
case Spine(_, _, rear) =>
suffix(rear, suf)
case _ => false
}
- } ensuring (res => !res || suf != l)
+ } ensuring (res => !res || (suf != l &&
+ suffixDisequality(l, suf)))
+
+ /**
+ * suf(q, suf) ==> suf(q.rear, suf.rear)
+ */
+ def suffixTrans[T](q: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ require(suffix(q, suf))
+ // induction scheme
+ (if (q == suf) true
+ else {
+ q* match {
+ case Spine(_, _, rear) =>
+ suffixTrans(rear, suf)
+ case Tip(_) => true
+ }
+ }) && // property
+ ((q*, suf*) match {
+ case (Spine(_, _, rear), Spine(_, _, sufRear)) =>
+ // 'sufRear' should be a suffix of 'rear1'
+ suffix(rear, sufRear)
+ case _ => true
+ })
+ }.holds
+
+ /**
+ * properSuf(l, suf) ==> l != suf
+ */
+ def suffixDisequality[T](l: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ require(properSuffix(l, suf))
+ suffixTrans(l, suf) && // lemma instantiation
+ ((l*, suf*) match { // induction scheme
+ case (Spine(_, _, rear), Spine(_, _, sufRear)) =>
+ // 'sufRear' should be a suffix of 'rear1'
+ suffixDisequality(rear, sufRear)
+ case _ => true
+ }) && l != suf
+ }.holds
def suffixCompose[T](q: $[ConQ[T]], suf1: $[ConQ[T]], suf2: $[ConQ[T]]): Boolean = {
require(suffix(q, suf1) && properSuffix(suf1, suf2))
@@ -424,17 +460,6 @@ object Conqueue {
})
} holds
- // uncomment this once the model is fixed
- /*def suffixInEquality[T](l: LazyConQ[T], suf: LazyConQ[T], suf2: ) : Boolean = {
- require(properSuffix(l, suf))
- (l != suf) && (
- evalLazyConQS(l) match {
- case Spine(_, _, rear) =>
- suffixInEquality(rear, suf)
- case _ => false
- })
- }.holds*/
-
// properties of 'concUntil'
def concreteUntilIsSuffix[T](l: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {