content: module AmortizedQueue where
  
  import Prelude hiding (head)
  
  data AbsQueue a = AQ { front :: [a]
                       , rear  :: [a] }
  
  {-@ data AbsQueue a = AQ { front :: [a]
                           , rear  :: {v:[a] | size v <= size front} }  @-}
  
  {-@ die :: {v:String | false} -> a @-}
  die :: String -> a
  die x = error x
  
  {-@ measure size @-}
  size        :: [a] -> Int
  size []     = 0
  size (x:xs) = 1 + size xs
  
  {-@ measure qsize @-}
  qsize            :: AbsQueue a -> Int
  qsize (AQ xs ys) = size xs + size ys
  
  {-@ invariant {v:[a]        | size v >=  0} @-}
  {-@ invariant {v:AbsQueue a | qsize v >= 0} @-}
  
  {-@ type NEList  a = {v:[a]        | size v > 0} @-}
  {-@ type NEQueue a = {v:AbsQueue a | qsize v > 0} @-}
  
  
  makeQueue            :: [a] -> [a] -> AbsQueue a
  makeQueue f b
    | size b <= size f = AQ f b
    | otherwise        = AQ (f ++ reverse b) []
  
                         
  {- measure qhead @-}
  
  {-@ qhead      :: NEQueue a -> a @-}
  qhead (AQ f _) = head f
  qhead _        = die "never"
  
  {- measure head @-}
  
  {-@ head   :: NEList a -> a @-}
  head (x:_) = x
  -- head _     = die "never"
  
  
  {- toList :: q:AbsQueue a -> {v:[a] | 0 < len v => head v = front q} @-}
  toList :: AbsQueue a -> [a]
  toList = undefined 
  -- forall q :: AbsQueue a, xs:: [a], x::a.
  --    not (isEmpty(q)) && asList(q) == xs =>                    
  {-
  import leon.lang._
  import leon.annotation._
  
  object AmortizedQueue {
    sealed abstract class List
    case class Cons(head : Int, tail : List) extends List
    case object Nil extends List
  
    sealed abstract class AbsQueue
    case class Queue(front : List, rear : List) extends AbsQueue
  
    def size(list : List) : Int = (list match {
      case Nil => 0
      case Cons(_, xs) => 1 + size(xs)
    }) ensuring(_ >= 0)
  
    def content(l: List) : Set[Int] = l match {
      case Nil => Set.empty[Int]
      case Cons(x, xs) => Set(x) ++ content(xs)
    }
    
    def asList(queue : AbsQueue) : List = queue match {
      case Queue(front, rear) => concat(front, reverse(rear))
    }
  
    def concat(l1 : List, l2 : List) : List = (l1 match {
      case Nil => l2
      case Cons(x,xs) => Cons(x, concat(xs, l2))
    }) ensuring (res => size(res) == size(l1) + size(l2) && content(res) == content(l1) ++ content(l2))
  
    def isAmortized(queue : AbsQueue) : Boolean = queue match {
      case Queue(front, rear) => size(front) >= size(rear)
    }
  
    def isEmpty(queue : AbsQueue) : Boolean = queue match {
      case Queue(Nil, Nil) => true
      case _ => false
    }
  
    def reverse(l : List) : List = (l match {
      case Nil => Nil
      case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil))
    }) ensuring (content(_) == content(l))
  
    def amortizedQueue(front : List, rear : List) : AbsQueue = {
      if (size(rear) <= size(front))
        Queue(front, rear)
      else
        Queue(concat(front, reverse(rear)), Nil)
    } ensuring(isAmortized(_))
  
    def enqueue(queue : AbsQueue, elem : Int) : AbsQueue = (queue match {
      case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear))
    }) ensuring(isAmortized(_))
  
    def tail(queue : AbsQueue) : AbsQueue = {
      require(isAmortized(queue) && !isEmpty(queue))
      queue match {
        case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear)
      }
    } ensuring (isAmortized(_))
  
    def front(queue : AbsQueue) : Int = {
      require(isAmortized(queue) && !isEmpty(queue))
      queue match {
        case Queue(Cons(f, _), _) => f
      }
    }
  
    @induct
    def propFront(queue : AbsQueue, list : List) : Boolean = {
      require(!isEmpty(queue) && isAmortized(queue))
      if (asList(queue) == list) {
        list match {
          case Cons(x, _) => front(queue) == x
        }
      } else
        true
    } holds
  
    def enqueueAndFront(queue : AbsQueue, elem : Int) : Boolean = {
      if (isEmpty(queue))
        front(enqueue(queue, elem)) == elem
      else
        true
    } holds
  
    def enqueueDequeueThrice(queue : AbsQueue, e1 : Int, e2 : Int, e3 : Int) : Boolean = {
      if (isEmpty(queue)) {
        val q1 = enqueue(queue, e1)
        val q2 = enqueue(q1, e2)
        val q3 = enqueue(q2, e3)
        val e1prime = front(q3)
        val q4 = tail(q3)
        val e2prime = front(q4)
        val q5 = tail(q4)
        val e3prime = front(q5)
        e1 == e1prime && e2 == e2prime && e3 == e3prime
      } else
        true
    } holds
  }
  
  -}
  