// This file defines some functions that we ask you to prove lemmas about.
// Please don't modify it or turn it in.

module Defs {
  datatype List<T> = Nil | Cons(head: T, tail: List<T>)

  function Length<T>(l: List<T>): nat {
    match l
    case Nil => 0
    case Cons(_, l') => 1 + Length(l')
  }

  type Binary = List<bool>

  datatype BTrie = Leaf(included: bool) | Node(included: bool, left: BTrie, right: BTrie)

  predicate Member(b: Binary, t: BTrie) {
    match t
    case Leaf(inc) => inc && b == Nil
    case Node(inc, left, right) =>
      match b
      case Nil => inc
      case Cons(false, b') => Member(b', left)
      case Cons(true, b') => Member(b', right)
  }

  datatype Option<T> = None | Some(value: T)

  // Here is a generic version of tries, identical to BTrie save for the type of
  // value associated with a key.  The prior version implicitly represented sets
  // as dictionaries mapping to Booleans.
  datatype GTrie<T> = GLeaf(value: T) | GNode(value: T, left: GTrie<T>, right: GTrie<T>)

  function Or(a: bool, b: bool): bool
  {
    a || b
  }

  function Max(a: nat, b: nat): nat {
    if a < b then b else a
  }

  function Depth<T>(gt: GTrie<T>): nat {
    match gt
    case GLeaf(_) => 0
    case GNode(_, gt1, gt2) => 1 + Max(Depth(gt1), Depth(gt2))
  }

  function FuncComposition<T>(x: (T -> T), y: (T -> T)): (T -> T) { z => y(x(z)) }
}