From c3d24e422b220d1499a3f12b3e7f11e8f9cf1323 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 20 Jul 2015 19:16:05 +0200
Subject: [PATCH] Make List API scala compatible, add @library
---
doc/library.rst | 2 +-
library/collection/List.scala | 14 ++------------
2 files changed, 3 insertions(+), 13 deletions(-)
diff --git a/doc/library.rst b/doc/library.rst
index 8708e5a74..a165c0a6b 100644
--- a/doc/library.rst
+++ b/doc/library.rst
@@ -143,7 +143,7 @@ Leon Lists support a rich and strongly specified API.
+---------------------------------------------------+---------------------------------------------------+
| ``lastOption: Option[T]`` | Optionally return the last element of this List. |
+---------------------------------------------------+---------------------------------------------------+
-| ``firstOption: Option[T]`` | Optionally return the first element of this List. |
+| ``headOption: Option[T]`` | Optionally return the first element of this List. |
+---------------------------------------------------+---------------------------------------------------+
| ``unique: List[T]`` | Return this List without duplicates. |
+---------------------------------------------------+---------------------------------------------------+
diff --git a/library/collection/List.scala b/library/collection/List.scala
index d9031e8b7..404c53c44 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -35,17 +35,6 @@ sealed abstract class List[T] {
(that != Nil[T]() || res == this)
}
- def headOption: Option[T] = this match {
- case Nil() => None[T]()
- case Cons(h, _) => Some(h)
- }
-
- val tailOption: Option[List[T]] = this match {
- case Nil() => None[List[T]]()
- case Cons(_, t) => Some(t)
- }
-
-
def head: T = {
require(this != Nil[T]())
val Cons(h, _) = this
@@ -268,7 +257,7 @@ sealed abstract class List[T] {
None[T]()
}} ensuring { _.isDefined != this.isEmpty }
- def firstOption: Option[T] = { this match {
+ def headOption: Option[T] = { this match {
case Cons(h, t) =>
Some(h)
case Nil() =>
@@ -550,6 +539,7 @@ case class Nil[T]() extends List[T]
// 'Cons' Extractor
object :: {
+ @library
def unapply[A](l: List[A]): Option[(A, List[A])] = l match {
case Nil() => None()
case Cons(x, xs) => Some((x, xs))
--
GitLab