Stack.scala

import leon.lang._
import leon.collection._

abstract class Stack[T] {
  def empty : Stack[T]
  def pop : (Option[T], Stack[T])
  def push (e : T) : Stack[T]
  def size : BigInt
}

object StackSpec {
  // ok
  def test_v1[T] (e : T, s : Stack[T]) : Boolean = {
    s.push(e).pop._1 match {
      case Some(e2) => e == e2
      case _        => false
   }
  }.holds

  // failed
  def test_v2[T] (e : T, s : Stack[T]) : Boolean = {
    s.push(e).pop._1 == Some(e)
  }.holds

  // ok
  def test_v3[T] (e : T, s : ListStack[T]) : Boolean = {
    s.push(e).pop._1 == Some(e)
  }.holds

  // ok
  def test_v4 (e : Int, s : IntStack) : Boolean = {
    s.push(e).pop._1 == Some(e)
  }.holds

}

abstract class IntStack {
  def empty : IntStack
  def pop : (Option[Int], IntStack)
  def push (e : Int) : IntStack
  def size : BigInt
}

case class ListStack[T](s : List[T]) extends Stack[T] {
  def empty : ListStack[T] = ListStack(Nil[T]())

  def pop : (Option[T], ListStack[T]) = {
    s match {
      case Nil() => (None[T](), this)
      case h::t  => (Some[T](h), ListStack(t))
    }
  }
  def push (e : T) : ListStack[T] = {
    ListStack(e :: s)
  }
  def size : BigInt = s.size
}

case class ListIntStack(s : List[Int]) extends IntStack {
  def empty : ListIntStack = ListIntStack(Nil[Int]())

  def pop : (Option[Int], ListIntStack) = {
    s match {
      case Nil() => (None[Int](), this)
      case h::t  => (Some[Int](h), ListIntStack(t))
    }
  }
  def push (e : Int) : ListIntStack = {
    ListIntStack(e :: s)
  }
  def size : BigInt = s.size
}