## lustrec / src / mmap.ml @ 32614c2d

History | View | Annotate | Download (10.7 KB)

1 | 40d33d55 | xavier.thirioux | (***********************************************************************) |
---|---|---|---|

2 | (* *) |
||

3 | (* OCaml *) |
||

4 | (* *) |
||

5 | (* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) |
||

6 | (* *) |
||

7 | (* Copyright 1996 Institut National de Recherche en Informatique et *) |
||

8 | (* en Automatique. All rights reserved. This file is distributed *) |
||

9 | (* under the terms of the GNU Library General Public License, with *) |
||

10 | (* the special exception on linking described in file ../LICENSE. *) |
||

11 | (* *) |
||

12 | (***********************************************************************) |
||

13 | |||

14 | module type OrderedType = |
||

15 | sig |
||

16 | type t |
||

17 | val compare: t -> t -> int |
||

18 | end |
||

19 | |||

20 | module type S = |
||

21 | sig |
||

22 | type key |
||

23 | type +'a t |
||

24 | val empty: 'a t |
||

25 | val is_empty: 'a t -> bool |
||

26 | val mem: key -> 'a t -> bool |
||

27 | val add: key -> 'a -> 'a t -> 'a t |
||

28 | val singleton: key -> 'a -> 'a t |
||

29 | val remove: key -> 'a t -> 'a t |
||

30 | val merge: |
||

31 | (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t |
||

32 | val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int |
||

33 | val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool |
||

34 | val iter: (key -> 'a -> unit) -> 'a t -> unit |
||

35 | val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b |
||

36 | val for_all: (key -> 'a -> bool) -> 'a t -> bool |
||

37 | val exists: (key -> 'a -> bool) -> 'a t -> bool |
||

38 | val filter: (key -> 'a -> bool) -> 'a t -> 'a t |
||

39 | val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t |
||

40 | val cardinal: 'a t -> int |
||

41 | val bindings: 'a t -> (key * 'a) list |
||

42 | val min_binding: 'a t -> (key * 'a) |
||

43 | val max_binding: 'a t -> (key * 'a) |
||

44 | val choose: 'a t -> (key * 'a) |
||

45 | val split: key -> 'a t -> 'a t * 'a option * 'a t |
||

46 | val find: key -> 'a t -> 'a |
||

47 | val map: ('a -> 'b) -> 'a t -> 'b t |
||

48 | val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t |
||

49 | end |
||

50 | |||

51 | module Make(Ord: OrderedType) = struct |
||

52 | |||

53 | type key = Ord.t |
||

54 | |||

55 | type 'a t = |
||

56 | Empty |
||

57 | | Node of 'a t * key * 'a * 'a t * int |
||

58 | |||

59 | let height = function |
||

60 | Empty -> 0 |
||

61 | | Node(_,_,_,_,h) -> h |
||

62 | |||

63 | let create l x d r = |
||

64 | let hl = height l and hr = height r in |
||

65 | Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1)) |
||

66 | |||

67 | let singleton x d = Node(Empty, x, d, Empty, 1) |
||

68 | |||

69 | let bal l x d r = |
||

70 | let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in |
||

71 | let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in |
||

72 | if hl > hr + 2 then begin |
||

73 | match l with |
||

74 | Empty -> invalid_arg "Map.bal" |
||

75 | | Node(ll, lv, ld, lr, _) -> |
||

76 | if height ll >= height lr then |
||

77 | create ll lv ld (create lr x d r) |
||

78 | else begin |
||

79 | match lr with |
||

80 | Empty -> invalid_arg "Map.bal" |
||

81 | | Node(lrl, lrv, lrd, lrr, _)-> |
||

82 | create (create ll lv ld lrl) lrv lrd (create lrr x d r) |
||

83 | end |
||

84 | end else if hr > hl + 2 then begin |
||

85 | match r with |
||

86 | Empty -> invalid_arg "Map.bal" |
||

87 | | Node(rl, rv, rd, rr, _) -> |
||

88 | if height rr >= height rl then |
||

89 | create (create l x d rl) rv rd rr |
||

90 | else begin |
||

91 | match rl with |
||

92 | Empty -> invalid_arg "Map.bal" |
||

93 | | Node(rll, rlv, rld, rlr, _) -> |
||

94 | create (create l x d rll) rlv rld (create rlr rv rd rr) |
||

95 | end |
||

96 | end else |
||

97 | Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1)) |
||

98 | |||

99 | let empty = Empty |
||

100 | |||

101 | let is_empty = function Empty -> true | _ -> false |
||

102 | |||

103 | let rec add x data = function |
||

104 | Empty -> |
||

105 | Node(Empty, x, data, Empty, 1) |
||

106 | | Node(l, v, d, r, h) -> |
||

107 | let c = Ord.compare x v in |
||

108 | if c = 0 then |
||

109 | Node(l, x, data, r, h) |
||

110 | else if c < 0 then |
||

111 | bal (add x data l) v d r |
||

112 | else |
||

113 | bal l v d (add x data r) |
||

