tree_of_list.mlw 1.26 KB
Newer Older
1 2 3 4 5 6 7 8 9

(** 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

10 11 12 13 14 15 16 17 18 19 20
  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
21 22 23 24 25 26

  type elt

  let rec tree_of_list_aux (n: int) (l: list elt) : (tree elt, list elt)
    requires { 0 <= n <= length l }
    variant  { n }
27
    ensures  { let t, l' = result in
28
               inorder t ++ l' = l && size t = n &&
MARCHE Claude's avatar
MARCHE Claude committed
29
               (n > 0 -> let h = height t in power 2 (h-1) <= n < power 2 h) }
30 31
  =
    if n = 0 then
32
      Empty, l
33 34 35
    else
      let n = n - 1 in
      let n1 = div n 2 in
36
      let left, l = tree_of_list_aux n1 l in
37 38
      match l with
      | Nil -> absurd
39 40
      | Cons x l -> let right, l = tree_of_list_aux (n - n1) l in
                    Node left x right, l
41 42 43 44 45
      end

  let tree_of_list (l: list elt) : tree elt
    ensures { inorder result = l }
    ensures { size result > 0 -> let h = height result in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
46
                power 2 (h-1) <= size result < power 2 h }
47
  =
48
    let t, l = tree_of_list_aux (length l) l in
49 50 51 52
    assert { l = Nil };
    t

end