Abstract

Static hashmaps.

Implementations of the map module type using hash-based data structures.

Synopsis

module type two_level_hashmap = {
type key
type ctx
type map 'ctx [n] [f] [m] 'v
val member [n] [f] [m] 'v: ctx -> key -> map ctx [n] [f] [m] v -> bool
val not_member [n] [f] [m] 'v: ctx -> key -> map ctx [n] [f] [m] v -> bool
val lookup [n] [f] [m] 'v: ctx -> key -> map ctx [n] [f] [m] v -> opt v
val from_array [u] 'v: ctx -> [u](key, v) -> ?[n][f][m].map ctx [n] [f] [m] v
val from_array_rep [u] 'v: ctx -> [u]key -> v -> ?[n][f][m].map ctx [n] [f] [m] v
val from_array_hist [u] 'v: ctx -> (v -> v -> v) -> v -> [u](key, v) -> ?[n][f][m].map ctx [n] [f] [m] v
val from_array_nodup [n] 'v: ctx -> [n](key, v) -> ?[f][m].map ctx [n] [f] [m] v
val from_array_rep_nodup [n] 'v: ctx -> [n]key -> v -> ?[f][m].map ctx [n] [f] [m] v
val adjust [n] [f] [m] [u] 'v: (v -> v -> v) -> v -> map ctx [n] [f] [m] v -> [u](key, v) -> map ctx [n] [f] [m] v
val map [n] [f] [m] 'v 't: (g: (v -> t)) -> map ctx [n] [f] [m] v -> map ctx [n] [f] [m] t
val map_with_key [n] [f] [m] 'v 't: (g: (key -> v -> t)) -> map ctx [n] [f] [m] v -> map ctx [n] [f] [m] t
val to_array [n] [f] [m] 'v: map ctx [n] [f] [m] v -> [n](key, v)
val update [n] [f] [m] [u] 'v: map ctx [n] [f] [m] v -> [u](key, v) -> map ctx [n] [f] [m] v
val size [n] [f] [m] 'v: map ctx [n] [f] [m] v -> i64
val context [n] [f] [m] 'v: map ctx [n] [f] [m] v -> ctx
val insert [n] [f] [m] [u] 'v: ctx -> map ctx [n] [f] [m] v -> [u](key, v) -> ?[n'][f'][m'].map ctx [n'] [f'] [m'] v
val insert_with [n] [f] [m] [u] 'v: ctx -> (v -> v -> v) -> v -> map ctx [n] [f] [m] v -> [u](key, v) -> ?[n'][f'][m'].map ctx [n'] [f'] [m'] v
}
module mk_two_level_hashmap: (I: integral) -> (U: integral) -> (K: hashkey with uint = U.t) -> (E: rng_engine with int.t = U.t) -> two_level_hashmap with key = K.key with ctx = K.ctx
module mk_hashmap_params: (I: integral) -> (U: integral) -> (K: hashkey with uint = U.t) -> (E: rng_engine with int.t = U.t) -> map with key = K.key with ctx = K.ctx
module mk_hashmap: {
type key = K.key
type ctx = K.ctx
type~ map [n] 'v = map [n] v
val member [n] 'v: K.ctx -> K.key -> map [n] v -> bool
val not_member [n] 'v: K.ctx -> K.key -> map [n] v -> bool
val lookup [n] 'v: K.ctx -> K.key -> map [n] v -> #none | #some v
val from_array [u] 'v: K.ctx -> [u](K.key, v) -> ?[n].map [n] v
val from_array_rep [u] 'v: K.ctx -> [u]K.key -> v -> ?[n].map [n] v
val from_array_hist [u] 'v: K.ctx -> v -> v -> v -> v -> [u](K.key, v) -> ?[n].map [n] v
val from_array_nodup [u] 'v: K.ctx -> [u](K.key, v) -> ?[n].map [n] v
val from_array_rep_nodup [u] 'v: K.ctx -> [u]K.key -> v -> ?[n].map [n] v
val adjust [n] [u] 'v: v -> v -> v -> v -> map [n] v -> [u](K.key, v) -> map [n] v
val map [n] 'a 'b: (g: a -> b) -> map [n] a -> map [n] b
val map_with_key [n] 'a 'b: (g: K.key -> a -> b) -> map [n] a -> map [n] b
val to_array [n] 'v: map [n] v -> ?[d₀].[d₀](K.key, v)
val update [n] [u] 'v: map [n] v -> [u](K.key, v) -> map [n] v
val size [n] 'v: map [n] v -> i64
val context [n] 'v: map [n] v -> K.ctx
val insert [n] [u] 'v: K.ctx -> map [n] v -> [u](K.key, v) -> ?[m].map [m] v
val insert_with [n] [u] 'v: K.ctx -> v -> v -> v -> v -> map [n] v -> [u](K.key, v) -> ?[m].map [m] v
}
module mk_hashmap_u32: {
type key = K.key
type ctx = K.ctx
type~ map [n] 'v = map [n] v
val member [n] 'v: K.ctx -> K.key -> map [n] v -> bool
val not_member [n] 'v: K.ctx -> K.key -> map [n] v -> bool
val lookup [n] 'v: K.ctx -> K.key -> map [n] v -> #none | #some v
val from_array [u] 'v: K.ctx -> [u](K.key, v) -> ?[n].map [n] v
val from_array_rep [u] 'v: K.ctx -> [u]K.key -> v -> ?[n].map [n] v
val from_array_hist [u] 'v: K.ctx -> v -> v -> v -> v -> [u](K.key, v) -> ?[n].map [n] v
val from_array_nodup [u] 'v: K.ctx -> [u](K.key, v) -> ?[n].map [n] v
val from_array_rep_nodup [u] 'v: K.ctx -> [u]K.key -> v -> ?[n].map [n] v
val adjust [n] [u] 'v: v -> v -> v -> v -> map [n] v -> [u](K.key, v) -> map [n] v
val map [n] 'a 'b: (g: a -> b) -> map [n] a -> map [n] b
val map_with_key [n] 'a 'b: (g: K.key -> a -> b) -> map [n] a -> map [n] b
val to_array [n] 'v: map [n] v -> ?[d₀].[d₀](K.key, v)
val update [n] [u] 'v: map [n] v -> [u](K.key, v) -> map [n] v
val size [n] 'v: map [n] v -> i64
val context [n] 'v: map [n] v -> K.ctx
val insert [n] [u] 'v: K.ctx -> map [n] v -> [u](K.key, v) -> ?[m].map [m] v
val insert_with [n] [u] 'v: K.ctx -> v -> v -> v -> v -> map [n] v -> [u](K.key, v) -> ?[m].map [m] v
}
module type open_addressing_hashmap = {
type key
type ctx
type map 'ctx [n] [f] 'v
val member [n] [f] 'v: ctx -> key -> map ctx [n] [f] v -> bool
val not_member [n] [f] 'v: ctx -> key -> map ctx [n] [f] v -> bool
val lookup [n] [f] 'v: ctx -> key -> map ctx [n] [f] v -> opt v
val from_array [u] 'v: ctx -> [u](key, v) -> ?[n][f].map ctx [n] [f] v
val from_array_rep [u] 'v: ctx -> [u]key -> v -> ?[n][f].map ctx [n] [f] v
val from_array_hist [u] 'v: ctx -> (v -> v -> v) -> v -> [u](key, v) -> ?[n][f].map ctx [n] [f] v
val from_array_nodup [n] 'v: ctx -> [n](key, v) -> ?[f].map ctx [n] [f] v
val from_array_rep_nodup [n] 'v: ctx -> [n]key -> v -> ?[f].map ctx [n] [f] v
val adjust [n] [f] [u] 'v: (v -> v -> v) -> v -> map ctx [n] [f] v -> [u](key, v) -> map ctx [n] [f] v
val map [n] [f] 'v 't: (g: (v -> t)) -> map ctx [n] [f] v -> map ctx [n] [f] t
val map_with_key [n] [f] 'v 't: (g: (key -> v -> t)) -> map ctx [n] [f] v -> map ctx [n] [f] t
val to_array [n] [f] 'v: map ctx [n] [f] v -> [n](key, v)
val update [n] [f] [u] 'v: map ctx [n] [f] v -> [u](key, v) -> map ctx [n] [f] v
val size [n] [f] 'v: map ctx [n] [f] v -> i64
val context [n] [f] 'v: map ctx [n] [f] v -> ctx
val insert [n] [f] [u] 'v: ctx -> map ctx [n] [f] v -> [u](key, v) -> ?[n'][f'].map ctx [n'] [f'] v
val insert_with [n] [f] [u] 'v: ctx -> (v -> v -> v) -> v -> map ctx [n] [f] v -> [u](key, v) -> ?[n'][f'].map ctx [n'] [f'] v
}
module mk_open_addressing_hashmap: (K: hashkey with uint = u64) -> (E: rng_engine with int.t = u64) -> (P: {
val hashmap_size: i64 -> i64
val probe: u64 -> u64
}) -> open_addressing_hashmap with key = K.key with ctx = K.ctx
module mk_linear_hashmap: (K: hashkey with uint = u64) -> (E: rng_engine with int.t = u64) -> map with key = K.key with ctx = K.ctx

