// Now we see why it was worth defining all of the above.  When we *don't* know
// that a tree is a binary search tree, we need a less "linear" membership
// check, which we handle through explicitly representing a *stack* of pending
// trees to search.
method TreeMemberLoop(x: int, t: Tree) returns (b: bool)
  ensures b == TreeMember(x, t)
/*{
  var trs := Cons(t, Nil);
  // Here is our stack, which mirrors the call stack in traditional
  // implementations of recursive functions.  For instance, a Python interpreter
  // internally maintains a call stack but hides it from the programmer.
  // Initially, we have a single "call" on the stack, on the original tree.

  while trs.Cons?
  {
    var tr := trs.hd;
    trs := trs.tl;

    // So we pop tr off of the stack and need to handle it properly.
    // If it is a Leaf, there is nothing more to do.  However....
    if tr.Node? {
      // OK, the node we're handling is nonempty.
      if x == tr.data {
        // It happens to contain x at its root.  Done.
        return true;
      } else {
        // Didn't find x yet?  Queue up "recursive calls" to the left and right
        // children.  That is, push them onto the stack.
        trs := Cons(tr.left, Cons(tr.right, trs));
      }
    }
  }

  return false;
}*/

// Here are other definitions from our running code that will (or will probably) be relevant.

datatype List<T> = Nil | Cons(hd: T, tl: List<T>)

function Length<T>(ls: List<T>): nat {
  match ls
  case Nil => 0
  case Cons(_, ls') => 1 + Length(ls')
}
predicate Member<T(==)>(x: T, ls: List<T>) {
  match ls
  case Nil => false
  case Cons(y, ls') => y == x || Member(x, ls')
}

// So lists weren't so bad to work with.  How about binary trees?

datatype Tree = Leaf | Node(left: Tree, data: int, right: Tree)

predicate TreeMember(x: int, t: Tree) {
  match t
  case Leaf => false
  case Node(left, data, right) => TreeMember(x, left) || data == x || TreeMember(x, right)
}

// This mysterious pair of functions is the heart of the termination argument
// for our next example.

ghost function Size(t: Tree): nat {
  match t
  case Leaf => 0
  case Node(left, _, right) => Size(left) + 2 + Size(right)
}

ghost function Sizes(ls: List<Tree>): nat {
  match ls
  case Nil => 0
  case Cons(hd, tl) => Size(hd) + 1 + Sizes(tl)
}

// We also define what it means for a data value to be found within a list of
// trees.
ghost predicate TreesMember(x: int, trs: List<Tree>) {
  exists t :: Member(t, trs) && TreeMember(x, t)
}