efdea2f · elk · git.iko.soy

git.iko.soy/elk

on master help sign in

Fix Dict insert bug by using generalized balance function

efdea2fMax New13 years ago

libraries/Dict.elm+82−88

compare with master

unifiedsplit

@@ -34,15 +34,35 @@ Insert, remove, and query operations all take *O(log n)* time.

34import open Basics

35import open Maybe

36import Native.Error

37−import List as List

37+import List

38+import String

38import Native.Utils

39import Native.Utils

40-- BBlack and NBlack should only be used during the deletion

41-- BBlack and NBlack should only be used during the deletion

41-- algorithm. Any other occurrence is a bug and should fail an assert.

42-- algorithm. Any other occurrence is a bug and should fail an assert.

42−data NColor = Red | Black

43+data NColor = Red

44+ | Black

45+ -- ^ Double Black, counts as 2 blacks for the invariant

43− | BBlack | NBlack

46+ | BBlack

44−

47+ -- ^ Negative Black, counts as -1 blacks for the invariant

48+ | NBlack

49+

50+

51+showNColor : NColor -> String

52+showNColor c = case c of

53+ Red -> "Red"

54+ Black -> "Black"

55+ BBlack -> "BBlack"

56+ NBlack -> "NBlack"

57+

45−data LeafColor = LBlack | LBBlack

58+data LeafColor = LBlack

59+ -- ^ Double Black, counts as 2

60+ | LBBlack

61+

62+showLColor : LeafColor -> String

63+showLColor c = case c of

64+ LBlack -> "LBlack"

65+ LBBlack -> "LBBlack"

47data Dict k v = RBNode NColor k v (Dict k v) (Dict k v)

67data Dict k v = RBNode NColor k v (Dict k v) (Dict k v)

48 | RBEmpty LeafColor

68 | RBEmpty LeafColor

@@ -93,51 +113,6 @@ member : comparable -> Dict comparable v -> Bool

93-- Does t contain k?

113-- Does t contain k?

94member k t = isJust <| lookup k t

114member k t = isJust <| lookup k t

115

96−rotateLeft : Dict k v -> Dict k v

97−rotateLeft t =

98− case t of

99− RBNode cy ky vy a (RBNode cz kz vz b c) -> RBNode cy kz vz (RBNode Red ky vy a b) c

100− _ -> Native.Error.raise "rotateLeft of a node without enough children"

101−

102−-- rotateRight -- the reverse, and

103−-- makes Y have Z's color, and makes Z Red.

104−rotateRight : Dict k v -> Dict k v

105−rotateRight t =

106− case t of

107− RBNode cz kz vz (RBNode cy ky vy a b) c -> RBNode cz ky vy a (RBNode Red kz vz b c)

108− _ -> Native.Error.raise "rotateRight of a node without enough children"

109−

110−rotateLeftIfNeeded : Dict k v -> Dict k v

111−rotateLeftIfNeeded t =

112− case t of

113− RBNode _ _ _ _ (RBNode Red _ _ _ _) -> rotateLeft t

114− _ -> t

115−

116−rotateRightIfNeeded : Dict k v -> Dict k v

117−rotateRightIfNeeded t =

118− case t of

119− RBNode _ _ _ (RBNode Red _ _ (RBNode Red _ _ _ _) _) _ -> rotateRight t

120− _ -> t

121−

122−otherColor c = case c of { Red -> Black ; Black -> Red }

123−

124−color_flip : Dict k v -> Dict k v

125−color_flip t =

126− case t of

127− RBNode c1 bk bv (RBNode c2 ak av la ra) (RBNode c3 ck cv lc rc) ->

128− RBNode (otherColor c1) bk bv

129− (RBNode (otherColor c2) ak av la ra)

130− (RBNode (otherColor c3) ck cv lc rc)

131− _ -> Native.Error.raise "color_flip called on a Empty or Node with a Empty child"

132−

133−color_flipIfNeeded : Dict k v -> Dict k v

134−color_flipIfNeeded t =

135− case t of

136− RBNode _ _ _ (RBNode Red _ _ _ _) (RBNode Red _ _ _ _) -> color_flip t

137− _ -> t

138−

139−fixUp t = color_flipIfNeeded (rotateRightIfNeeded (rotateLeftIfNeeded t))

140−

141ensureBlackRoot : Dict k v -> Dict k v

116ensureBlackRoot : Dict k v -> Dict k v

142ensureBlackRoot t =

117ensureBlackRoot t =

143 case t of

118 case t of

@@ -158,6 +133,11 @@ remove k t = let u _ = Nothing in

158 update k u t

133 update k u t

159

134

160data Flag = Insert | Remove | Same

135data Flag = Insert | Remove | Same

136+showFlag : Flag -> String

137+showFlag f = case f of

138+ Insert -> "Insert"

139+ Remove -> "Remove"

140+ Same -> "Same"

161

141

162{-| Update the value of a dictionary for a specific key with a given function. -}