Description

↑module type two_level_hashmap
↑type key

The key type.

↑type ctx

The context type.

↑type map 'ctx [n] [f] [m] 'v

The hashmap definition.

↑val member [n] [f] [m] 'v: ctx -> key -> map ctx [n] [f] [m] v -> bool

Check if a key is member of the hashmap.

Work: O(1)

Span: O(1)

↑val not_member [n] [f] [m] 'v: ctx -> key -> map ctx [n] [f] [m] v -> bool

Check if a key is not member of the hashmap

Work: O(1)

Span: O(1)

↑val lookup [n] [f] [m] 'v: ctx -> key -> map ctx [n] [f] [m] v -> opt v

Look up a value.

Work: O(1)

Span: O(1)

↑val from_array [u] 'v: ctx -> [u](key, v) -> ?[n][f][m].map ctx [n] [f] [m] v

Given a key-value array construct a hashmap.

Expected Work: O(n + u)

Expected Span: O(log n)

↑val from_array_rep [u] 'v: ctx -> [u]key -> v -> ?[n][f][m].map ctx [n] [f] [m] v

Create hashmap with default value.

Expected Work: O(n)

Expected Span: O(log n)

↑val from_array_hist [u] 'v: ctx -> (v -> v -> v) -> v -> [u](key, v) -> ?[n][f][m].map ctx [n] [f] [m] v

