examples/generate_all_trees.mlw

   1
   2 (*
   3    Generate all binary trees of size n.
   4
   5    Given n, the program return an array a of size n+1 such that
   6    a[i] contains the list of all binary trees of size i.
   7
   8    TODO: tail-recursive version of combine
   9 *)
  10
  11 module GenerateAllTrees
  12
  13   use int.Int
  14   use list.List
  15   use list.Mem
  16   use list.Append
  17   use list.Distinct
  18   use array.Array
  19   use list.Length
  20
  21   type tree = Empty | Node tree tree
  22
  23   function size (t: tree) : int = match t with
  24     | Empty    -> 0
  25     | Node l r -> 1 + size l + size r
  26   end
  27
  28   lemma size_nonneg: forall t: tree. size t >= 0
  29
  30   lemma size_left:
  31     forall t: tree. size t > 0 ->
  32     exists l r: tree. t = Node l r /\ size l < size t
  33
  34   predicate all_trees (n: int) (l: list tree) =
  35     distinct l /\
  36     forall t: tree. size t = n <-> mem t l
  37
  38   lemma all_trees_0: all_trees 0 (Cons Empty Nil)
  39
  40   lemma tree_diff:
  41     forall l1 l2: tree. size l1 <> size l2 ->
  42     forall r1 r2: tree. Node l1 r1 <> Node l2 r2
  43
  44   (* combines two lists of trees l1 and l2 into the list of trees
  45      with a left sub-tree from l1 and a right sub-tree from l2 *)
  46   let combine (i1: int) (l1: list tree) (i2: int) (l2: list tree)
  47     requires { 0 <= i1 /\ all_trees i1 l1 /\ 0 <= i2 /\ all_trees i2 l2 }
  48     ensures  { distinct result }
  49     ensures  { forall t:tree. mem t result <->
  50       (exists l r: tree. t = Node l r /\ size l = i1 /\ size r = i2) }
  51   = let rec loop1 (l1: list tree) : list tree variant { l1 }
  52       requires { distinct l1 }
  53       ensures  { distinct result }
  54       ensures  { forall t:tree. mem t result <->
  55         (exists l r: tree. t = Node l r /\ mem l l1 /\ mem r l2) }
  56     = match l1 with
  57       | Nil -> Nil
  58       | Cons t1 l1 ->
  59           let rec loop2 (l2: list tree) : list tree variant { l2 }
  60             requires { distinct l2 }
  61             ensures  { distinct result }
  62             ensures  { forall t:tree. mem t result <->
  63               (exists r: tree. t = Node t1 r /\ mem r l2) }
  64           = match l2 with
  65             | Nil -> Nil
  66             | Cons t2 l2 -> Cons (Node t1 t2) (loop2 l2)
  67             end
  68          in
  69          loop2 l2 ++ loop1 l1
  70       end
  71     in
  72     loop1 l1
  73
  74   let all_trees (n: int)
  75     requires { n >= 0 }
  76     ensures { forall i: int. 0 <= i <= n -> all_trees i result[i] }
  77   = let a = make (n+1) Nil in
  78     a[0] <- Cons Empty Nil;
  79     for i = 1 to n do
  80       invariant { forall k: int. 0 <= k < i -> all_trees k a[k] }
  81       a[i] <- Nil;
  82       for j = 0 to i-1 do
  83         invariant { forall k: int. 0 <= k < i -> all_trees k a[k] }
  84         invariant { distinct a[i] }
  85         invariant { forall t: tree. mem t a[i] <->
  86           (exists l r: tree. t = Node l r /\ size t = i /\ size l < j) }
  87         a[i] <- (combine j a[j] (i-1-j) a[i-1-j]) ++ a[i]
  88       done
  89     done;
  90     a
  91
  92 end