From 9126073399c98f47bf2f57de5bbbe2f2a190262f Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Sun, 19 Apr 2015 00:40:10 +0200
Subject: [PATCH] A simple parallel merge sort testcase using 'parallel'

---
 library/collection/List.scala                 | 15 +++++++++++
 .../BasicMergeSort.scala}                     |  0
 .../list-algorithms/BasicMergeSortPar.scala   | 27 +++++++++++++++++++
 3 files changed, 42 insertions(+)
 rename testcases/verification/{sorting/MergeSort.scala => list-algorithms/BasicMergeSort.scala} (100%)
 create mode 100644 testcases/verification/list-algorithms/BasicMergeSortPar.scala

diff --git a/library/collection/List.scala b/library/collection/List.scala
index ef22189d7..436886cca 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -310,6 +310,21 @@ sealed abstract class List[T] {
     (take(c), drop(c))
   }
 
+  def splitAtIndex(index: BigInt) : (List[T], List[T]) = { this match {
+    case Nil() => (Nil[T](), Nil[T]())
+    case Cons(h, rest) => {
+      if (index <= BigInt(0)) {
+        (Nil[T](), this)
+      } else {
+        val (left,right) = rest.splitAtIndex(index - 1)
+        (Cons[T](h,left), right)
+      }
+    }
+  }} ensuring { (res:(List[T],List[T])) =>
+    res._1 ++ res._2 == this &&
+    res._1 == take(index) && res._2 == drop(index)
+  }
+
   def updated(i: BigInt, y: T): List[T] = {
     require(0 <= i && i < this.size)
     this match {
diff --git a/testcases/verification/sorting/MergeSort.scala b/testcases/verification/list-algorithms/BasicMergeSort.scala
similarity index 100%
rename from testcases/verification/sorting/MergeSort.scala
rename to testcases/verification/list-algorithms/BasicMergeSort.scala
diff --git a/testcases/verification/list-algorithms/BasicMergeSortPar.scala b/testcases/verification/list-algorithms/BasicMergeSortPar.scala
new file mode 100644
index 000000000..e5620482d
--- /dev/null
+++ b/testcases/verification/list-algorithms/BasicMergeSortPar.scala
@@ -0,0 +1,27 @@
+import leon.lang._
+import leon.collection._
+import leon.par._
+object MergeSortPar {
+
+  def merge[T](less: (T, T) => Boolean)(xs: List[T], ys: List[T]): List[T] = {
+    (xs, ys) match {
+      case (Nil(), _) => ys
+      case (_, Nil()) => xs
+      case (Cons(x,xtail), Cons(y,ytail)) =>
+        if (less(x, y))
+          x :: merge(less)(xtail, ys)
+        else
+          y :: merge(less)(xs, ytail)
+    }
+  } ensuring { res => res.content == xs.content ++ ys.content &&
+                      res.size == xs.size + ys.size }
+
+  def msort[T](less: (T, T) => Boolean)(l: List[T]): List[T] = {
+    if (l.size <= 1) l
+    else {
+      val (first, second) = l.evenSplit
+      val (s1, s2) = parallel(msort(less)(first), msort(less)(second))
+      merge(less)(s1, s2)
+    }
+  } ensuring { res => res.content == l.content && res.size == l.size }
+}
-- 
GitLab