142{-| Update the value of a dictionary for a specific key with a given function. -}

163update : comparable -> (Maybe v -> Maybe v) -> Dict comparable v -> Dict comparable v

143update : comparable -> (Maybe v -> Maybe v) -> Dict comparable v -> Dict comparable v

@@ -168,76 +148,87 @@ update k u t =

168 Just v -> (Insert, RBNode Red k v empty empty)

148 Just v -> (Insert, RBNode Red k v empty empty)

169 RBNode c k' v l r -> case Native.Utils.compare k k' of

149 RBNode c k' v l r -> case Native.Utils.compare k k' of

170 EQ -> case u (Just v) of

150 EQ -> case u (Just v) of

171− Nothing -> (Remove, rem t)

151+ Nothing -> (Remove, rem c l r)

172 Just v' -> (Same, RBNode c k' v' l r)

152 Just v' -> (Same, RBNode c k' v' l r)

173 LT -> let (fl, l') = up l in

153 LT -> let (fl, l') = up l in

174 case fl of

154 case fl of

175 Same -> (Same, RBNode c k' v l' r)

155 Same -> (Same, RBNode c k' v l' r)

176− Insert -> (Insert, fixUp <| RBNode c k' v l' r)

156+ Insert -> (Insert, balance c k' v l' r)

177 Remove -> (Remove, bubble c k' v l' r)

157 Remove -> (Remove, bubble c k' v l' r)

178 GT -> let (fl, r') = up r in

158 GT -> let (fl, r') = up r in

179 case fl of

159 case fl of

180 Same -> (Same, RBNode c k' v l r')

160 Same -> (Same, RBNode c k' v l r')

181− Insert -> (Insert, fixUp <| RBNode c k' v l r')

161+ Insert -> (Insert, balance c k' v l r')

182 Remove -> (Remove, bubble c k' v l r')

162 Remove -> (Remove, bubble c k' v l r')

183 (fl, t') = up t

163 (fl, t') = up t

184 in case fl of

164 in case fl of

185 Same -> t'

165 Same -> t'

186 Insert -> ensureBlackRoot t'

166 Insert -> ensureBlackRoot t'

187 Remove -> blacken t'

167 Remove -> blacken t'

188−

168+

189{-| Create a dictionary with one key-value pair. -}

169{-| Create a dictionary with one key-value pair. -}

190singleton : comparable -> v -> Dict comparable v

170singleton : comparable -> v -> Dict comparable v

191singleton k v = insert k v (RBEmpty LBlack)

171singleton k v = insert k v (RBEmpty LBlack)

192

172

193−{- Remove helpers: everything from here to remove should only be used

194− internally by remove as they would otherwise break rb-invariants -}

195−

196isBBlack : Dict k v -> Bool

173isBBlack : Dict k v -> Bool

197isBBlack t = case t of

174isBBlack t = case t of

198− RBNode c _ _ _ _ -> case c of

199− BBlack -> True

175+ RBNode BBlack _ _ _ _ -> True

200− _ -> False

201 RBEmpty LBBlack -> True

176 RBEmpty LBBlack -> True

202 _ -> False

177 _ -> False

203

178

204moreBlack : NColor -> NColor

179moreBlack : NColor -> NColor

205moreBlack c = case c of

180moreBlack c = case c of

206− BBlack -> BBlack

207 Black -> BBlack

181 Black -> BBlack

208 Red -> Black

182 Red -> Black

209 NBlack -> Red

183 NBlack -> Red

184+ BBlack -> Native.Error.raise "Can't make a double black node more black!"

185+

210lessBlack : NColor -> NColor

186lessBlack : NColor -> NColor

211lessBlack c = case c of

187lessBlack c = case c of

212 BBlack -> Black

188 BBlack -> Black

213 Black -> Red

189 Black -> Red

214 Red -> NBlack

190 Red -> NBlack

215− NBlack -> NBlack

191+ NBlack -> Native.Error.raise "Can't make a negative black node less black!"

216−

217−moreBlackTree : Dict k v -> Dict k v

218−moreBlackTree t = case t of

219− RBNode c k v l r -> RBNode (moreBlack c) k v l r

220− RBEmpty _ -> RBEmpty LBBlack

221

192

222lessBlackTree : Dict k v -> Dict k v

193lessBlackTree : Dict k v -> Dict k v

223lessBlackTree t = case t of

194lessBlackTree t = case t of

224 RBNode c k v l r -> RBNode (lessBlack c) k v l r

195 RBNode c k v l r -> RBNode (lessBlack c) k v l r

225− RBEmpty _ -> RBEmpty LBlack

196+ RBEmpty LBBlack -> RBEmpty LBlack

197+

198+reportRemBug : String -> NColor -> String -> String -> a

199+reportRemBug msg c lgot rgot =

200+ Native.Error.raise . String.concat <| [

201+ "Internal red-black tree invariant violated, expected ",

202+ msg,

203+ "and got",

204+ showNColor c,

205+ " ",

206+ lgot,

207+ " ",

208+ rgot,

209+ "\nPlease report this bug to https://github.com/evancz/Elm/issues"

210+ ]

226

211

227-- Remove the top node from the tree, may leave behind BBlacks

212-- Remove the top node from the tree, may leave behind BBlacks

228−rem : Dict k v -> Dict k v

213+rem : NColor -> Dict k v -> Dict k v -> Dict k v

229−rem t = case t of

214+rem c l r = case (l, r) of

230− RBNode c k v (RBEmpty _) (RBEmpty _) -> case c of

215+ ((RBEmpty _), (RBEmpty _)) -> case c of

231− Red -> RBEmpty LBlack

216+ Red -> RBEmpty LBlack

232 Black -> RBEmpty LBBlack

217 Black -> RBEmpty LBBlack

233− RBNode Black _ _ (RBEmpty _) (RBNode _ k v l r) ->

218+ ((RBEmpty cl), (RBNode cr k' v' l' r')) ->

219+ case (c, cl, cr) of

234− RBNode Black k v l r

220+ (Black, LBlack, Red) -> RBNode Black k' v' l' r'

221+ _ -> reportRemBug "Black, LBlack, Red" c (showLColor cl) (showNColor cr)

235− RBNode Black _ _ (RBNode _ k v l r) (RBEmpty _) ->

222+ ((RBNode cl k' v' l' r'), (RBEmpty cr)) ->

223+ case (c, cl, cr) of

236− RBNode Black k v l r

224+ (Black, Red, LBlack) -> RBNode Black k' v' l' r'

225+ _ -> reportRemBug "Black, Red, LBlack" c (showNColor cl) (showLColor cr)

237 -- l and r are both RBNodes

226 -- l and r are both RBNodes

238− RBNode c _ _ l r ->

227+ ((RBNode cl kl vl ll rl), (RBNode cr kr vr lr rr)) ->

228+ let l = RBNode cl kl vl ll rl

229+ r = RBNode cr kr vr lr rr

239− let (k, v) = max l

230+ (k, v) = max l

240− l' = remove_max l

231+ l' = remove_max cl kl vl ll rl

241 in bubble c k v l' r

232 in bubble c k v l' r

242

233

243-- Kills a BBlack or moves it upward, may leave behind NBlack

234-- Kills a BBlack or moves it upward, may leave behind NBlack

@@ -245,19 +236,24 @@ bubble : NColor -> k -> v -> Dict k v -> Dict k v -> Dict k v

245bubble c k v l r = if isBBlack l || isBBlack r

236bubble c k v l r = if isBBlack l || isBBlack r

246 then balance (moreBlack c) k v (lessBlackTree l) (lessBlackTree r)

237 then balance (moreBlack c) k v (lessBlackTree l) (lessBlackTree r)

247 else RBNode c k v l r

238 else RBNode c k v l r

248−

239+

249-- Removes rightmost node, may leave root as BBlack

240-- Removes rightmost node, may leave root as BBlack

250−remove_max : Dict k v -> Dict k v

241+remove_max : NColor -> k -> v -> Dict k v -> Dict k v -> Dict k v

251−remove_max t = case t of

242+remove_max c k v l r = case r of

252− RBNode c k v l (RBEmpty _) -> rem t

243+ RBEmpty _ -> rem c l r

244+ RBNode cr kr vr lr rr

253− RBNode c k v l r -> bubble c k v l (remove_max r)

245+ -> bubble c k v l (remove_max cr kr vr lr rr)

254

246

255-- generalized tree balancing act

247-- generalized tree balancing act

256balance : NColor -> k -> v -> Dict k v -> Dict k v -> Dict k v

248balance : NColor -> k -> v -> Dict k v -> Dict k v -> Dict k v

249+balance c k v l r =

250+

257−balance c k v l r = balance_node (RBNode c k v l r)

251+ balance_node (RBNode c k v l r)

258

252

259blackish : Dict k v -> Bool

253blackish : Dict k v -> Bool

254+blackish t = case t of

260−blackish (RBNode c _ _ _ _) = c == Black || c == BBlack

255+ RBNode c _ _ _ _ -> c == Black || c == BBlack

256+ RBEmpty _ -> True

261

257

262balance_node : Dict k v -> Dict k v

258balance_node : Dict k v -> Dict k v

263balance_node t =

259balance_node t =

@@ -286,9 +282,7 @@ balance_node t =

286 (RBNode Black _ _ _ _) ->

282 (RBNode Black _ _ _ _) ->

287 RBNode Black yk yv (balance Black xk xv (redden a) b) (RBNode Black zk zv c d)

283 RBNode Black yk yv (balance Black xk xv (redden a) b) (RBNode Black zk zv c d)

288 _ -> t

284 _ -> t

289−

290 _ -> t

285 _ -> t

291−

292 else t

286 else t

293

287

294-- make the top node black

288-- make the top node black