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
(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2026 formalsec *)
(* Written by the Smtml programmers *)
module type S = sig
type key
type !'a t
val create : int -> 'a t
val capacity : 'a t -> int
val clear : 'a t -> unit
val length : 'a t -> int
val add : 'a t -> key -> 'a -> unit
val replace : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find_opt : 'a t -> key -> 'a option
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
val copy : 'a t -> 'a t
val to_seq : 'a t -> (key * 'a) Seq.t
val to_seq_keys : 'a t -> key Seq.t
val to_seq_values : 'a t -> 'a Seq.t
val add_seq : 'a t -> (key * 'a) Seq.t -> unit
val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
val stats : 'a t -> Hashtbl.statistics
end
module Make (H : Hashtbl.HashedType) : S with type key = H.t = struct
type key = H.t
module Tbl = Hashtbl.Make (H)
type 'a node =
{ key : key
; mutable value : 'a
; mutable prev : 'a node option
; mutable next : 'a node option
}
type !'a t =
{ tbl : 'a node Tbl.t
; mutable head : 'a node option (* most recently used *)
; mutable tail : 'a node option (* least recently used *)
; capacity : int
; mutable size : int
}
let create capacity =
{ tbl = Tbl.create (max 16 (min capacity 65536))
; head = None
; tail = None
; capacity
; size = 0
}
let capacity t = t.capacity
let length t = t.size
let unlink t n =
(match n.prev with Some p -> p.next <- n.next | None -> t.head <- n.next);
(match n.next with Some q -> q.prev <- n.prev | None -> t.tail <- n.prev);
n.prev <- None;
n.next <- None
let insert_front t n =
n.prev <- None;
n.next <- t.head;
(match t.head with Some h -> h.prev <- Some n | None -> ());
t.head <- Some n;
if Option.is_none t.tail then t.tail <- Some n
let touch t n =
match t.head with
| Some h when phys_equal h n -> ()
| _ ->
unlink t n;
insert_front t n
let remove_node t n =
unlink t n;
Tbl.remove t.tbl n.key;
t.size <- t.size - 1
let evict t = match t.tail with None -> () | Some n -> remove_node t n
let add t k v =
match Tbl.find_opt t.tbl k with
| Some n ->
n.value <- v;
touch t n
| None ->
let n = { key = k; value = v; prev = None; next = None } in
Tbl.add t.tbl k n;
insert_front t n;
t.size <- t.size + 1;
if t.capacity > 0 && t.size > t.capacity then evict t
let replace = add
let find_opt t k =
match Tbl.find_opt t.tbl k with
| None -> None
| Some n ->
touch t n;
Some n.value
let mem t k = Tbl.mem t.tbl k
let remove t k =
match Tbl.find_opt t.tbl k with None -> () | Some n -> remove_node t n
let clear t =
Tbl.reset t.tbl;
t.head <- None;
t.tail <- None;
t.size <- 0
let stats t = Tbl.stats t.tbl
let iter f t =
let rec loop = function
| None -> ()
| Some n ->
f n.key n.value;
loop n.next
in
loop t.head
let fold f t acc =
let rec loop acc = function
| None -> acc
| Some n -> loop (f n.key n.value acc) n.next
in
loop acc t.head
let filter_map_inplace f t =
let rec loop = function
| None -> ()
| Some n ->
let next = n.next in
( match f n.key n.value with
| Some v -> n.value <- v
| None -> remove_node t n );
loop next
in
loop t.head
let copy t =
let t' = create t.capacity in
(* [acc] ends up ordered tail-to-head, so adding it in order leaves the
most recently used binding at the front. *)
let rec collect acc = function
| None -> acc
| Some n -> collect ((n.key, n.value) :: acc) n.next
in
List.iter (fun (k, v) -> add t' k v) (collect [] t.head);
t'
let to_seq t =
let rec loop = function
| None -> Seq.Nil
| Some n -> Seq.Cons ((n.key, n.value), fun () -> loop n.next)
in
fun () -> loop t.head
let to_seq_keys t =
let rec loop = function
| None -> Seq.Nil
| Some n -> Seq.Cons (n.key, fun () -> loop n.next)
in
fun () -> loop t.head
let to_seq_values t =
let rec loop = function
| None -> Seq.Nil
| Some n -> Seq.Cons (n.value, fun () -> loop n.next)
in
fun () -> loop t.head
let add_seq t seq = Seq.iter (fun (k, v) -> add t k v) seq
let replace_seq t seq = Seq.iter (fun (k, v) -> replace t k v) seq
end