Library
Module
Module type
Parameter
Class
Class type
Borrow(R)(H)
is a BORROW
indexed by H
and govern by the replacement policy R
.
A BORROW
is similar to a TRANSFER
except that:
It is always unsafe to clean-up resources obtained from a BORROW
.
See Rache
(or Functors
) for more information.
module R : REPLACEMENT
create destroy n
creates a cache with a size-bound of n
. Remember that the size-bound is not upheld strictly by all caches.
borrow_or_make c k mk f
If k
is bound to r
in c
then it calls f r
.
Otherwise, it generates r
using mk
, then inserts the binding k
-to-r
in c
, then calls f r
.
Note that inserting the binding in c
may cause another binding to be removed and its associated resource to be cleaned-up.
It is unsafe to make use of c
during the evaluation of f
.
It is unsafe to clean-up r
.
Note that the in caches with a non-FIFO
replacement policy, this may have a side effect on the k
-to-r
binding. Specifically, in those caches, it might make it less likely to be removed when supernumerary bindings are inserted.
borrow c k f
calls f
with r
if k
is bound to r
in c
. This does not remove the resource from the cache: the cache is still responsible for cleaning-up the resource.
It is unsafe to use the cache from within the function f
.
It is unsafe to clean-up r
.
Note that the in caches with a non-FIFO
replacement policy, this may have a side effect on the k
-to-v
binding. Specifically, in those caches, it might make it less likely to be removed when supernumerary bindings are inserted.
fold f c init
folds the function f
and value init
over the bindings of c
from newest to oldest.
At each called to f
, the resource of the traversed binding is borrowed by f
. Consequently, the same limitations apply for fold
as for borrow
.
It is unsafe to clean-up any of the borrowed resources.
It is unsafe to use the cache from within f
.
fold_oldest_first
is like fold
but in reversed order: the elements that would be the first to be removed are traversed first. In a FIFO
cache, it is oldest-first traversal.
The same limitations and warning applies as for fold
.
The removal functions (remove
, clear
, and filter
) remove the specified elements from the cache. In all cases, the resources are cleaned-up by the cache.
remove c k
removes and cleans-up the binding from k
in c
. If k
is not bound in c
, it does nothing.
val clear : 'resource t -> unit
clear c
removes and cleans-up all bindings from c
.
filter c f
removes and cleans-up all the bindings (k, v)
such that f k v = false
.
val length : 'resource t -> int
length c
is the number of bindings held by c
.
val capacity : 'resource t -> int
capacity c
is the number of bindings c
can hold: capacity (create n) = n