114 | |||

115 | let rec find x = function |
||

116 | Empty -> |
||

117 | raise Not_found |
||

118 | | Node(l, v, d, r, _) -> |
||

119 | let c = Ord.compare x v in |
||

120 | if c = 0 then d |
||

121 | else find x (if c < 0 then l else r) |
||

122 | |||

123 | let rec mem x = function |
||

124 | Empty -> |
||

125 | false |
||

126 | | Node(l, v, d, r, _) -> |
||

127 | let c = Ord.compare x v in |
||

128 | c = 0 || mem x (if c < 0 then l else r) |
||

129 | |||

130 | let rec min_binding = function |
||

131 | Empty -> raise Not_found |
||

132 | | Node(Empty, x, d, r, _) -> (x, d) |
||

133 | | Node(l, x, d, r, _) -> min_binding l |
||

134 | |||

135 | let rec max_binding = function |
||

136 | Empty -> raise Not_found |
||

137 | | Node(l, x, d, Empty, _) -> (x, d) |
||

138 | | Node(l, x, d, r, _) -> max_binding r |
||

139 | |||

140 | let rec remove_min_binding = function |
||

141 | Empty -> invalid_arg "Map.remove_min_elt" |
||

142 | | Node(Empty, x, d, r, _) -> r |
||

143 | | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r |
||

144 | |||

145 | let merge t1 t2 = |
||

146 | match (t1, t2) with |
||

147 | (Empty, t) -> t |
||

148 | | (t, Empty) -> t |
||

149 | | (_, _) -> |
||

150 | let (x, d) = min_binding t2 in |
||

151 | bal t1 x d (remove_min_binding t2) |
||

152 | |||

153 | let rec remove x = function |
||

154 | Empty -> |
||

155 | Empty |
||

156 | | Node(l, v, d, r, h) -> |
||

157 | let c = Ord.compare x v in |
||

158 | if c = 0 then |
||

159 | merge l r |
||

160 | else if c < 0 then |
||

161 | bal (remove x l) v d r |
||

162 | else |
||

163 | bal l v d (remove x r) |
||

164 | |||

165 | let rec iter f = function |
||

166 | Empty -> () |
||

167 | | Node(l, v, d, r, _) -> |
||

168 | iter f l; f v d; iter f r |
||

169 | |||

170 | let rec map f = function |
||

171 | Empty -> |
||

172 | Empty |
||

173 | | Node(l, v, d, r, h) -> |
||

174 | let l' = map f l in |
||

175 | let d' = f d in |
||

176 | let r' = map f r in |
||

