LARA

import leon.Utils._

/**
 * Code should be contained in a single top-level object 
 */
object Test1 {

  /**
   * You can define Algebraic Data Types using abstract classes and case classes.
   */
  abstract class List
  case class Cons(head: Int, tail: List) extends List
  case class Nil() extends List


  def size(l: List): Int = (l match {
    case Nil() => 0
    case Cons(h, t) => 1+size(t)
  }) ensuring { _ >= 0 }

  def contains(l: List, v: Int): Boolean = (l match {
    case Nil() => false
    case Cons(h, t) => v == h || contains(t, v)
  }) ensuring { res => time < 7*(size(l)+3) }

  abstract class Tree
  case class Node(l: Tree, v: Int, r: Tree) extends Tree
  case class Leaf() extends Tree

  def treeHeight(t: Tree): Int = (t match {
    case Node(l, v, r) =>
      val lh = treeHeight(l)
      val rh = treeHeight(r)
      if (lh > rh) 1 + lh else 1 + rh
    case Leaf() =>
      0
  }) ensuring { _ >=  0 }

  def treeSize(t: Tree): Int = (t match {
    case Node(l, v, r) =>
      1 + treeSize(l) + treeSize(r)
    case Leaf() =>
      0
  }) ensuring { _ >=  0 }

  def treeContains(t: Tree, v: Int): Boolean = (t match {
    case Node(l, v2, r) =>
      v == v2 || treeContains(l, v) || treeContains(r, v)
    case Leaf() =>
      false
  }) ensuring{ res => time < treeSize(t)*10+2 }

  def treeLeftMost(t: Tree): Int = (t match {
    case Node(l, v, r) =>
      l match {
        case Leaf() =>
          v
        case _ =>
          treeLeftMost(l)
      }
    case Leaf() =>
      -1
  }) ensuring{ res => time < treeHeight(t)*10+10 }

  def treeContains0(t: Tree): Boolean = {
    treeContains(t, 0)
  } ensuring{ res => time < treeSize(t)*10+3 }

}