package codex
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
The Codex library for building static analysers based on abstract interpretation
Install
dune-project
Dependency
Authors
Maintainers
Sources
1.0-rc4.tar.gz
md5=bc7266a140c6886add673ede90e335d3
sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386
doc/src/codex.het-hashtbl/hetHashtbl.ml.html
Source file hetHashtbl.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400(**************************************************************************) (* This file is part of the Codex semantics library. *) (* *) (* Copyright (C) 2013-2025 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) (* you can redistribute it and/or modify it under the terms of the GNU *) (* Lesser General Public License as published by the Free Software *) (* Foundation, version 2.1. *) (* *) (* It is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU Lesser General Public License for more details. *) (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file LICENSE). *) (* *) (**************************************************************************) (* Most of this code is adapated from the OCaml Standard library's implementation of Hashtbl. Copyright 1996 Institut National de Recherche en Informatique et en Automatique. distributed under the terms of the GNU Lesser General Public License version 2.1, with the special exception on linking described in the license *) (* Hash tables *) module type HETEROGENEOUS_HASHED_TYPE = sig type 'a t val polyeq: 'a t -> 'b t -> ('a, 'b) PatriciaTree.cmp val hash: 'a t -> int end module type HETEROGENEOUS_SEEDED_HASHED_TYPE = sig type 'a t val polyeq: 'a t -> 'b t -> ('a, 'b) PatriciaTree.cmp val hash: int -> 'a t -> int end module type S = sig type 'a t type 'key key type ('key, 'a) value type 'b key_value = KeyValue : 'a key * ('a, 'b) value -> 'b key_value val create : ?random:bool -> int -> 'a t val clear : 'a t -> unit val reset : 'a t -> unit val copy : 'a t -> 'a t val add : 'a t -> 'key key -> ('key, 'a) value -> unit val remove : 'a t -> 'b key -> unit val find : 'a t -> 'key key -> ('key, 'a) value val find_opt : 'a t -> 'key key -> ('key, 'a) value option val find_all : 'a t -> 'key key -> ('key, 'a) value list val replace : 'a t -> 'key key -> ('key, 'a) value -> unit val mem : 'a t -> 'key key -> bool val add_seq : 'a t -> 'a key_value Seq.t -> unit val replace_seq : 'a t -> 'a key_value Seq.t -> unit val of_seq : 'a key_value Seq.t -> 'a t type 'a polyiter = { f : 'key. 'key key -> ('key, 'a) value -> unit; } [@@unboxed] val iter : 'a polyiter -> 'a t -> unit type ('a, 'b) polyfiltermap = { f : 'key. 'key key -> ('key, 'a) value -> ('key, 'b) value option; } [@@unboxed] val filter_map_inplace : ('a, 'a) polyfiltermap -> 'a t -> unit type ('a, 'acc) polyfold = { f : 'key. 'key key -> ('key, 'a) value -> 'acc -> 'acc; } [@@unboxed] val fold : ('a, 'acc) polyfold -> 'a t -> 'acc -> 'acc val length : 'a t -> int val stats : 'a t -> Hashtbl.statistics val to_seq : 'a t -> unit -> 'a key_value Seq.node end let is_randomized = Hashtbl.is_randomized let prng = lazy (Random.State.make_self_init()) (* Functions which appear before the functorial interface must either be independent of the hash function or take it as a parameter (see #2202 and code below the functor definitions. *) (* Creating a fresh, empty table *) let rec power_2_above x n = if x >= n then x else if x * 2 > Sys.max_array_length then x else power_2_above (x * 2) n module MakeSeeded(Key: HETEROGENEOUS_SEEDED_HASHED_TYPE)(Value: PatriciaTree.HETEROGENEOUS_VALUE) = struct type 'value t = { mutable size: int; (* number of entries *) mutable data: 'value bucketlist array; (* the buckets *) seed: int; (* for randomization *) mutable initial_size: int; (* initial array size *) } and 'value bucketlist = | Empty | Cons : { mutable key: 'key Key.t; mutable data: ('key, 'value) Value.t; mutable next: 'value bucketlist } -> 'value bucketlist type 'a key = 'a Key.t type ('a, 'b) value = ('a, 'b) Value.t let create ?(random ) initial_size = let s = power_2_above 16 initial_size in let random = match random with | Some bool -> bool | None -> is_randomized () in let seed = if random then Random.State.bits (Lazy.force prng) else 0 in { initial_size = s; size = 0; seed = seed; data = Array.make s Empty } let clear h = if h.size > 0 then begin h.size <- 0; Array.fill h.data 0 (Array.length h.data) Empty end let reset h = let len = Array.length h.data in if len = abs h.initial_size then clear h else begin h.size <- 0; h.data <- Array.make (abs h.initial_size) Empty end let copy_bucketlist = function | Empty -> Empty | Cons {key; data; next} -> let rec loop prec = function | Empty -> () | Cons {key; data; next} -> let r = Cons {key; data; next} in begin match prec with | Empty -> assert false | Cons prec -> prec.next <- r end; loop r next in let r = Cons {key; data; next} in loop r next; r let copy h = { h with data = Array.map copy_bucketlist h.data } let key_index h key = (Key.hash h.seed key) land (Array.length h.data - 1) let ongoing_traversal h = h.initial_size < 0 let flip_ongoing_traversal h = h.initial_size <- - h.initial_size type index_fun = { f : 'a. 'a key -> int } [@@unboxed] let insert_all_buckets indexfun inplace odata ndata = let nsize = Array.length ndata in let ndata_tail = Array.make nsize Empty in let rec insert_bucket = function | Empty -> () | Cons {key; data; next} as cell -> let cell = if inplace then cell else Cons {key; data; next = Empty} in let nidx = indexfun.f key in begin match ndata_tail.(nidx) with | Empty -> ndata.(nidx) <- cell; | Cons tail -> tail.next <- cell; end; ndata_tail.(nidx) <- cell; insert_bucket next in for i = 0 to Array.length odata - 1 do insert_bucket odata.(i) done; if inplace then for i = 0 to nsize - 1 do match ndata_tail.(i) with | Empty -> () | Cons tail -> tail.next <- Empty done let resize indexfun h = let odata = h.data in let osize = Array.length odata in let nsize = osize * 2 in if nsize < Sys.max_array_length then begin let ndata = Array.make nsize Empty in let inplace = not (ongoing_traversal h) in h.data <- ndata; (* so that indexfun sees the new bucket count *) insert_all_buckets (indexfun h) inplace odata ndata end let add h key data = let i = key_index h key in let bucket = Cons{key; data; next=h.data.(i)} in h.data.(i) <- bucket; h.size <- h.size + 1; if h.size > Array.length h.data lsl 1 then resize (fun t -> { f=fun a -> key_index t a }) h let rec remove_bucket: type a. 'b t -> int -> a key -> 'b bucketlist -> 'b bucketlist -> unit = fun h i key prec next -> match next with | Empty -> () | (Cons {key=k; next; _}) as c -> match Key.polyeq key k with | Diff -> remove_bucket h i key c next | Eq -> h.size <- h.size - 1; match prec with | Empty -> h.data.(i) <- next | Cons c -> c.next <- next let remove h key = let i = key_index h key in remove_bucket h i key Empty h.data.(i) let rec find_rec : type a. a key -> 'b bucketlist -> (a, 'b) value = fun key bucketlist -> match bucketlist with | Empty -> raise Not_found | Cons{key=k; data; next} -> match Key.polyeq key k with | Eq -> data | Diff -> find_rec key next let find h key = find_rec key h.data.(key_index h key) let find_opt h key = match find h key with | value -> Some value | exception Not_found -> None let find_all : type a. 'b t -> a key -> (a, 'b) value list = fun h key -> let rec find_in_bucket : 'b bucketlist -> (a, 'b) value list = function | Empty -> [] | Cons{key=k; data=d; next} -> match Key.polyeq k key with | Eq -> d :: find_in_bucket next | Diff -> find_in_bucket next in find_in_bucket h.data.(key_index h key) let rec replace_bucket: type a. a key -> (a, 'b) value -> 'b bucketlist -> bool = fun key data bucketlist -> match bucketlist with | Empty -> true | Cons ({key=k; next; _} as slot) -> match Key.polyeq k key with | Eq -> slot.key <- key; slot.data <- data; false | Diff -> replace_bucket key data next let replace h key data = let i = key_index h key in let l = h.data.(i) in if replace_bucket key data l then begin h.data.(i) <- Cons{key; data; next=l}; h.size <- h.size + 1; if h.size > Array.length h.data lsl 1 then resize (fun t -> { f=fun a -> key_index t a }) h end let mem: type a. 'b t -> a key -> bool = fun h key -> let rec mem_in_bucket = function | Empty -> false | Cons{key=k; next; _} -> match Key.polyeq k key with | Eq -> true | Diff -> mem_in_bucket next in mem_in_bucket h.data.(key_index h key) type 'b key_value = KeyValue: 'a key * ('a, 'b) value -> 'b key_value let add_seq tbl i = Seq.iter (fun (KeyValue(k,v)) -> add tbl k v) i let replace_seq tbl i = Seq.iter (fun (KeyValue(k,v)) -> replace tbl k v) i let of_seq i = let tbl = create 16 in replace_seq tbl i; tbl type 'b polyiter = { f: 'a. 'a key -> ('a, 'b) value -> unit } [@@unboxed] let iter f h = let rec do_bucket = function | Empty -> () | Cons{key; data; next} -> f.f key data; do_bucket next in let old_trav = ongoing_traversal h in if not old_trav then flip_ongoing_traversal h; try let d = h.data in for i = 0 to Array.length d - 1 do do_bucket d.(i) done; if not old_trav then flip_ongoing_traversal h; with exn when not old_trav -> flip_ongoing_traversal h; raise exn type ('b, 'c) polyfiltermap = { f: 'a. 'a key -> ('a, 'b) value -> ('a, 'c) value option } [@@unboxed] let rec filter_map_inplace_bucket f h i prec = function | Empty -> begin match prec with | Empty -> h.data.(i) <- Empty | Cons c -> c.next <- Empty end | (Cons ({key; data; next} as c)) as slot -> begin match f.f key data with | None -> h.size <- h.size - 1; filter_map_inplace_bucket f h i prec next | Some data -> begin match prec with | Empty -> h.data.(i) <- slot | Cons c -> c.next <- slot end; c.data <- data; filter_map_inplace_bucket f h i slot next end let filter_map_inplace f h = let d = h.data in let old_trav = ongoing_traversal h in if not old_trav then flip_ongoing_traversal h; try for i = 0 to Array.length d - 1 do filter_map_inplace_bucket f h i Empty h.data.(i) done; if not old_trav then flip_ongoing_traversal h with exn when not old_trav -> flip_ongoing_traversal h; raise exn type ('b, 'acc) polyfold = { f: 'a. 'a key -> ('a, 'b) value -> 'acc -> 'acc } [@@unboxed] let fold f h init = let rec do_bucket b accu = match b with Empty -> accu | Cons{key; data; next} -> do_bucket next (f.f key data accu) in let old_trav = ongoing_traversal h in if not old_trav then flip_ongoing_traversal h; try let d = h.data in let accu = ref init in for i = 0 to Array.length d - 1 do accu := do_bucket d.(i) !accu done; if not old_trav then flip_ongoing_traversal h; !accu with exn when not old_trav -> flip_ongoing_traversal h; raise exn let length h = h.size let rec bucket_length accu = function | Empty -> accu | Cons{next} -> bucket_length (accu + 1) next let stats h = let mbl = Array.fold_left (fun m b -> Int.max m (bucket_length 0 b)) 0 h.data in let histo = Array.make (mbl + 1) 0 in Array.iter (fun b -> let l = bucket_length 0 b in histo.(l) <- histo.(l) + 1) h.data; { Hashtbl.num_bindings = h.size; num_buckets = Array.length h.data; max_bucket_length = mbl; bucket_histogram = histo } let to_seq tbl = (* capture current array, so that even if the table is resized we keep iterating on the same array *) let tbl_data = tbl.data in (* state: index * next bucket to traverse *) let rec aux i buck () = match buck with | Empty -> if i = Array.length tbl_data then Seq.Nil else aux(i+1) tbl_data.(i) () | Cons {key; data; next} -> Seq.Cons (KeyValue(key, data), aux i next) in aux 0 Empty end module Make (Key: HETEROGENEOUS_HASHED_TYPE) (Value: PatriciaTree.HETEROGENEOUS_VALUE) = MakeSeeded(struct include Key let hash (_seed: int) x = Key.hash x end)(Value)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>