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-01-30 19:07:53 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 : Sigs.AUX.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 : Sigs.AUX.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)
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 Leaf _ -> true
91 let kid = Uid.to_int (H.uid k) in
92 let rec loop n = match Node.node n with
95 | Branch (p, _, l, r) -> if kid <= p then loop l else loop r
98 let rec min_elt n = match Node.node n with
99 | Empty -> raise Not_found
101 | Branch (_,_,s,_) -> min_elt s
103 let rec max_elt n = match Node.node n with
104 | Empty -> raise Not_found
106 | Branch (_,_,_,t) -> max_elt t
109 let rec elements_aux acc n = match Node.node n with
112 | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
116 let mask k m = (k lor (m-1)) land (lnot m)
118 let naive_highest_bit x =
121 if i = 0 then 1 else if x lsr i = 1 then 1 lsl i else loop (i-1)
125 let hbit = Array.init 256 naive_highest_bit
127 external clz : int -> int = "caml_clz" "noalloc"
128 external leading_bit : int -> int = "caml_leading_bit" "noalloc"
132 let n = (x) lsr 24 in
133 if n != 0 then hbit.(n) lsl 24
134 else let n = (x) lsr 16 in if n != 0 then hbit.(n) lsl 16
135 else let n = (x) lsr 8 in if n != 0 then hbit.(n) lsl 8
138 _ -> raise (Invalid_argument ("highest_bit " ^ (string_of_int x)))
140 let highest_bit64 x =
141 let n = x lsr 32 in if n != 0 then highest_bit n lsl 32
144 let branching_bit p0 p1 = highest_bit64 (p0 lxor p1)
146 let join p0 t0 p1 t1 =
147 let m = branching_bit p0 p1 in
148 let msk = mask p0 m in
149 if zero_bit p0 m then
150 branch_ne msk m t0 t1
152 branch_ne msk m t1 t0
154 let match_prefix k p m = (mask k m) == p
157 let kid = Uid.to_int (H.uid k) in
159 let rec ins n = match Node.node n with
161 | Leaf j -> if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n
162 | Branch (p,m,t0,t1) ->
163 if match_prefix kid p m then
164 if zero_bit kid m then
165 branch_ne p m (ins t0) t1
167 branch_ne p m t0 (ins t1)
169 join kid (leaf k) p n
174 let kid = Uid.to_int(H.uid k) in
175 let rec rmv n = match Node.node n with
177 | Leaf j -> if k == j then empty else n
178 | Branch (p,m,t0,t1) ->
179 if match_prefix kid p m then
180 if zero_bit kid m then
181 branch_ne p m (rmv t0) t1
183 branch_ne p m t0 (rmv t1)
189 (* should run in O(1) thanks to hash consing *)
191 let equal a b = Node.equal a b
193 let compare a b = (Uid.to_int (Node.uid a)) - (Uid.to_int (Node.uid b))
196 if equal s t (* This is cheap thanks to hash-consing *)
199 match Node.node s, Node.node t with
202 | Leaf k, _ -> add k t
203 | _, Leaf k -> add k s
204 | Branch (p,m,s0,s1), Branch (q,n,t0,t1) ->
205 if m == n && match_prefix q p m then
206 branch p m (merge s0 t0) (merge s1 t1)
207 else if m > n && match_prefix q p m then
209 branch_ne p m (merge s0 t) s1
211 branch_ne p m s0 (merge s1 t)
212 else if m < n && match_prefix p q n then
214 branch_ne q n (merge s t0) t1
216 branch_ne q n t0 (merge s t1)
218 (* The prefixes disagree. *)
224 let rec subset s1 s2 = (equal s1 s2) ||
225 match (Node.node s1,Node.node s2) with
228 | Leaf k1, _ -> mem k1 s2
229 | Branch _, Leaf _ -> false
230 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
231 if m1 == m2 && p1 == p2 then
232 subset l1 l2 && subset r1 r2
233 else if m1 < m2 && match_prefix p1 p2 m2 then
234 if zero_bit p1 m2 then
235 subset l1 l2 && subset r1 l2
237 subset l1 r2 && subset r1 r2
242 let union s1 s2 = merge s1 s2
243 (* Todo replace with e Memo Module *)
245 let rec inter s1 s2 =
249 match (Node.node s1,Node.node s2) with
252 | Leaf k1, _ -> if mem k1 s2 then s1 else empty
253 | _, Leaf k2 -> if mem k2 s1 then s2 else empty
254 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
255 if m1 == m2 && p1 == p2 then
256 merge (inter l1 l2) (inter r1 r2)
257 else if m1 > m2 && match_prefix p2 p1 m1 then
258 inter (if zero_bit p2 m1 then l1 else r1) s2
259 else if m1 < m2 && match_prefix p1 p2 m2 then
260 inter s1 (if zero_bit p1 m2 then l2 else r2)
268 match (Node.node s1,Node.node s2) with
271 | Leaf k1, _ -> if mem k1 s2 then empty else s1
272 | _, Leaf k2 -> remove k2 s1
273 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
274 if m1 == m2 && p1 == p2 then
275 merge (diff l1 l2) (diff r1 r2)
276 else if m1 > m2 && match_prefix p2 p1 m1 then
277 if zero_bit p2 m1 then
278 merge (diff l1 s2) r1
280 merge l1 (diff r1 s2)
281 else if m1 < m2 && match_prefix p1 p2 m2 then
282 if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
287 (*s All the following operations ([cardinal], [iter], [fold], [for_all],
288 [exists], [filter], [partition], [choose], [elements]) are
289 implemented as for any other kind of binary trees. *)
291 let rec cardinal n = match Node.node n with
294 | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
296 let rec iter f n = match Node.node n with
299 | Branch (_,_,t0,t1) -> iter f t0; iter f t1
301 let rec fold f s accu = match Node.node s with
304 | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
307 let rec for_all p n = match Node.node n with
310 | Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1
312 let rec exists p n = match Node.node n with
315 | Branch (_,_,t0,t1) -> exists p t0 || exists p t1
317 let rec filter pr n = match Node.node n with
319 | Leaf k -> if pr k then n else empty
320 | Branch (p,m,t0,t1) -> branch_ne p m (filter pr t0) (filter pr t1)
323 let rec part (t,f as acc) n = match Node.node n with
325 | Leaf k -> if p k then (add k t, f) else (t, add k f)
326 | Branch (_,_,t0,t1) -> part (part acc t0) t1
328 part (empty, empty) s
330 let rec choose n = match Node.node n with
331 | Empty -> raise Not_found
333 | Branch (_, _,t0,_) -> choose t0 (* we know that [t0] is non-empty *)
337 let coll k (l, b, r) =
338 if k < x then add k l, b, r
339 else if k > x then l, b, add k r
342 fold coll s (empty, false, empty)
344 (*s Additional functions w.r.t to [Set.S]. *)
346 let rec intersect s1 s2 = (equal s1 s2) ||
347 match (Node.node s1,Node.node s2) with
350 | Leaf k1, _ -> mem k1 s2
351 | _, Leaf k2 -> mem k2 s1
352 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
353 if m1 == m2 && p1 == p2 then
354 intersect l1 l2 || intersect r1 r2
355 else if m1 < m2 && match_prefix p2 p1 m1 then
356 intersect (if zero_bit p2 m1 then l1 else r1) s2
357 else if m1 > m2 && match_prefix p1 p2 m2 then
358 intersect s1 (if zero_bit p1 m2 then l2 else r2)
363 let from_list l = List.fold_left (fun acc e -> add e acc) empty l
368 module Make = Builder(Hcons.Make)
369 module Weak = Builder(Hcons.Weak)
374 include Make(Hcons.PosInt)
376 Format.pp_print_string ppf "{ ";
377 iter (fun i -> Format.fprintf ppf "%i " i) s;
378 Format.pp_print_string ppf "}";
379 Format.pp_print_flush ppf ()