Create hashmap where duplicates are reduced with an commutative and associative operation.

Expected Work: O(n + u ✕ W(op))

Expected Span: O(log n) (Assuming best case for hist)

↑val from_array_nodup [n] 'v: ctx -> [n](key, v) -> ?[f][m].map ctx [n] [f] [m] v

Given a key-value array construct a hashmap. If any keys are duplicates then the function call will never finish. It does less work than the safe variant.

Expected Work: O(n + u)

Expected Span: O(log n)

↑val from_array_rep_nodup [n] 'v: ctx -> [n]key -> v -> ?[f][m].map ctx [n] [f] [m] v

Create hashmap with default value. If any keys are duplicates then the function call will never finish. It does less work than the safe variant.

Expected Work: O(n)

Expected Span: O(log n)

↑val adjust [n] [f] [m] [u] 'v: (v -> v -> v) -> v -> map ctx [n] [f] [m] v -> [u](key, v) -> map ctx [n] [f] [m] v

Combine key-value pairs into a map using the provided associative and commutative operation. Keys that are not present in the map is not added.

Work: O(n + u ✕ W(op))

Span: O(u) in the worst case but O(1) in the best case.

↑val map [n] [f] [m] 'v 't: (g: (v -> t)) -> map ctx [n] [f] [m] v -> map ctx [n] [f] [m] t

Map a function over the hashmap values.

Work: O(n ✕ W(g))

Span: O(S(g))

↑val map_with_key [n] [f] [m] 'v 't: (g: (key -> v -> t)) -> map ctx [n] [f] [m] v -> map ctx [n] [f] [m] t

Map a function over the hashmap values.

Work: O(n ✕ W(g))

Span: O(S(g))

↑val to_array [n] [f] [m] 'v: map ctx [n] [f] [m] v -> [n](key, v)

Convert hashmap to an array of key-value pairs.

