vacid0: red black trees continued

parent 107a7483
......@@ -111,10 +111,16 @@ module M
The result is not necessarily a black node. *)
parameter lbalance :
l : tree -> k : key -> v : value -> r : tree ->
let lbalance (l : tree) (k : key) (v : value) (r : tree) =
{ lt_tree k l and gt_tree k r and bst l and bst r }
tree
match l with
| Node Red (Node Red a kx vx b) ky vy c -> (* BUG or-pattern *)
Node Red (Node Black a kx vx b) ky vy (Node Black c k v r)
| Node Red a kx vx (Node Red b ky vy c) ->
Node Red (Node Black a kx vx b) ky vy (Node Black c k v r)
| _ ->
Node Black l k v r
end
{ bst result and
(forall n : int. almost_rbtree n l -> rbtree n r -> rbtree (n+1) result)
and
......@@ -131,10 +137,16 @@ module M
B a x b -> B a x b
*)
parameter rbalance :
l : tree -> k : key -> v : value -> r : tree ->
let rbalance (l : tree) (k : key) (v : value) (r : tree) =
{ lt_tree k l and gt_tree k r and bst l and bst r }
tree
match r with
| Node Red (Node Red b ky vy c) kz vz d ->
Node Red (Node Black l k v b) ky vy (Node Black c kz vz d)
| Node Red b ky vy (Node Red c kz vz d) ->
Node Red (Node Black l k v b) ky vy (Node Black c kz vz d)
| _ ->
Node Black l k v r
end
{ bst result and
(forall n : int. almost_rbtree n r -> rbtree n l -> rbtree (n+1) result)
and
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment