From 1b3766a2f1abc532b8a3a838727a77e63ed3dc45 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 26 Aug 2015 14:30:07 +0200
Subject: [PATCH] Some extra library methods
---
library/collection/List.scala | 29 ++++++++++++++++++++++++++---
library/lang/Option.scala | 15 +++++++++++++--
2 files changed, 39 insertions(+), 5 deletions(-)
diff --git a/library/collection/List.scala b/library/collection/List.scala
index 399ef5b83..0fc2d4f84 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -380,6 +380,8 @@ sealed abstract class List[T] {
case _ => false
}
+ def nonEmpty = !isEmpty
+
// Higher-order API
def map[R](f: T => R): List[R] = { this match {
case Nil() => Nil[R]()
@@ -493,8 +495,28 @@ sealed abstract class List[T] {
_ == this.filter(p).size
}
+ def indexWhere(p: T => Boolean): BigInt = { this match {
+ case Nil() => BigInt(-1)
+ case Cons(h, _) if p(h) => BigInt(0)
+ case Cons(_, t) =>
+ val rec = t.indexWhere(p)
+ if (rec >= 0) rec + BigInt(1)
+ else BigInt(-1)
+ }} ensuring {
+ _ >= BigInt(0) == (this exists p)
+ }
+
+
+ // Translation to other collections
+ def toSet: Set[T] = foldLeft(Set[T]()){
+ case (current, next) => current ++ Set(next)
+ }
+
}
+case class Cons[T](h: T, t: List[T]) extends List[T]
+case class Nil[T]() extends List[T]
+
object List {
@ignore
def apply[T](elems: T*): List[T] = {
@@ -544,10 +566,11 @@ object ListOps {
}
}
} ensuring { isSorted _ }
-}
-case class Cons[T](h: T, t: List[T]) extends List[T]
-case class Nil[T]() extends List[T]
+ def toMap[K, V](l: List[(K, V)]): Map[K, V] = l.foldLeft(Map[K, V]()){
+ case (current, (k, v)) => current ++ Map(k -> v)
+ }
+}
// 'Cons' Extractor
object :: {
diff --git a/library/lang/Option.scala b/library/lang/Option.scala
index 75e018a39..0efcc4aba 100644
--- a/library/lang/Option.scala
+++ b/library/lang/Option.scala
@@ -3,6 +3,7 @@
package leon.lang
import leon.annotation._
+import leon.collection._
@library
sealed abstract class Option[T] {
@@ -19,11 +20,11 @@ sealed abstract class Option[T] {
case None() => default
}
- def orElse(or: Option[T]) = {this match {
+ def orElse(or: Option[T]) = { this match {
case Some(v) => this
case None() => or
}} ensuring {
- res => (this.isDefined || or.isDefined) == res.isDefined
+ _.isDefined == this.isDefined || or.isDefined
}
def isEmpty = this match {
@@ -61,6 +62,16 @@ sealed abstract class Option[T] {
def exists(p: T => Boolean) = !forall(!p(_))
+ // Transformation to other collections
+ def toList: List[T] = this match {
+ case None() => Nil[T]()
+ case Some(x) => List(x)
+ }
+
+ def toSet: Set[T] = this match {
+ case None() => Set[T]()
+ case Some(x) => Set(x)
+ }
}
case class Some[T](v: T) extends Option[T]
--
GitLab