Work: O(n)

Span: O(1)

↑val update [n] [f] [m] [u] 'v: map ctx [n] [f] [m] v -> [u](key, v) -> map ctx [n] [f] [m] v

Updates the value of the hash map using the key with the smallest index. No new keys are added.

Work: O(n + u)

Span: O(u) in the worst case but O(1) in the best case.

↑val size [n] [f] [m] 'v: map ctx [n] [f] [m] v -> i64

The number of elements in the hashmap.

Work: O(1)

Span: O(1)

↑val context [n] [f] [m] 'v: map ctx [n] [f] [m] v -> ctx

Gets the context of the hashmap.

Work: O(1)

Span: O(1)

↑val insert [n] [f] [m] [u] 'v: ctx -> map ctx [n] [f] [m] v -> [u](key, v) -> ?[n'][f'][m'].map ctx [n'] [f'] [m'] v

Insert new key-value pairs into a hashmap. If a key already exists in the hashmap, the new value will overwrite the old one.

Expected Work: O(n + u)

Expected Span: O(log (n + u))

↑val insert_with [n] [f] [m] [u] 'v: ctx -> (v -> v -> v) -> v -> map ctx [n] [f] [m] v -> [u](key, v) -> ?[n'][f'][m'].map ctx [n'] [f'] [m'] v

Insert new key-value pairs into a hashmap, combining values of duplicate keys using the provided associative and commutative operation.

Expected Work: O(n' + (n + u) ✕ W(op))

Expected Span: O(log (n + u)) (Assuming best case for hist)

↑module mk_two_level_hashmap

This is an implementation of a static hash table using two level hashing. The modules time complexities assumes only unique keys but the modules does work with duplicate keys.

↑module mk_hashmap_params

Create an implementation of map using two level hash tables.

↑module mk_hashmap
↑module mk_hashmap_u32
↑module type open_addressing_hashmap
↑type key
↑type ctx
↑type map 'ctx [n] [f] 'v
↑val member [n] [f] 'v: ctx -> key -> map ctx [n] [f] v -> bool
↑val not_member [n] [f] 'v: ctx -> key -> map ctx [n] [f] v -> bool
↑val lookup [n] [f] 'v: ctx -> key -> map ctx [n] [f] v -> opt v
↑val from_array [u] 'v: ctx -> [u](key, v) -> ?[n][f].map ctx [n] [f] v
↑val from_array_rep [u] 'v: ctx -> [u]key -> v -> ?[n][f].map ctx [n] [f] v
↑val from_array_hist [u] 'v: ctx -> (v -> v -> v) -> v -> [u](key, v) -> ?[n][f].map ctx [n] [f] v
↑val from_array_nodup [n] 'v: ctx -> [n](key, v) -> ?[f].map ctx [n] [f] v
↑val from_array_rep_nodup [n] 'v: ctx -> [n]key -> v -> ?[f].map ctx [n] [f] v
↑val adjust [n] [f] [u] 'v: (v -> v -> v) -> v -> map ctx [n] [f] v -> [u](key, v) -> map ctx [n] [f] v
↑val map [n] [f] 'v 't: (g: (v -> t)) -> map ctx [n] [f] v -> map ctx [n] [f] t
↑val map_with_key [n] [f] 'v 't: (g: (key -> v -> t)) -> map ctx [n] [f] v -> map ctx [n] [f] t
↑val to_array [n] [f] 'v: map ctx [n] [f] v -> [n](key, v)
↑val update [n] [f] [u] 'v: map ctx [n] [f] v -> [u](key, v) -> map ctx [n] [f] v
↑val size [n] [f] 'v: map ctx [n] [f] v -> i64
↑val context [n] [f] 'v: map ctx [n] [f] v -> ctx
↑val insert [n] [f] [u] 'v: ctx -> map ctx [n] [f] v -> [u](key, v) -> ?[n'][f'].map ctx [n'] [f'] v
↑val insert_with [n] [f] [u] 'v: ctx -> (v -> v -> v) -> v -> map ctx [n] [f] v -> [u](key, v) -> ?[n'][f'].map ctx [n'] [f'] v
↑module mk_open_addressing_hashmap
↑module mk_linear_hashmap