OCaml Program
Inlining:
More
Less
Checking:
Static
Dynamic
Hybrid
 
type colour = R | B type rb = E | T of colour * rb * int * rb (* property (1) *) let rec red_or_black t = match t with | E -> true | T (c, t1, i, t2) -> (c = R or c = B) && red_or_black t1 && red_or_black t2 (* property (2) *) let root_is t rb = match t with | E -> true | T (c, t1, i, t2) -> c = rb (* property (3) *) let rec all_leaves_are_black t = match t with | E -> true | T (c, t1, i, t2) -> all_leaves_are_black t1 && all_leaves_are_black t2 (* property (4) *) let rec red_children_are_black t = match t with | E -> true | T (c, t1, i, t2) -> let b = red_children_are_black t1 && red_children_are_black t2 in if c = R then if root_is t1 R then false else if root_is t2 R then false else b else b (* proeprty (5) *) let rec blackdepth t = match t with | E -> 0 (* we don’t count Es as real nodes *) | T (c, t1, i, t2) -> if c = B then 1 + blackdepth t1 else blackdepth t1 let rec blackinvariant t = match t with | E -> true | T (c, t1, i, t2) -> blackdepth t1 = blackdepth t2 && blackinvariant t1 && blackinvariant t2 let rbinvariant t = red_children_are_black t && blackinvariant t let notE t = match t with | E -> false | T(c, t1, x, t2) -> true (* val balance : color -> rb -> int -> rb -> rb *) contract balance = {t | true} -> {z | if rbinvariant t && notE t then rbinvariant z && notE z else true} let balance t = match t with | T(B, t1, z, t2) -> begin match t1 with | T(R, l, y, r) -> begin match l with | T(R, a, x, b) -> T(R, T(B, a, x, b), y, T(B, r, z, t2)) | n1 -> begin match r with | T(R, b1, y1, c1) -> T(R, T(B, l, y, b1), y1, T(B, c1, z, t2)) | n2 -> t end end | n3 -> begin match t2 with | T(R, l1, z1, r1) -> begin match l1 with | T(R, b2, y2, c2) -> T(R, T(B, t1, z, b2), y2, T(B, c2, z1, r1)) | n4 -> begin match r1 with | T(R, c3, z2, d) -> T(R, T(B, t1, z, l1), z1, T(B, c3, z2, d)) | n5 -> t end end | n6 -> t end end | n7 -> t let rec contains x t = match t with | E -> false | T(c, t1, i, t2) -> if x = i then true else if x < i then contains x t1 else contains x t2 contract insert = {t | rbinvariant t} -> {x | true} -> {z | notE z && rbinvariant z} let rec insert t x = match t with | E -> T(R, E, x, E) | T(c, t1, y, t2) -> if x = y then t else if x < y then balance (T(c, insert t1 x, y, t2)) else balance (T(c, t1 , y, insert t2 x)) contract makeBlack = {t | notE t} -> {z | root_is z B && (if rbinvariant t then rbinvariant z else true)} let makeBlack t = match t with | T(c, t1, y, t2) -> T(B, t1, y, t2) | E -> failwith "makeBlack" (* val rbinsert : RB -> Int -> RB *) contract rbinsert = {t | rbinvariant t} -> {x | true} -> {z | rbinvariant z} let rbinsert s x = makeBlack (insert s x) (* val rbmin :: rb -> int *) contract rbmin = {t | notE t} -> {y | true} let rec rbmin t = match t with | T(c, t1, x, t2) -> begin match t1 with | E -> (c, x) | T(c1, t11, y, t12) -> rbmin t1 end | E -> failwith "rbmin" (* val btmax : tree -> int *) contract rbmax = {t | notE t} -> {y | true} let rec rbmax t = match t with | T(c, t1, x, t2) -> begin match t2 with | E -> (c, x) | T(c1, t21, y, t22) -> rbmax t2 end | E -> failwith "rbmax" contract delete = {t | rbinvariant t} -> {x | true} -> {z | rbinvariant z} let rec delete t x = match t with | E -> E | T(c, t, y, u) -> if y = x then begin match u with | E -> begin match t with | E -> E | T(c1, tl, z, tr) -> let (c2, tmax) = rbmax t in let t1 = delete t tmax in balance (T(c2, t1, tmax, E)) end | T(c3, ul, w, ur) -> let (c4, umin) = rbmin u in let u1 = delete u umin in balance (T(c4, E, umin, u1)) end else if x < y then balance (T(c, delete t x, y, u)) else balance (T(c, t, y, delete u x)) contract rbdelete = {t | rbinvariant t} -> {x | true} -> {z | rbinvariant z} let rbdelete s x = match delete s x with | E -> E | T(c, t1, y, t2) -> makeBlack (T(c, t1, y, t2))