Some extra library methods

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 :: {

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]