Name constructors so that they are less likely to collide with something.

This commit is contained in:
evancz 2012-10-10 15:05:23 -07:00
parent 2fcf29ca8f
commit 7822f02666

View file

@ -5,11 +5,11 @@ import Data.Maybe (isJust)
data NColor = Red | Black data NColor = Red | Black
data RBTree k v = Node NColor k v (RBTree k v) (RBTree k v) | Empty data RBTree k v = RBNode NColor k v (RBTree k v) (RBTree k v) | RBEmpty
raise = console.log raise = console.log
empty = Empty empty = RBEmpty
-- Helpers for checking invariants -- Helpers for checking invariants
@ -17,8 +17,8 @@ empty = Empty
equal_pathLen t = equal_pathLen t =
let path_numBlacks t = let path_numBlacks t =
case t of case t of
{ Empty -> 1 { RBEmpty -> 1
; Node col _ _ l r -> ; RBNode col _ _ l r ->
let { bl = path_numBlacks l ; br = path_numBlacks r } in let { bl = path_numBlacks l ; br = path_numBlacks r } in
if bl /= br || bl == 0-1 || br == 0-1 if bl /= br || bl == 0-1 || br == 0-1
then 0-1 then 0-1
@ -28,22 +28,22 @@ equal_pathLen t =
rootBlack t = rootBlack t =
case t of case t of
{ Empty -> True { RBEmpty -> True
; Node Black _ _ _ _ -> True ; RBNode Black _ _ _ _ -> True
; _ -> False } ; _ -> False }
redBlack_children t = redBlack_children t =
case t of case t of
{ Node Red _ _ (Node Red _ _ _ _) _ -> False { RBNode Red _ _ (RBNode Red _ _ _ _) _ -> False
; Node Red _ _ _ (Node Red _ _ _ _) -> False ; RBNode Red _ _ _ (RBNode Red _ _ _ _) -> False
; Empty -> True ; RBEmpty -> True
; Node _ _ _ l r -> redBlack_children l && redBlack_children r ; RBNode _ _ _ l r -> redBlack_children l && redBlack_children r
} }
findExtreme f t = findExtreme f t =
case t of case t of
{ Empty -> Nothing { RBEmpty -> Nothing
; Node c k _ l r -> ; RBNode c k _ l r ->
case findExtreme f (f (l,r)) of case findExtreme f (f (l,r)) of
{ Nothing -> Just k { Nothing -> Just k
; Just k' -> Just k' } ; Just k' -> Just k' }
@ -67,8 +67,8 @@ olte xo yo = optionRelation (<=) True xo yo
ordered t = ordered t =
case t of case t of
{ Empty -> True { RBEmpty -> True
; Node c k v l r -> ; RBNode c k v l r ->
let (lmax,rmin) = (findmaxRbt l, findminRbt r) in let (lmax,rmin) = (findmaxRbt l, findminRbt r) in
olte lmax (Just k) && olte (Just k) rmin && ordered l && ordered r olte lmax (Just k) && olte (Just k) rmin && ordered l && ordered r
} }
@ -76,10 +76,10 @@ ordered t =
-- Check that there aren't any right red nodes in the tree *) -- Check that there aren't any right red nodes in the tree *)
leftLeaning t = leftLeaning t =
case t of case t of
{ Empty -> True { RBEmpty -> True
; Node _ _ _ (Node Black _ _ _ _) (Node Red _ _ _ _) -> False ; RBNode _ _ _ (RBNode Black _ _ _ _) (RBNode Red _ _ _ _) -> False
; Node _ _ _ Empty (Node Red _ _ _ _) -> False ; RBNode _ _ _ RBEmpty (RBNode Red _ _ _ _) -> False
; Node _ _ _ l r -> (leftLeaning l) && (leftLeaning r) ; RBNode _ _ _ l r -> (leftLeaning l) && (leftLeaning r)
} }
invariants_hold t = invariants_hold t =
@ -91,22 +91,22 @@ invariants_hold t =
min t = min t =
case t of case t of
{ Node _ k v Empty _ -> (k,v) { RBNode _ k v RBEmpty _ -> (k,v)
; Node _ _ _ l _ -> min l ; RBNode _ _ _ l _ -> min l
; Empty -> console.log "(min Empty) is not defined" ; RBEmpty -> console.log "(min RBEmpty) is not defined"
} }
max t = max t =
case t of case t of
{ Node _ k v _ Empty -> (k,v) { RBNode _ k v _ RBEmpty -> (k,v)
; Node _ _ _ _ r -> max r ; RBNode _ _ _ _ r -> max r
; Empty -> console.log "(max Empty) is not defined" ; RBEmpty -> console.log "(max RBEmpty) is not defined"
} }
lookup k t = lookup k t =
case t of case t of
{ Empty -> Nothing { RBEmpty -> Nothing
; Node _ k' v l r -> ; RBNode _ k' v l r ->
case compare k k' of case compare k k' of
{ LT -> lookup k l { LT -> lookup k l
; EQ -> Just v ; EQ -> Just v
@ -118,39 +118,39 @@ member k t = isJust $ lookup k t
rotateLeft t = rotateLeft t =
case t of case t of
{ Node cy ky vy a (Node cz kz vz b c) -> Node cy kz vz (Node Red ky vy a b) c { RBNode cy ky vy a (RBNode cz kz vz b c) -> RBNode cy kz vz (RBNode Red ky vy a b) c
; _ -> raise "rotateLeft of a node without enough children" } ; _ -> raise "rotateLeft of a node without enough children" }
-- rotateRight -- the reverse, and -- rotateRight -- the reverse, and
-- makes Y have Z's color, and makes Z Red. -- makes Y have Z's color, and makes Z Red.
rotateRight t = rotateRight t =
case t of case t of
{ Node cz kz vz (Node cy ky vy a b) c -> Node cz ky vy a (Node Red kz vz b c) { RBNode cz kz vz (RBNode cy ky vy a b) c -> RBNode cz ky vy a (RBNode Red kz vz b c)
; _ -> raise "rotateRight of a node without enough children" } ; _ -> raise "rotateRight of a node without enough children" }
rotateLeftIfNeeded t = rotateLeftIfNeeded t =
case t of case t of
{ Node _ _ _ _ (Node Red _ _ _ _) -> rotateLeft t { RBNode _ _ _ _ (RBNode Red _ _ _ _) -> rotateLeft t
; _ -> t } ; _ -> t }
rotateRightIfNeeded t = rotateRightIfNeeded t =
case t of case t of
{ Node _ _ _ (Node Red _ _ (Node Red _ _ _ _) _) _ -> rotateRight t { RBNode _ _ _ (RBNode Red _ _ (RBNode Red _ _ _ _) _) _ -> rotateRight t
; _ -> t } ; _ -> t }
otherColor c = case c of { Red -> Black ; Black -> Red } otherColor c = case c of { Red -> Black ; Black -> Red }
color_flip t = color_flip t =
case t of case t of
{ Node c1 bk bv (Node c2 ak av la ra) (Node c3 ck cv lc rc) -> { RBNode c1 bk bv (RBNode c2 ak av la ra) (RBNode c3 ck cv lc rc) ->
Node (otherColor c1) bk bv RBNode (otherColor c1) bk bv
(Node (otherColor c2) ak av la ra) (RBNode (otherColor c2) ak av la ra)
(Node (otherColor c3) ck cv lc rc) (RBNode (otherColor c3) ck cv lc rc)
; _ -> raise "color_flip called on a Empty or Node with a Empty child" } ; _ -> raise "color_flip called on a RBEmpty or RBNode with a RBEmpty child" }
color_flipIfNeeded t = color_flipIfNeeded t =
case t of case t of
{ Node _ _ _ (Node Red _ _ _ _) (Node Red _ _ _ _) -> color_flip t { RBNode _ _ _ (RBNode Red _ _ _ _) (RBNode Red _ _ _ _) -> color_flip t
; _ -> t } ; _ -> t }
fixUp t = color_flipIfNeeded (rotateRightIfNeeded (rotateLeftIfNeeded t)) fixUp t = color_flipIfNeeded (rotateRightIfNeeded (rotateLeftIfNeeded t))
@ -158,19 +158,19 @@ fixUp t = color_flipIfNeeded (rotateRightIfNeeded (rotateLeftIfNeeded t))
ensureBlackRoot t = ensureBlackRoot t =
case t of case t of
{ Node Red k v l r -> Node Black k v l r { RBNode Red k v l r -> RBNode Black k v l r
; _ -> t } ; _ -> t }
-- Invariant: t is a valid left-leaning rb tree *) -- Invariant: t is a valid left-leaning rb tree *)
insert k v t = insert k v t =
let ins t = let ins t =
case t of case t of
{ Empty -> Node Red k v Empty Empty { RBEmpty -> RBNode Red k v RBEmpty RBEmpty
; Node c k' v' l r -> ; RBNode c k' v' l r ->
let h = case compare k k' of let h = case compare k k' of
{ LT -> Node c k' v' (ins l) r { LT -> RBNode c k' v' (ins l) r
; EQ -> Node c k' v l r -- replace ; EQ -> RBNode c k' v l r -- replace
; GT -> Node c k' v' l (ins r) } ; GT -> RBNode c k' v' l (ins r) }
in fixUp h } in fixUp h }
in if not (invariants_hold t) then in if not (invariants_hold t) then
raise "invariants broken before insert" raise "invariants broken before insert"
@ -179,42 +179,42 @@ insert k v t =
raise "invariants broken after insert" raise "invariants broken after insert"
else new_t) else new_t)
singleton k v = insert k v Empty singleton k v = insert k v RBEmpty
isRed t = isRed t =
case t of case t of
{ Node Red _ _ _ _ -> True { RBNode Red _ _ _ _ -> True
; _ -> False } ; _ -> False }
isRedLeft t = isRedLeft t =
case t of case t of
{ Node _ _ _ (Node Red _ _ _ _) _ -> True { RBNode _ _ _ (RBNode Red _ _ _ _) _ -> True
; _ -> False } ; _ -> False }
isRedLeftLeft t = isRedLeftLeft t =
case t of case t of
{ Node _ _ _ (Node _ _ _ (Node Red _ _ _ _) _) _ -> True { RBNode _ _ _ (RBNode _ _ _ (RBNode Red _ _ _ _) _) _ -> True
; _ -> False } ; _ -> False }
isRedRight t = isRedRight t =
case t of case t of
{ Node _ _ _ _ (Node Red _ _ _ _) -> True { RBNode _ _ _ _ (RBNode Red _ _ _ _) -> True
; _ -> False } ; _ -> False }
isRedRightLeft t = isRedRightLeft t =
case t of case t of
{ Node _ _ _ _ (Node _ _ _ (Node Red _ _ _ _) _) -> True { RBNode _ _ _ _ (RBNode _ _ _ (RBNode Red _ _ _ _) _) -> True
; _ -> False } ; _ -> False }
moveRedLeft t = moveRedLeft t =
let t' = color_flip t in let t' = color_flip t in
case t' of case t' of
{ Node c k v l r -> { RBNode c k v l r ->
case r of case r of
{ Node _ _ _ (Node Red _ _ _ _) _ -> { RBNode _ _ _ (RBNode Red _ _ _ _) _ ->
color_flip (rotateLeft (Node c k v l (rotateRight r))) color_flip (rotateLeft (RBNode c k v l (rotateRight r)))
; _ -> t' } ; _ -> t' }
; _ -> t' } ; _ -> t' }
@ -235,11 +235,11 @@ moveRedRightIfNeeded t =
deleteMin t = deleteMin t =
let del t = let del t =
case t of case t of
{ Node _ _ _ Empty _ -> Empty { RBNode _ _ _ RBEmpty _ -> RBEmpty
; _ -> let t' = moveRedLeftIfNeeded t in ; _ -> let t' = moveRedLeftIfNeeded t in
case t' of case t' of
{ Node c k v l r -> fixUp (Node c k v (del l) r) { RBNode c k v l r -> fixUp (RBNode c k v (del l) r)
; Empty -> Empty } ; RBEmpty -> RBEmpty }
} }
in ensureBlackRoot (del t) in ensureBlackRoot (del t)
@ -247,39 +247,39 @@ deleteMax t =
let del t = let del t =
let t' = if isRedLeft t then rotateRight t else t in let t' = if isRedLeft t then rotateRight t else t in
case t' of case t' of
{ Node _ _ _ _ Empty -> Empty { RBNode _ _ _ _ RBEmpty -> RBEmpty
; _ -> let t'' = moveRedRightIfNeeded t' in ; _ -> let t'' = moveRedRightIfNeeded t' in
case t'' of case t'' of
{ Node c k v l r -> fixUp (Node c k v l (del r)) { RBNode c k v l r -> fixUp (RBNode c k v l (del r))
; Empty -> Empty } } ; RBEmpty -> RBEmpty } }
in ensureBlackRoot (del t) in ensureBlackRoot (del t)
remove k t = remove k t =
let { let {
eq_and_noRightNode t = case t of { Node _ k' _ _ Empty -> k == k' ; _ -> False } eq_and_noRightNode t = case t of { RBNode _ k' _ _ RBEmpty -> k == k' ; _ -> False }
; eq t = case t of { Node _ k' _ _ _ -> k == k' ; _ -> False } ; eq t = case t of { RBNode _ k' _ _ _ -> k == k' ; _ -> False }
; delLT t = ; delLT t =
let t' = moveRedLeftIfNeeded t in let t' = moveRedLeftIfNeeded t in
case t' of case t' of
{ Node c k' v l r -> fixUp (Node c k' v (del l) r) { RBNode c k' v l r -> fixUp (RBNode c k' v (del l) r)
; Empty -> raise "delLT on Empty" } ; RBEmpty -> raise "delLT on RBEmpty" }
; delEQ t = ; delEQ t =
case t of -- Replace with successor case t of -- Replace with successor
{ Node c _ _ l r -> { RBNode c _ _ l r ->
let (k',v') = min r in let (k',v') = min r in
fixUp (Node c k' v' l (deleteMin r)) fixUp (RBNode c k' v' l (deleteMin r))
; Empty -> raise "delEQ called on a Empty" } ; RBEmpty -> raise "delEQ called on a RBEmpty" }
; delGT t = ; delGT t =
case t of case t of
{ Node c k' v l r -> fixUp (Node c k' v l (del r)) { RBNode c k' v l r -> fixUp (RBNode c k' v l (del r))
; Empty -> raise "delGT called on a Empty" } ; RBEmpty -> raise "delGT called on a RBEmpty" }
; del t = ; del t =
case t of case t of
{ Empty -> Empty { RBEmpty -> RBEmpty
; Node _ k' _ _ _ -> ; RBNode _ k' _ _ _ ->
if k < k' then delLT t if k < k' then delLT t
else (let t' = if isRedLeft t then rotateRight t else t in else (let t' = if isRedLeft t then rotateRight t else t in
if eq_and_noRightNode t' then Empty if eq_and_noRightNode t' then RBEmpty
else (let t = moveRedRightIfNeeded t in else (let t = moveRedRightIfNeeded t in
if eq t then delEQ t else delGT t)) } if eq t then delEQ t else delGT t)) }
} }
@ -291,9 +291,6 @@ remove k t =
fold f acc t = fold f acc t =
case t of case t of
{ Empty -> acc { RBEmpty -> acc
; Node _ k v l r -> fold f (f k v (fold f acc l)) r ; RBNode _ k v l r -> fold f (f k v (fold f acc l)) r
} }
{--
--}