From b66665a0f46101f9a3b9667690db095f3889975c Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 23 Feb 2015 21:32:02 +0100
Subject: [PATCH] Scans in library
---
library/collection/List.scala | 25 +++++++++++++++++++++++++
1 file changed, 25 insertions(+)
diff --git a/library/collection/List.scala b/library/collection/List.scala
index a35e027c4..8e10e0d35 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -330,6 +330,18 @@ sealed abstract class List[T] {
case Nil() => z
case Cons(h, t) => f(h, t.foldRight(f)(z))
}
+
+ 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)
+ }
+
+ def scanRight[R](f: (T,R) => R)(z: R): List[R] = { this match {
+ case Nil() => z :: Nil()
+ case Cons(h, t) =>
+ val rest@Cons(h1,_) = t.scanRight(f)(z)
+ f(h, h1) :: rest
+ }} ensuring { !_.isEmpty }
def flatMap[R](f: T => List[R]): List[R] =
ListOps.flatten(this map f)
@@ -502,4 +514,17 @@ object ListSpecs {
// }} &&
// l.foldLeft(z)(f) == l.reverse.foldRight((x:T,y:R) => f(y,x))(z)
//}.holds
+ //
+
+ //Can't prove this
+ //@induct
+ //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(f)(z).head == l.foldRight(f)(z)
+ }.holds
+
}
--
GitLab