package logtk
Install
Dune Dependency
Authors
Maintainers
Sources
md5=97cdb2f90468e9e27c7bbe3b4fb160bb
sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d
doc/logtk.proofs/Logtk_proofs/LLProof/Tbl/index.html
Module LLProof.Tbl
Source
Safe version of Hashtbl.find
.
get_or tbl k ~default
returns the value associated to k
if present, and returns default
otherwise (if k
doesn't belong in tbl
).
add_list tbl x y
adds y
to the list x
is bound to. If x
is not bound, it becomes bound to y
.
incr ?by tbl x
increments or initializes the counter associated with x
. If get tbl x = None
, then after update, get tbl x = Some 1
; otherwise, if get tbl x = Some n
, now get tbl x = Some (n+1)
.
Like incr
but subtract 1 (or the value of by
). If the value reaches 0, the key is removed from the table. This does nothing if the key is not already present in the table.
Iterate on keys (similar order as Hashtbl.iter
).
Iterate on values in the table.
keys_list t
is the list of keys in t
. If the key is in the Hashtable multiple times, all occurrences will be returned.
Map on a hashtable's items, collect into a list.
Iterate on bindings in the table.
Add the corresponding pairs to the table, using Hashtbl.add
.
Add the corresponding pairs to the table, using Hashtbl.add
.
From the given bindings, added in order.
add_iter_count tbl i
increments the count of each element of i
by calling incr
. This is useful for counting how many times each element of i
occurs.
add_seq_count tbl seq
increments the count of each element of seq
by calling incr
. This is useful for counting how many times each element of seq
occurs.
Like add_seq_count
, but allocates a new table and returns it.
Like add_seq_count
, but allocates a new table and returns it.
Build a table from the given list of bindings k_i -> v_i
, added in order using add
. If a key occurs several times, it will be added several times, and the visible binding will be the last one.
update tbl ~f ~k
updates key k
by calling f k (Some v)
if k
was mapped to v
, or f k None
otherwise; if the call returns None
then k
is removed/stays removed, if the call returns Some v'
then the binding k -> v'
is inserted using Hashtbl.replace
.
get_or_add tbl ~k ~f
finds and returns the binding of k
in tbl
, if it exists. If it does not exist, then f k
is called to obtain a new binding v
; k -> v
is added to tbl
and v
is returned.
Printer for tables. Renamed from print
since 2.0.