(* type key == int *) sort color = {a:int | 0 <= a <= 1} (* * The following definition takes much more time in type-checking: * sort color = {a:int | a = 0 \/ a = 1} *) datatype rbtree with (color, nat, nat, nat) = (* color, black height, violation, size *) E(0, 0, 0, 0) | {cl:color, cr:color, bh:nat, sl:nat, sr:nat} B(0, bh+1, 0, sl+sr+1) of rbtree(cl, bh, 0, sl) * int * rbtree(cr, bh, 0, sr) | {cl:color, cr:color, bh:nat, sl:nat, sr:nat} R(1, bh, cl+cr, sl+sr+1) of rbtree(cl, bh, 0, sl) * int * rbtree(cr, bh, 0, sr) fun restore (R(R(a, x, b), y, c), z, d) = R(B(a, x, b), y, B(c, z, d)) | restore (R(a, x, R(b, y, c)), z, d) = R(B(a, x, b), y, B(c, z, d)) | restore (a, x, R(R(b, y, c), z, d)) = R(B(a, x, b), y, B(c, z, d)) | restore (a, x, R(b, y, R(c, z, d))) = R(B(a, x, b), y, B(c, z, d)) | restore (E, x, E) = B (E, x, E) | restore (E, x, t2 as B _) = B (E, x, t2) | restore (E, x, t2 as R (E, _, E)) = B (E, x, t2) | restore (E, x, t2 as R (E, _, B _)) = B (E, x, t2) | restore (E, x, t2 as R (B _, _, E)) = B (E, x, t2) | restore (E, x, t2 as R (B _, _, B _)) = B (E, x, t2) | restore (t1 as B _, x, E) = B (t1, x, E) | restore (t1 as B _, x, t2 as B _) = B (t1, x, t2) | restore (t1 as B _, x, t2 as R (E, _, E)) = B (t1, x, t2) | restore (t1 as B _, x, t2 as R (E, _, B _)) = B (t1, x, t2) | restore (t1 as B _, x, t2 as R (B _, _, E)) = B (t1, x, t2) | restore (t1 as B _, x, t2 as R (B _, _, B _)) = B (t1, x, t2) | restore (t1 as R (E, _, E), x, E) = B (t1, x, E) | restore (t1 as R (E, _, E), x, t2 as B _) = B (t1, x, t2) | restore (t1 as R (E, _, E), x, t2 as R (E, _, E)) = B (t1, x, t2) | restore (t1 as R (E, _, E), x, t2 as R (E, _, B _)) = B (t1, x, t2) | restore (t1 as R (E, _, E), x, t2 as R (B _, _, E)) = B (t1, x, t2) | restore (t1 as R (E, _, E), x, t2 as R (B _, _, B _)) = B (t1, x, t2) | restore (t1 as R (E, _, B _), x, E) = B (t1, x, E) | restore (t1 as R (E, _, B _), x, t2 as B _) = B (t1, x, t2) | restore (t1 as R (E, _, B _), x, t2 as R (E, _, E)) = B (t1, x, t2) | restore (t1 as R (E, _, B _), x, t2 as R (E, _, B _)) = B (t1, x, t2) | restore (t1 as R (E, _, B _), x, t2 as R (B _, _, E)) = B (t1, x, t2) | restore (t1 as R (E, _, B _), x, t2 as R (B _, _, B _)) = B (t1, x, t2) | restore (t1 as R (B _, _, E), x, E) = B (t1, x, E) | restore (t1 as R (B _, _, E), x, t2 as B _) = B (t1, x, t2) | restore (t1 as R (B _, _, E), x, t2 as R (E, _, E)) = B (t1, x, t2) | restore (t1 as R (B _, _, E), x, t2 as R (E, _, B _)) = B (t1, x, t2) | restore (t1 as R (B _, _, E), x, t2 as R (B _, _, E)) = B (t1, x, t2) | restore (t1 as R (B _, _, E), x, t2 as R (B _, _, B _)) = B (t1, x, t2) | restore (t1 as R (B _, _, B _), x, E) = B (t1, x, E) | restore (t1 as R (B _, _, B _), x, t2 as B _) = B (t1, x, t2) | restore (t1 as R (B _, _, B _), x, t2 as R (E, _, E)) = B (t1, x, t2) | restore (t1 as R (B _, _, B _), x, t2 as R (E, _, B _)) = B (t1, x, t2) | restore (t1 as R (B _, _, B _), x, t2 as R (B _, _, E)) = B (t1, x, t2) | restore (t1 as R (B _, _, B _), x, t2 as R (B _, _, B _)) = B (t1, x, t2) (* | restore (a, x, b) = B(a, x, b) *) withtype {cl:color, cr:color, bh:nat, vl:nat, vr:nat, sl:nat, sr:nat | vl+vr <= 1} <> => rbtree(cl, bh, vl, sl) * int * rbtree(cr, bh, vr, sr) -> [c:color] rbtree(c, bh+1, 0, sl+sr+1) exception Item_already_exists fun insert (x, t) = let fun ins (E) = R(E, x, E) | ins (B(a, y, b)) = if x < y then restore(ins a, y, b) else if y < x then restore(a, y, ins b) else raise Item_already_exists | ins (R(a, y, b)) = if x < y then R(ins a, y, b) else if y < x then R(a, y, ins b) else raise Item_already_exists withtype {c:color, bh:nat, s:nat} => rbtree(c, bh, 0, s) -> [c':color, v:nat | v <= c] rbtree(c', bh, v, s+1) in case ins t of R(a, y, b) => B(a, y, b) | t as B _ => t end withtype {c:color, bh:nat, s:nat} <> => int * rbtree(c, bh, 0, s) -> [bh':nat | bh <= bh' <= bh+1] rbtree(0, bh', 0, s+1)