import stainless.proof._
import stainless.lang._
import stainless.collection._

object QuickSort {

  def listmin(l: List[BigInt]): (Boolean,BigInt) = {
    l match {
      case Nil() =>
        (false,0)
      case Cons(x,xs) =>
        val (isDef,xsmin) = listmin(xs)
        val lMin = if(isDef) { if(x<xsmin) x else xsmin } else x
        (true,lMin)
    }
  }

  def listmax(l: List[BigInt]): (Boolean,BigInt) = {
    l match {
      case Nil() =>
        (false,0)
      case Cons(x,xs) =>
        val (isDef,xsmax) = listmax(xs)
        val lMax = if(isDef) { if(x>xsmax) x else xsmax } else x
        (true,lMax)
    }
  }

  def isASorted(l: List[BigInt]): Boolean = {
    l match {
      case Nil() =>
        true
      case Cons(x, xs) =>
        val (isDef,xsh) = hd(xs)
        !isDef || ( x<=xsh && isASorted(xs) )
    }
  }

  def hd(l: List[BigInt]): (Boolean,BigInt) = {
    l match {
      case Nil() =>
        (false,0)
      case Cons(x,_) =>
        (true, x)
    }
  }

  def quickSort(l: List[BigInt]) : List[BigInt] = {
    decreases(l.size, BigInt(0))
    l match {
      case Nil() =>
        Nil[BigInt]()
      case Cons(x, xs) =>
        val (ys,zs) = partition(x, xs)
        concat(quickSort(ys), x, quickSort(zs))
    }
  } ensuring { res => isASorted(res) }

  def partition(p: BigInt, xs: List[BigInt]) : ( List[BigInt], List[BigInt] ) = {
    xs match {
      case Nil() =>
        ( Nil[BigInt](), Nil[BigInt]() )
      case Cons(y, ys) =>
        val (l1,l2) = partition(p,ys)
        if(p>y)
          { ( Cons(y,l1), l2 ) }
        else
          { ( l1, Cons(y,l2) ) }
    }
  } ensuring { res  =>
    val ls = res._1
    val bs = res._2
    val (isDefMinXs,minXs) = listmin(xs)
    val (isDefMinLs,minLs) = listmin(ls)
    val (isDefMinBs,minBs) = listmin(bs)
    val (isDefMaxXs,maxXs) = listmax(xs)
    val (isDefMaxLs,maxLs) = listmax(ls)
    val (isDefMaxBs,maxBs) = listmax(bs)
    ((isDefMinLs && isDefMaxLs && isDefMinXs) ==> (p>maxLs  && minXs==minLs)) &&
    ((isDefMinBs && isDefMaxBs && isDefMaxXs) ==> (p<=maxBs && maxXs==maxBs)) &&
    isDefMinXs == (isDefMinLs || isDefMinBs) &&
    isDefMaxXs == (isDefMaxLs || isDefMaxBs)
  }

  def concat(xs: List[BigInt], y: BigInt, ys: List[BigInt]) : List[BigInt] = {
    require(
      isASorted(xs) && isASorted(ys) &&
      ( listmax(xs)._1 ==> (listmax(xs)._2 <= y) ) &&
      ( listmin(ys)._1 ==> (y <= listmin(ys)._2) )
    )
    xs match {
      case Nil() =>
        Cons(y, ys)
      case Cons(l, ls) =>
        Cons(l, concat(ls,y,ys))
    }
  } ensuring { res => isASorted(res) }

}