2 (***********************************************************************)
4 (* Copyright (C) Jean-Christophe Filliatre *)
6 (* This software is free software; you can redistribute it and/or *)
7 (* modify it under the terms of the GNU Library General Public *)
8 (* License version 2.1, with the special exception on linking *)
9 (* described in file http://www.lri.fr/~filliatr/ftp/ocaml/ds/LICENSE *)
11 (* This software is distributed in the hope that it will be useful, *)
12 (* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
13 (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
15 (***********************************************************************)
18 Time-stamp: <Last modified on 2013-03-10 18:18:54 CET by Kim Nguyen>
21 (* Modified by Kim Nguyen *)
22 (* The Patricia trees are themselves deeply hash-consed. The module
23 provides a Make (and Weak) functor to build hash-consed patricia
24 trees whose elements are Abstract hash-consed values.
31 module type HConsBuilder =
32 functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
34 module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
35 S with type elt = H.t =
42 | Branch of int * int * 'a * 'a
44 module rec Node : Hcons.S with type data = Data.t = HCB(Data)
45 and Data : Common_sig.HashedType with type t = Node.t set =
51 | Leaf k1, Leaf k2 -> k1 == k2
52 | Branch(b1,i1,l1,r1), Branch(b2,i2,l2,r2) ->
53 b1 == b2 && i1 == i2 && (Node.equal l1 l2) && (Node.equal r1 r2)
55 | (Empty|Leaf _|Branch _), _ -> false
59 | Leaf i -> HASHINT2 (PRIME1, Uid.to_int (H.uid i))
61 HASHINT4(b, i, Uid.to_int l.Node.id, Uid.to_int r.Node.id)
66 let empty = Node.make Empty
68 let is_empty s = (Node.node s) == Empty
70 let branch p m l r = Node.make (Branch(p,m,l,r))
72 let leaf k = Node.make (Leaf k)
74 (* To enforce the invariant that a branch contains two non empty
76 let branch_ne p m t0 t1 =
77 if (is_empty t0) then t1
78 else if is_empty t1 then t0 else branch p m t0 t1
80 (******** from here on, only use the smart constructors ************)
82 let zero_bit k m = (k land m) == 0
84 let singleton k = leaf k
87 match Node.node n with
89 | Branch _ | Empty -> false
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 ()