3 (***********************************************************************)
5 (* Copyright (C) Jean-Christophe Filliatre *)
7 (* This software is free software; you can redistribute it and/or *)
8 (* modify it under the terms of the GNU Library General Public *)
9 (* License version 2.1, with the special exception on linking *)
10 (* described in file http://www.lri.fr/~filliatr/ftp/ocaml/ds/LICENSE *)
12 (* This software is distributed in the hope that it will be useful, *)
13 (* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
14 (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
16 (***********************************************************************)
18 (* Modified by Kim Nguyen *)
19 (* The Patricia trees are themselves deeply hashconsed. The module
20 provides a Make (and Weak) functor to build hashconsed patricia
21 trees whose elements are Abstract hashconsed values. This allows
22 to build sets of integers without boxing them in an hacons structure
29 include Hcons.S with type t := t
32 module type HConsBuilder =
33 functor (H : Sigs.HashedType) -> Hcons.S with type data = H.t
35 module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
36 S with type elt = H.t =
43 | Branch of int * int * 'a * 'a
45 module rec Node : Hcons.S with type data = Data.t = HCB(Data)
46 and Data : Sigs.HashedType with type t = Node.t set =
52 | Leaf k1, Leaf k2 -> k1 == k2
53 | Branch(b1,i1,l1,r1),Branch(b2,i2,l2,r2) ->
54 b1 == b2 && i1 == i2 && (Node.equal l1 l2) && (Node.equal r1 r2)
60 | Leaf i -> HASHINT2 (PRIME1, Uid.to_int (H.uid i))
62 HASHINT4(b, i, Uid.to_int l.Node.id, Uid.to_int r.Node.id)
67 let empty = Node.make Empty
69 let is_empty s = (Node.node s) == Empty
71 let branch p m l r = Node.make (Branch(p,m,l,r))
73 let leaf k = Node.make (Leaf k)
75 (* To enforce the invariant that a branch contains two non empty
77 let branch_ne p m t0 t1 =
78 if (is_empty t0) then t1
79 else if is_empty t1 then t0 else branch p m t0 t1
81 (******** from here on, only use the smart constructors ************)
83 let zero_bit k m = (k land m) == 0
85 let singleton k = leaf k
88 match Node.node n with Leaf _ -> true
92 let kid = Uid.to_int (H.uid k) in
93 let rec loop n = match Node.node n with
96 | Branch (p, _, l, r) -> if kid <= p then loop l else loop r
99 let rec min_elt n = match Node.node n with
100 | Empty -> raise Not_found
102 | Branch (_,_,s,_) -> min_elt s
104 let rec max_elt n = match Node.node n with
105 | Empty -> raise Not_found
107 | Branch (_,_,_,t) -> max_elt t
110 let rec elements_aux acc n = match Node.node n with
113 | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
117 let mask k m = (k lor (m-1)) land (lnot m)
119 let naive_highest_bit x =
122 if i = 0 then 1 else if x lsr i = 1 then 1 lsl i else loop (i-1)
126 let hbit = Array.init 256 naive_highest_bit
128 external clz : int -> int = "caml_clz" "noalloc"
129 external leading_bit : int -> int = "caml_leading_bit" "noalloc"
133 let n = (x) lsr 24 in
134 if n != 0 then hbit.(n) lsl 24
135 else let n = (x) lsr 16 in if n != 0 then hbit.(n) lsl 16
136 else let n = (x) lsr 8 in if n != 0 then hbit.(n) lsl 8
139 _ -> raise (Invalid_argument ("highest_bit " ^ (string_of_int x)))
141 let highest_bit64 x =
142 let n = x lsr 32 in if n != 0 then highest_bit n lsl 32
145 let branching_bit p0 p1 = highest_bit64 (p0 lxor p1)
147 let join p0 t0 p1 t1 =
148 let m = branching_bit p0 p1 in
149 let msk = mask p0 m in
150 if zero_bit p0 m then
151 branch_ne msk m t0 t1
153 branch_ne msk m t1 t0
155 let match_prefix k p m = (mask k m) == p
158 let kid = Uid.to_int (H.uid k) in
160 let rec ins n = match Node.node n with
162 | Leaf j -> if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n
163 | Branch (p,m,t0,t1) ->
164 if match_prefix kid p m then
165 if zero_bit kid m then
166 branch_ne p m (ins t0) t1
168 branch_ne p m t0 (ins t1)
170 join kid (leaf k) p n
175 let kid = Uid.to_int(H.uid k) in
176 let rec rmv n = match Node.node n with
178 | Leaf j -> if k == j then empty else n
179 | Branch (p,m,t0,t1) ->
180 if match_prefix kid p m then
181 if zero_bit kid m then
182 branch_ne p m (rmv t0) t1
184 branch_ne p m t0 (rmv t1)
190 (* should run in O(1) thanks to Hash consing *)
192 let equal a b = Node.equal a b
194 let compare a b = (Uid.to_int (Node.uid a)) - (Uid.to_int (Node.uid b))
197 if (equal s t) (* This is cheap thanks to hash-consing *)
200 match Node.node s, Node.node t with
203 | Leaf k, _ -> add k t
204 | _, Leaf k -> add k s
205 | Branch (p,m,s0,s1), Branch (q,n,t0,t1) ->
206 if m == n && match_prefix q p m then
207 branch p m (merge s0 t0) (merge s1 t1)
208 else if m > n && match_prefix q p m then
210 branch_ne p m (merge s0 t) s1
212 branch_ne p m s0 (merge s1 t)
213 else if m < n && match_prefix p q n then
215 branch_ne q n (merge s t0) t1
217 branch_ne q n t0 (merge s t1)
219 (* The prefixes disagree. *)
225 let rec subset s1 s2 = (equal s1 s2) ||
226 match (Node.node s1,Node.node s2) with
229 | Leaf k1, _ -> mem k1 s2
230 | Branch _, Leaf _ -> false
231 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
232 if m1 == m2 && p1 == p2 then
233 subset l1 l2 && subset r1 r2
234 else if m1 < m2 && match_prefix p1 p2 m2 then
235 if zero_bit p1 m2 then
236 subset l1 l2 && subset r1 l2
238 subset l1 r2 && subset r1 r2
243 let union s1 s2 = merge s1 s2
244 (* Todo replace with e Memo Module *)
246 let rec inter s1 s2 =
250 match (Node.node s1,Node.node s2) with
253 | Leaf k1, _ -> if mem k1 s2 then s1 else empty
254 | _, Leaf k2 -> if mem k2 s1 then s2 else empty
255 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
256 if m1 == m2 && p1 == p2 then
257 merge (inter l1 l2) (inter r1 r2)
258 else if m1 > m2 && match_prefix p2 p1 m1 then
259 inter (if zero_bit p2 m1 then l1 else r1) s2
260 else if m1 < m2 && match_prefix p1 p2 m2 then
261 inter s1 (if zero_bit p1 m2 then l2 else r2)
269 match (Node.node s1,Node.node s2) with
272 | Leaf k1, _ -> if mem k1 s2 then empty else s1
273 | _, Leaf k2 -> remove k2 s1
274 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
275 if m1 == m2 && p1 == p2 then
276 merge (diff l1 l2) (diff r1 r2)
277 else if m1 > m2 && match_prefix p2 p1 m1 then
278 if zero_bit p2 m1 then
279 merge (diff l1 s2) r1
281 merge l1 (diff r1 s2)
282 else if m1 < m2 && match_prefix p1 p2 m2 then
283 if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
288 (*s All the following operations ([cardinal], [iter], [fold], [for_all],
289 [exists], [filter], [partition], [choose], [elements]) are
290 implemented as for any other kind of binary trees. *)
292 let rec cardinal n = match Node.node n with
295 | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
297 let rec iter f n = match Node.node n with
300 | Branch (_,_,t0,t1) -> iter f t0; iter f t1
302 let rec fold f s accu = match Node.node s with
305 | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
308 let rec for_all p n = match Node.node n with
311 | Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1
313 let rec exists p n = match Node.node n with
316 | Branch (_,_,t0,t1) -> exists p t0 || exists p t1
318 let rec filter pr n = match Node.node n with
320 | Leaf k -> if pr k then n else empty
321 | Branch (p,m,t0,t1) -> branch_ne p m (filter pr t0) (filter pr t1)
324 let rec part (t,f as acc) n = match Node.node n with
326 | Leaf k -> if p k then (add k t, f) else (t, add k f)
327 | Branch (_,_,t0,t1) -> part (part acc t0) t1
329 part (empty, empty) s
331 let rec choose n = match Node.node n with
332 | Empty -> raise Not_found
334 | Branch (_, _,t0,_) -> choose t0 (* we know that [t0] is non-empty *)
338 let coll k (l, b, r) =
339 if k < x then add k l, b, r
340 else if k > x then l, b, add k r
343 fold coll s (empty, false, empty)
345 (*s Additional functions w.r.t to [Set.S]. *)
347 let rec intersect s1 s2 = (equal s1 s2) ||
348 match (Node.node s1,Node.node s2) with
351 | Leaf k1, _ -> mem k1 s2
352 | _, Leaf k2 -> mem k2 s1
353 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
354 if m1 == m2 && p1 == p2 then
355 intersect l1 l2 || intersect r1 r2
356 else if m1 < m2 && match_prefix p2 p1 m1 then
357 intersect (if zero_bit p2 m1 then l1 else r1) s2
358 else if m1 > m2 && match_prefix p1 p2 m2 then
359 intersect s1 (if zero_bit p1 m2 then l2 else r2)
364 let from_list l = List.fold_left (fun acc e -> add e acc) empty l
369 module Make = Builder(Hcons.Make)
370 module Weak = Builder(Hcons.Weak)
375 include Make(Hcons.PosInt)
377 Format.pp_print_string ppf "{ ";
378 iter (fun i -> Format.fprintf ppf "%i " i) s;
379 Format.pp_print_string ppf "}";
380 Format.pp_print_flush ppf ()