Build a tree of logarithmic height from a list, in linear time, while preserving the order of elements

Author: Jean-Christophe Filliâtre (CNRS)

module TreeOfList

  use int.Int
  use int.ComputerDivision
  use int.Power
  use list.List
  use list.Append
  use list.Length
  use bintree.Tree
  use bintree.Size
  use bintree.Inorder
  use bintree.InorderLength
  use bintree.Height

  type elt

  let rec tree_of_list_aux (n: int) (l: list elt) : (tree elt, list elt)
    requires { 0 <= n <= length l }
    variant  { n }
    ensures  { let t, l' = result in
               inorder t ++ l' = l && size t = n &&
               (n > 0 -> let h = height t in power 2 (h-1) <= n < power 2 h) }
  =
    if n = 0 then
      Empty, l
    else
      let n = n - 1 in
      let n1 = div n 2 in
      let left, l = tree_of_list_aux n1 l in
      match l with
      | Nil -> absurd
      | Cons x l -> let right, l = tree_of_list_aux (n - n1) l in
                    Node left x right, l
      end

  let tree_of_list (l: list elt) : tree elt
    ensures { inorder result = l }
    ensures { size result > 0 -> let h = height result in
                power 2 (h-1) <= size result < power 2 h }
  =
    let t, l = tree_of_list_aux (length l) l in
    assert { l = Nil };
    t

end