177 | Node(l', v, d', r', h) |
||

178 | |||

179 | let rec mapi f = function |
||

180 | Empty -> |
||

181 | Empty |
||

182 | | Node(l, v, d, r, h) -> |
||

183 | let l' = mapi f l in |
||

184 | let d' = f v d in |
||

185 | let r' = mapi f r in |
||

186 | Node(l', v, d', r', h) |
||

187 | |||

188 | let rec fold f m accu = |
||

189 | match m with |
||

190 | Empty -> accu |
||

191 | | Node(l, v, d, r, _) -> |
||

192 | fold f r (f v d (fold f l accu)) |
||

193 | |||

194 | let rec for_all p = function |
||

195 | Empty -> true |
||

196 | | Node(l, v, d, r, _) -> p v d && for_all p l && for_all p r |
||

197 | |||

198 | let rec exists p = function |
||

199 | Empty -> false |
||

200 | | Node(l, v, d, r, _) -> p v d || exists p l || exists p r |
||

201 | |||

202 | (* Beware: those two functions assume that the added k is *strictly* |
||

203 | smaller (or bigger) than all the present keys in the tree; it |
||

204 | does not test for equality with the current min (or max) key. |
||

205 | |||

206 | Indeed, they are only used during the "join" operation which |
||

207 | respects this precondition. |
||

208 | *) |
||

209 | |||

210 | let rec add_min_binding k v = function |
||

211 | | Empty -> singleton k v |
||

212 | | Node (l, x, d, r, h) -> |
||

213 | bal (add_min_binding k v l) x d r |
||

214 | |||

215 | let rec add_max_binding k v = function |
||

216 | | Empty -> singleton k v |
||

217 | | Node (l, x, d, r, h) -> |
||

218 | bal l x d (add_max_binding k v r) |
||

219 | |||

220 | (* Same as create and bal, but no assumptions are made on the |
||

221 | relative heights of l and r. *) |
||

222 | |||

223 | let rec join l v d r = |
||

224 | match (l, r) with |
||

225 | (Empty, _) -> add_min_binding v d r |
||

226 | | (_, Empty) -> add_max_binding v d l |
||

227 | | (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) -> |
||

228 | if lh > rh + 2 then bal ll lv ld (join lr v d r) else |
||

229 | if rh > lh + 2 then bal (join l v d rl) rv rd rr else |
||

230 | create l v d r |
||

231 | |||

232 | (* Merge two trees l and r into one. |
||

233 | All elements of l must precede the elements of r. |
||

234 | No assumption on the heights of l and r. *) |
||

235 | |||

236 | let concat t1 t2 = |
||

237 | match (t1, t2) with |
||

238 | (Empty, t) -> t |
||

239 | | (t, Empty) -> t |
||

240 | | (_, _) -> |
||

241 | let (x, d) = min_binding t2 in |
||

242 | join t1 x d (remove_min_binding t2) |
||

243 | |||

244 | let concat_or_join t1 v d t2 = |
||

245 | match d with |
||

246 | | Some d -> join t1 v d t2 |
||

247 | | None -> concat t1 t2 |
||

248 | |||

249 | let rec split x = function |
||

250 | Empty -> |
||

251 | (Empty, None, Empty) |
||

252 | | Node(l, v, d, r, _) -> |
||

253 | let c = Ord.compare x v in |
||

254 | if c = 0 then (l, Some d, r) |
||

255 | else if c < 0 then |
||

256 | let (ll, pres, rl) = split x l in (ll, pres, join rl v d r) |
||

257 | else |
||

258 | let (lr, pres, rr) = split x r in (join l v d lr, pres, rr) |
||

259 | |||

260 | let rec merge f s1 s2 = |
||

261 | match (s1, s2) with |
||

262 | (Empty, Empty) -> Empty |
||

263 | | (Node (l1, v1, d1, r1, h1), _) when h1 >= height s2 -> |
||

264 | let (l2, d2, r2) = split v1 s2 in |
||

265 | concat_or_join (merge f l1 l2) v1 (f v1 (Some d1) d2) (merge f r1 r2) |
||

266 | | (_, Node (l2, v2, d2, r2, h2)) -> |
||

267 | let (l1, d1, r1) = split v2 s1 in |
||

268 | concat_or_join (merge f l1 l2) v2 (f v2 d1 (Some d2)) (merge f r1 r2) |
||

269 | | _ -> |
||

270 | assert false |
||

271 | |||

272 | let rec filter p = function |
||

273 | Empty -> Empty |
||

274 | | Node(l, v, d, r, _) -> |
||

275 | (* call [p] in the expected left-to-right order *) |
||

276 | let l' = filter p l in |
||

277 | let pvd = p v d in |
||

278 | let r' = filter p r in |
||

279 | if pvd then join l' v d r' else concat l' r' |
||

280 | |||

281 | let rec partition p = function |
||

282 | Empty -> (Empty, Empty) |
||

283 | | Node(l, v, d, r, _) -> |
||

284 | (* call [p] in the expected left-to-right order *) |
||

285 | let (lt, lf) = partition p l in |
||

286 | let pvd = p v d in |
||

287 | let (rt, rf) = partition p r in |
||

288 | if pvd |
||

289 | then (join lt v d rt, concat lf rf) |
||

290 | else (concat lt rt, join lf v d rf) |
||

291 | |||

292 | type 'a enumeration = End | More of key * 'a * 'a t * 'a enumeration |
||

293 | |||

294 | let rec cons_enum m e = |
||

295 | match m with |
||

296 | Empty -> e |
||

297 | | Node(l, v, d, r, _) -> cons_enum l (More(v, d, r, e)) |
||

298 | |||

299 | let compare cmp m1 m2 = |
||

300 | let rec compare_aux e1 e2 = |
||

301 | match (e1, e2) with |
||

302 | (End, End) -> 0 |
||

303 | | (End, _) -> -1 |
||

304 | | (_, End) -> 1 |
||

305 | | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) -> |
||

306 | let c = Ord.compare v1 v2 in |
||

307 | if c <> 0 then c else |
||

308 | let c = cmp d1 d2 in |
||

309 | if c <> 0 then c else |
||

310 | compare_aux (cons_enum r1 e1) (cons_enum r2 e2) |
||

311 | in compare_aux (cons_enum m1 End) (cons_enum m2 End) |
||

312 | |||

313 | let equal cmp m1 m2 = |
||

314 | let rec equal_aux e1 e2 = |
||

315 | match (e1, e2) with |
||

316 | (End, End) -> true |
||

317 | | (End, _) -> false |
||

318 | | (_, End) -> false |
||

319 | | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) -> |
||

320 | Ord.compare v1 v2 = 0 && cmp d1 d2 && |
||

321 | equal_aux (cons_enum r1 e1) (cons_enum r2 e2) |
||

322 | in equal_aux (cons_enum m1 End) (cons_enum m2 End) |
||

323 | |||

324 | let rec cardinal = function |
||

325 | Empty -> 0 |
||

326 | | Node(l, _, _, r, _) -> cardinal l + 1 + cardinal r |
||

327 | |||

328 | let rec bindings_aux accu = function |
||

329 | Empty -> accu |
||

330 | | Node(l, v, d, r, _) -> bindings_aux ((v, d) :: bindings_aux accu r) l |
||

331 | |||

332 | let bindings s = |
||

333 | bindings_aux [] s |
||

334 | |||

335 | let choose = min_binding |
||

336 | |||

337 | end |