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

object Rev {

  def rev(l: List[BigInt]): List[BigInt] = {
    require(is_asorted(l))                 // rev precondition
    l match {
      case Nil() => Nil[BigInt]()
      case Cons(x, xs) => snoc(rev(xs),x)
    }
  } ensuring { res => is_dsorted(res) }     // rev postcondition

  def snoc(l: List[BigInt], x:BigInt): List[BigInt] = {
    require(is_dsorted(l) && leq_all(x,l)) // snoc precondition
    l match {
      case Nil() => Cons(x,Nil())
      case Cons(y, ys) => Cons(y,snoc(ys,x))
    }
  } ensuring { res => is_dsorted(res) }     // snoc postcondition

  def leq_all(x: BigInt, l: List[BigInt]): Boolean = {
    // for each y in the list l, x =< y
    l match {
      case Nil() => true
      case Cons(y, ys) => if (x > y) {false} else { leq_all(x, ys) }
    }
  }

  def is_asorted(l: List[BigInt]): Boolean = { // true if l is weakly ascending ordered
    l match {
      case Nil() => true
      case Cons(x,xs) => xs.isEmpty || (x <= xs.head && is_asorted(xs))
    }
  }

  def is_dsorted(l: List[BigInt]): Boolean = { // true if l is weakly descending ordered
    l match {
      case Nil() => true
      case Cons(x,xs) => xs.isEmpty || (x >= xs.head && is_dsorted(xs))
    }
  }
}