stdlib/bintree.mlw

   1
   2 (** {1 Polymorphic binary trees with elements at nodes} *)
   3
   4 module Tree
   5
   6   type tree 'a = Empty | Node (tree 'a) 'a (tree 'a)
   7
   8   let predicate is_empty (t:tree 'a)
   9     ensures { result <-> t = Empty }
  10   = match t with Empty -> true | Node _ _ _ -> false end
  11
  12 end
  13
  14 (** {2 Number of nodes} *)
  15
  16 module Size
  17
  18   use Tree
  19   use int.Int
  20
  21   let rec function size (t: tree 'a) : int = match t with
  22     | Empty -> 0
  23     | Node l _ r -> 1 + size l + size r
  24   end
  25
  26   lemma size_nonneg: forall t: tree 'a. 0 <= size t
  27
  28   lemma size_empty: forall t: tree 'a. 0 = size t <-> t = Empty
  29
  30 end
  31
  32 (** {2 Occurrences in a binary tree} *)
  33
  34 module Occ
  35
  36   use Tree
  37   use int.Int
  38
  39   function occ (x: 'a) (t: tree 'a) : int = match t with
  40     | Empty      -> 0
  41     | Node l y r -> (if y = x then 1 else 0) + occ x l + occ x r
  42   end
  43
  44   lemma occ_nonneg:
  45     forall x: 'a, t: tree 'a. 0 <= occ x t
  46
  47   predicate mem (x: 'a) (t: tree 'a) =
  48     0 < occ x t
  49
  50 end
  51
  52 (** {2 Height of a tree} *)
  53
  54 module Height
  55
  56   use Tree
  57   use int.Int
  58   use int.MinMax
  59
  60   let rec function height (t: tree 'a) : int = match t with
  61     | Empty      -> 0
  62     | Node l _ r -> 1 + max (height l) (height r)
  63   end
  64
  65   lemma height_nonneg:
  66     forall t: tree 'a. 0 <= height t
  67
  68 end
  69
  70 (** {2 In-order traversal} *)
  71
  72 module Inorder
  73
  74   use Tree
  75   use list.List
  76   use list.Append
  77
  78   let rec function inorder (t: tree 'a) : list 'a = match t with
  79     | Empty -> Nil
  80     | Node l x r -> inorder l ++ Cons x (inorder r)
  81   end
  82
  83 end
  84
  85 (** {2 Pre-order traversal} *)
  86
  87 module Preorder
  88
  89   use Tree
  90   use list.List
  91   use list.Append
  92
  93   let rec function preorder (t: tree 'a) : list 'a = match t with
  94     | Empty -> Nil
  95     | Node l x r -> Cons x (preorder l ++ preorder r)
  96   end
  97
  98 end
  99
 100 module InorderLength
 101
 102   use Tree
 103   use Size
 104   use Inorder
 105   use list.List
 106   use list.Length
 107
 108   lemma inorder_length: forall t: tree 'a. length (inorder t) = size t
 109
 110 end
 111
 112 (** {2 Huet's zipper} *)
 113
 114 module Zipper
 115
 116   use Tree
 117
 118   type zipper 'a =
 119     | Top
 120     | Left  (zipper 'a) 'a (tree 'a)
 121     | Right (tree 'a)   'a (zipper 'a)
 122
 123   let rec function zip (t: tree 'a) (z: zipper 'a) : tree 'a =
 124     match z with
 125     | Top -> t
 126     | Left z x r -> zip (Node t x r) z
 127     | Right l x z -> zip (Node l x t) z
 128     end
 129
 130   (* navigating in a tree using a zipper *)
 131
 132   type pointed 'a = (tree 'a, zipper 'a)
 133
 134   let function start (t: tree 'a) : pointed 'a = (t, Top)
 135
 136   let function up (p: pointed 'a) : pointed 'a = match p with
 137     | _, Top -> p (* do nothing *)
 138     | l, Left z x r | r, Right l x z -> (Node l x r, z)
 139   end
 140
 141   let function top (p: pointed 'a) : tree 'a = let t, z = p in zip t z
 142
 143   let function down_left (p: pointed 'a) : pointed 'a = match p with
 144     | Empty, _ -> p (* do nothing *)
 145     | Node l x r, z -> (l, Left z x r)
 146   end
 147
 148   let function down_right (p: pointed 'a) : pointed 'a = match p with
 149     | Empty, _ -> p (* do nothing *)
 150     | Node l x r, z -> (r, Right l x z)
 151   end
 152
 153 end
 154
 155 (* monomorphic AVL trees, for the purpose of Coma tests *)
 156 module AVL
 157
 158   use int.Int
 159   use int.MinMax
 160
 161   type elt
 162
 163   val predicate lt elt elt
 164   clone relations.TotalStrictOrder with
 165     type t = elt, predicate rel = lt, axiom .
 166
 167   (* binary trees with height stored in nodes *)
 168   type tree = E | N int tree elt tree
 169
 170   let function ht (t: tree) : int =
 171     match t with E -> 0 | N h _ _ _ -> h end
 172
 173   (* smart constructor *)
 174   let function node (l: tree) (x: elt) (r: tree) : tree =
 175     N (1 + max (ht l) (ht r)) l x r
 176
 177   let rec ghost function height (t: tree) : int
 178     ensures { result >= 0 }
 179   = match t with
 180     | E         -> 0
 181     | N _ l _ r -> 1 + max (height l) (height r)
 182     end
 183
 184   predicate wf (t: tree) =
 185     match t with
 186     | E         -> true
 187     | N h l _ r -> h = height t && wf l && wf r
 188     end
 189
 190   predicate mem (y: elt) (t: tree) =
 191     match t with
 192     | E         -> false
 193     | N _ l x r -> mem y l || y=x || mem y r
 194     end
 195
 196   predicate tree_lt (t: tree) (y: elt) =
 197     forall x. mem x t -> lt x y
 198
 199   predicate lt_tree (y: elt) (t: tree) =
 200     forall x. mem x t -> lt y x
 201
 202   predicate bst (t: tree) =
 203     match t with
 204     | E         -> true
 205     | N _ l x r -> bst l && tree_lt l x && bst r && lt_tree x r
 206     end
 207
 208   predicate avl (t: tree) =
 209     match t with
 210     | E         -> true
 211     | N _ l _ r -> avl l && avl r && -1 <= height l - height r <= 1
 212     end
 213
 214 end