Skip to content
Snippets Groups Projects
Commit f500a66b authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Enrich/correct/make leon lib. compatible with Scala

parent 961072ec
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
library/collection/List.scala
+ 139
− 63
View file @ f500a66b
......@@ -5,6 +5,7 @@ package leon.collection
import leon._
import leon.lang._
import leon.annotation._
import leon.math._
@library
sealed abstract class List[T] {
......@@ -23,12 +24,12 @@ sealed abstract class List[T] {
case Cons(h, t) if h == v => true
case Cons(_, t) => t.contains(v)
case Nil() => false
}) ensuring { res => res == (content contains v) }
}) ensuring { _ == (content contains v) }
def ++(that: List[T]): List[T] = (this match {
case Nil() => that
case Cons(x, xs) => Cons(x, xs ++ that)
}) ensuring { res =>
}) ensuring { res =>
(res.content == this.content ++ that.content) &&
(res.size == this.size + that.size)
}
......@@ -50,7 +51,7 @@ sealed abstract class List[T] {
if (index == BigInt(0)) {
head
} else {
tail(index-1)
tail(index-1)
}
}
......@@ -78,11 +79,13 @@ sealed abstract class List[T] {
} else {
Cons(h, t.take(i-1))
}
}} ensuring { _.size == (
if (i <= 0) BigInt(0)
else if (i >= this.size) this.size
else i
)}
}} ensuring { res =>
res.content.subsetOf(this.content) && (res.size == (
if (i <= 0) BigInt(0)
else if (i >= this.size) this.size
else i
))
}
def drop(i: BigInt): List[T] = { (this, i) match {
case (Nil(), _) => Nil[T]()
......@@ -92,11 +95,13 @@ sealed abstract class List[T] {
} else {
t.drop(i-1)
}
}} ensuring { _.size == (
if (i <= 0) this.size
else if (i >= this.size) BigInt(0)
else this.size - i
)}
}} ensuring { res =>
res.content.subsetOf(this.content) && (res.size == (
if (i <= 0) this.size
else if (i >= this.size) BigInt(0)
else this.size - i
))
}
def slice(from: BigInt, to: BigInt): List[T] = {
require(0 <= from && from <= to && to <= size)
......@@ -159,7 +164,10 @@ sealed abstract class List[T] {
}
case Nil() =>
Nil[T]()
}} ensuring { _.content == this.content -- Set(e) }
}} ensuring { res =>
res.size <= this.size &&
res.content == this.content -- Set(e)
}
def --(that: List[T]): List[T] = { this match {
case Cons(h, t) =>
......@@ -170,7 +178,10 @@ sealed abstract class List[T] {
}
case Nil() =>
Nil[T]()
}} ensuring { _.content == this.content -- that.content }
}} ensuring { res =>
res.size <= this.size &&
res.content == this.content -- that.content
}
def &(that: List[T]): List[T] = { this match {
case Cons(h, t) =>
......@@ -181,15 +192,24 @@ sealed abstract class List[T] {
}
case Nil() =>
Nil[T]()
}} ensuring { _.content == (this.content & that.content) }
}} ensuring { res =>
res.size <= this.size &&
res.content == (this.content & that.content)
}
def pad(s: BigInt, e: T): List[T] = (this, s) match {
def padTo(s: BigInt, e: T): List[T] = { (this, s) match {
case (_, s) if s <= 0 =>
this
case (Nil(), s) =>
Cons(e, Nil().pad(s-1, e))
Cons(e, Nil().padTo(s-1, e))
case (Cons(h, t), s) =>
Cons(h, t.pad(s-1, e))
Cons(h, t.padTo(s-1, e))
}} ensuring { res =>
if (s <= this.size)
res == this
else
res.size == s &&
res.content == this.content ++ Set(e)
}
def find(e: T): Option[BigInt] = { this match {
......@@ -203,16 +223,20 @@ sealed abstract class List[T] {
case Some(i) => Some(i+1)
}
}
}} ensuring { (res: Option[BigInt]) => res.isDefined == this.contains(e) }
}} ensuring { _.isDefined == this.contains(e) }
def init: List[T] = (this match {
case Cons(h, Nil()) =>
Nil[T]()
case Cons(h, t) =>
Cons[T](h, t.init)
case Nil() =>
Nil[T]()
}) ensuring ( (r: List[T]) => ((r.size < this.size) || (this.size == BigInt(0))) )
def init: List[T] = {
require(!isEmpty)
(this match {
case Cons(h, Nil()) =>
Nil[T]()
case Cons(h, t) =>
Cons[T](h, t.init)
})
} ensuring ( (r: List[T]) =>
r.size == this.size - 1 &&
r.content.subsetOf(this.content)
)
def last: T = {
require(!isEmpty)
......@@ -220,21 +244,21 @@ sealed abstract class List[T] {
case Cons(h, Nil()) => h
case Cons(_, t) => t.last
}
}
} ensuring { this.contains _ }
def lastOption: Option[T] = this match {
def lastOption: Option[T] = { this match {
case Cons(h, t) =>
t.lastOption.orElse(Some(h))
case Nil() =>
None()
}
}} ensuring { _.isDefined != this.isEmpty }
def firstOption: Option[T] = this match {
def firstOption: Option[T] = { this match {
case Cons(h, t) =>
Some(h)
case Nil() =>
None()
}
}} ensuring { _.isDefined != this.isEmpty }
def unique: List[T] = this match {
case Nil() => Nil()
......@@ -256,17 +280,6 @@ sealed abstract class List[T] {
Cons(Nil(), Nil())
}
def count(e: T): BigInt = this match {
case Cons(h, t) =>
if (h == e) {
1 + t.count(e)
} else {
t.count(e)
}
case Nil() =>
BigInt(0)
}
def evenSplit: (List[T], List[T]) = {
val c = size/2
(take(c), drop(c))
......@@ -285,6 +298,9 @@ sealed abstract class List[T] {
l
}
}
} ensuring { res =>
res.size == this.size + l.size &&
res.content == this.content ++ l.content
}
def replaceAt(pos: BigInt, l: List[T]): List[T] = {
......@@ -300,15 +316,20 @@ sealed abstract class List[T] {
l
}
}
} ensuring { res =>
res.content.subsetOf(l.content ++ this.content)
}
def rotate(s: BigInt): List[T] = {
if (s < 0) {
rotate(size+s)
rotate(size + s)
} else if (s > size) {
rotate(s - size)
} else {
val s2 = s % size
drop(s2) ++ take(s2)
drop(s) ++ take(s)
}
} ensuring { res =>
res.size == this.size
}
def isEmpty = this match {
......@@ -320,7 +341,7 @@ sealed abstract class List[T] {
def map[R](f: T => R): List[R] = { this match {
case Nil() => Nil[R]()
case Cons(h, t) => f(h) :: t.map(f)
}} ensuring { _.size == this.size}
}} ensuring { _.size == this.size }
def foldLeft[R](z: R)(f: (R,T) => R): R = this match {
case Nil() => z
......@@ -332,10 +353,10 @@ sealed abstract class List[T] {
case Cons(h, t) => f(h, t.foldRight(z)(f))
}
def scanLeft[R](z: R)(f: (R,T) => R): List[R] = this match {
def scanLeft[R](z: R)(f: (R,T) => R): List[R] = { this match {
case Nil() => z :: Nil()
case Cons(h,t) => z :: t.scanLeft(f(z,h))(f)
}
}} ensuring { !_.isEmpty }
def scanRight[R](z: R)(f: (T,R) => R): List[R] = { this match {
case Nil() => z :: Nil[R]()
......@@ -351,7 +372,29 @@ sealed abstract class List[T] {
case Nil() => Nil[T]()
case Cons(h, t) if p(h) => Cons(h, t.filter(p))
case Cons(_, t) => t.filter(p)
}} ensuring { res => res.size <= this.size && res.forall(p) }
}} ensuring { res =>
res.size <= this.size &&
res.content.subsetOf(this.content) &&
res.forall(p)
}
def filterNot(p: T => Boolean): List[T] =
filter(!p(_)) ensuring { res =>
res.size <= this.size &&
res.content.subsetOf(this.content) &&
res.forall(!p(_))
}
def partition(p: T => Boolean): (List[T], List[T]) = { this match {
case Nil() => (Nil[T](), Nil[T]())
case Cons(h, t) =>
val (l1, l2) = t.partition(p)
if (p(h)) (h :: l1, l2)
else (l1, h :: l2)
}} ensuring { res =>
res._1 == filter(p) &&
res._2 == filterNot(p)
}
// In case we implement for-comprehensions
def withFilter(p: T => Boolean) = filter(p)
......@@ -369,20 +412,41 @@ sealed abstract class List[T] {
case Cons(_, t) => t.find(p)
}} ensuring { _.isDefined == exists(p) }
// FIXME: I keep getting these weird type errors
//def groupBy[R](f: T => R): Map[R, List[T]] = this match {
// case Nil() => Map.empty[R, List[T]]
// case Cons(h, t) =>
// val key: R = f(h)
// val rest: Map[R, List[T]] = t.groupBy(f)
// val prev: List[T] = if (rest isDefinedAt key) rest(key) else Nil[T]()
// (rest ++ Map((key, h :: prev))) : Map[R, List[T]]
//}
def groupBy[R](f: T => R): Map[R, List[T]] = this match {
case Nil() => Map.empty[R, List[T]]
case Cons(h, t) =>
val key: R = f(h)
val rest: Map[R, List[T]] = t.groupBy(f)
val prev: List[T] = if (rest isDefinedAt key) rest(key) else Nil[T]()
(rest ++ Map((key, h :: prev))) : Map[R, List[T]]
}
def takeWhile(p: T => Boolean): List[T] = { this match {
case Cons(h,t) if p(h) => Cons(h, t.takeWhile(p))
case _ => Nil[T]()
}} ensuring { _ forall p }
}} ensuring { res =>
(res forall p) &&
(res.size <= this.size) &&
(res.content subsetOf this.content)
}
def dropWhile(p: T => Boolean): List[T] = { this match {
case Cons(h,t) if p(h) => t.dropWhile(p)
case _ => this
}} ensuring { res =>
(res.size <= this.size) &&
(res.content subsetOf this.content) &&
(res.isEmpty || !p(res.head))
}
def count(p: T => Boolean): BigInt = { this match {
case Nil() => BigInt(0)
case Cons(h, t) =>
(if (p(h)) BigInt(1) else BigInt(0)) + t.count(p)
}} ensuring {
_ == this.filter(p).size
}
}
@ignore
......@@ -506,7 +570,19 @@ object ListSpecs {
// }) &&
// ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
//}.holds
//def associative[T,U](l1: List[T], l2: List[T], f: List[T] => U, op: (U,U) => U) = {
// f(l1 ++ l2) == op(f(l1), f(l2))
//}
//
//def existsAssoc[T](l1: List[T], l2: List[T], p: T => Boolean) = {
// associative[T, Boolean](l1, l2, _.exists(p), _ || _ )
//}.holds
//
//def forallAssoc[T](l1: List[T], l2: List[T], p: T => Boolean) = {
// associative[T, Boolean](l1, l2, _.exists(p), _ && _ )
//}.holds
//@induct
//def folds[T,R](l : List[T], z : R, f : (R,T) => R) = {
// { l match {
......@@ -522,7 +598,7 @@ object ListSpecs {
//def scanVsFoldLeft[A,B](l : List[A], z: B, f: (B,A) => B): Boolean = {
// l.scanLeft(z)(f).last == l.foldLeft(z)(f)
//}.holds
@induct
def scanVsFoldRight[A,B](l: List[A], z: B, f: (A,B) => B): Boolean = {
l.scanRight(z)(f).head == l.foldRight(z)(f)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment