generate_all_trees.mlw 2.71 KB
Newer Older
1 2 3 4 5 6 7

(*
   Generate all binary trees of size n.

   Given n, the program return an array a of size n+1 such that
   a[i] contains the list of all binary trees of size i.

8
   TODO: tail-recursive version of combine
9 10 11 12 13 14 15 16
*)

module GenerateAllTrees

  use import int.Int
  use import list.List
  use import list.Mem
  use import list.Append
17
  use import list.Distinct
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
  use import module array.Array

  type tree = Empty | Node tree tree

  function size (t: tree) : int = match t with
    | Empty    -> 0
    | Node l r -> 1 + size l + size r
  end

  lemma size_nonneg: forall t: tree. size t >= 0

  lemma size_left:
    forall t: tree. size t > 0 ->
    exists l r: tree. t = Node l r /\ size l < size t

  predicate all_trees (n: int) (l: list tree) =
34
    distinct l /\
35 36 37 38
    forall t: tree. size t = n <-> mem t l

  lemma all_trees_0: all_trees 0 (Cons Empty Nil)

39 40 41 42
  lemma tree_diff:
    forall l1 l2: tree. size l1 <> size l2 ->
    forall r1 r2: tree. Node l1 r1 <> Node l2 r2

43 44 45 46 47
  (* combines two lists of trees l1 and l2 into the list of trees
     with a left sub-tree from l1 and a right sub-tree from l2 *)
  let combine (i1: int) (l1: list tree) (i2: int) (l2: list tree) =
    { 0 <= i1 /\ all_trees i1 l1 /\ 0 <= i2 /\ all_trees i2 l2 }
    let rec loop1 (l1: list tree) : list tree =
48
      { distinct l1 }
49 50 51 52
      match l1 with
      | Nil -> Nil
      | Cons t1 l1 ->
          let rec loop2 (l2: list tree) : list tree =
53
            { distinct l2 }
54 55 56 57
            match l2 with
            | Nil -> Nil
            | Cons t2 l2 -> Cons (Node t1 t2) (loop2 l2)
            end
58 59
            { distinct result /\
              forall t:tree. mem t result <->
60 61 62 63
              (exists r: tree. t = Node t1 r /\ mem r l2) }
         in
         loop2 l2 ++ loop1 l1
      end
64 65
      { distinct result /\
        forall t:tree. mem t result <->
66 67 68
        (exists l r: tree. t = Node l r /\ mem l l1 /\ mem r l2) }
    in
    loop1 l1
69 70
    { distinct result /\
      forall t:tree. mem t result <->
71 72 73 74 75 76 77 78 79 80 81 82
      (exists l r: tree. t = Node l r /\ size l = i1 /\ size r = i2) }

  let all_trees (n: int) =
    { n >= 0 }
    let a = make (n+1) Nil in
    a[0] <- Cons Empty Nil;
    for i = 1 to n do
      invariant { (forall k: int. 0 <= k < i -> all_trees k a[k]) }
      a[i] <- Nil;
      for j = 0 to i-1 do
        invariant {
          (forall k: int. 0 <= k < i -> all_trees k a[k]) /\
83
          distinct a[i] /\
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
          (forall t: tree. mem t a[i] <->
           exists l r: tree. t = Node l r /\ size t = i /\ size l < j) }
        a[i] <- (combine j a[j] (i-1-j) a[i-1-j]) ++ a[i]
      done
    done;
    a
    { forall i: int. 0 <= i <= n -> all_trees i result[i] }

end

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/generate_all_trees.gui"
End:
*)