Skip to content

Commit 1f588a7

Browse files
committed
Add Traversable#collectFirst as required by Silicon
1 parent db6f852 commit 1f588a7

1 file changed

Lines changed: 13 additions & 2 deletions

File tree

src/main/scala/viper/silver/ast/utility/Traversable.scala

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,19 @@ trait Traversable[+A] {
3030
override def withFilter(q: A => Boolean): WithFilter = new WithFilter(x => p(x) && q(x))
3131
}
3232

33-
/**
34-
* Builds a new collection by applying a partial function to all elements of this collection on which the function
33+
/** Finds the first element of the $coll for which the given partial
34+
* function is defined, and applies the partial function to it.
35+
*/
36+
def collectFirst[B](pf: PartialFunction[A, B]): Option[B] = {
37+
for (x <- self) {
38+
if (pf.isDefinedAt(x)) {
39+
return Some(pf(x))
40+
}
41+
}
42+
None
43+
}
44+
45+
/** Builds a new collection by applying a partial function to all elements of this collection on which the function
3546
* is defined.
3647
*/
3748
def collect[B](pf: PartialFunction[A, B]): Iterable[B] = {

0 commit comments

Comments
 (0)