structure AVL_TREE = struct assert compare <| 'a * 'a -> order datatype 'a AVLtree = AVLempty | AVLbranch of int * 'a * 'a AVLtree * 'a AVLtree typeref 'a AVLtree of nat * nat (* height and size and violation *) with AVLempty <| 'a AVLtree(0, 0) | AVLbranch <| {lh:nat, ls:nat, rh:nat, rs:nat | rh - 1 <= lh <= rh + 1} int(1+max(lh,rh)) * 'a * 'a AVLtree(lh, ls) * 'a AVLtree(rh, rs) -> 'a AVLtree(1+max(lh,rh), 1+ls+rs) fun('a) avlDepth(AVLempty) = 0 | avlDepth(AVLbranch(h, _, _, _) = h where avlDepth <| {h:nat, s:nat} 'a AVLtree(h, s) -> int(h) fun('a) avlRotateLeft(e, l as AVLbranch(lh, le, ll, lr), r) = let val rh = avlDepth(r) in if (lh <= rh+1) then AVLbranch(rh+1, e, l, r) else (* lh = rh + 2 *) let val llh = avlDepth(ll) and lrh = avlDepth(lr) in if (llh < lrh) then (* rh = llh: deep rotation *) case lr of AVLbranch(_, lre, lrl, lrr) => AVLbranch(rh+2, lre, AVLbranch(llh+1, le, ll, lrl), AVLbranch(rh+1, e, lrr, r)) else (* lrh <= llh: shallow rotate *) AVLbranch(lh+1, le, l, AVLbranch(lrh+1, e, lr, r)) end end where avlRotateLeft <| {lh:nat, ls:nat, rh:nat, rs:nat | rh - 1 <= lh <= rh+2 } 'a * 'a AVLtree(lh, ls) * 'a AVLtree(rh, rs) -> [h:nat | (lh <= rh+1 /\ h = rh+1) \/ (lh = rh+2 /\ (lh <= h = lh+1))] 'a AVLtree(h, ls+rs+1) fun('a) avlRotateRight(e, l, r as AVLbranch(rh, re, rl, rr)) = let val lh = avlDepth(l) in if (rh <= lh+1) then AVLbranch(rh+1, e, l, r) else (* rh = lh + 2 *) let val rlh = avlDepth(ll) and rrh = avlDepth(lr) in if (rlh > rrh) then (* lh = rrh: deep rotation *) case rl of AVLbranch(_, rle, rll, rlr) => AVLbranch(rh+2, rle, AVLbranch(lh+1, e, l, rll), AVLbranch(rrh+1, re, rlr, r)) else (* rlh <= rrh: shallow rotate *) AVLbranch(rh+1, re, AVLbranch(rlh+1, e, l, rl), r) end end where avlRotateRight <| {lh:nat, ls:nat, rh:nat, rs:nat | lh - 1 <= rh <= lh+2 } 'a * 'a AVLtree(lh, ls) * 'a AVLtree(rh, rs) -> [h:nat | (rh <= lh+1 /\ h = lh+1) \/ (rh = lh+2 /\ (rh <= h <= rh+1))] 'a AVLtree(h, ls+rs+1) fun('a) avlInsert(e, AVLempty) = AVLbranch(1, e, AVLempty, AVLempty) | avlInsert(e, t as AVLbranch(h, top, l, r) = case compare(e, te) of LESS => avlRotateLeft(te, avlInsert(e, l), r) | GREATER => avlRotateRight(te, l, avlInsert(e, r)) where avlInsert <| {h:nat, s:nat} 'a * 'a AVLtree(h, s) -> [h':nat | h <= h' <= h + 1] 'a AVLtree(h',s+1) end (* end of structure AVL_TREE *)