Abstract

Static hashsets with an unlifted type.

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.

Synopsis

module type two_level_hashset = {
type key
type ctx
type hashset [n] [f] [m]
val member [n] [f] [m]: ctx -> key -> hashset [n] [f] [m] -> bool
val not_member [n] [f] [m]: ctx -> key -> hashset [n] [f] [m] -> bool
val from_array [u]: ctx -> [u]key -> ?[n][f][m].hashset [n] [f] [m]
val from_array_nodup [n]: ctx -> [n]key -> ?[f][m].hashset [n] [f] [m]
val to_array [n] [f] [m]: hashset [n] [f] [m] -> [n]key
val size [n] [f] [m]: hashset [n] [f] [m] -> i64
val context [n] [f] [m]: hashset [n] [f] [m] -> ctx
val insert [n] [f] [m] [u]: ctx -> hashset [n] [f] [m] -> [u]key -> ?[n'][f'][m'].hashset [n'] [f'] [m']
}
module mk_two_level_hashset: (I: integral) -> (U: integral) -> (K: hashkey with uint = U.t) -> (E: rng_engine with int.t = U.t) -> two_level_hashset with key = K.key with ctx = K.ctx
module type hashset = {
type key
type ctx
type~ hashset
val member: ctx -> key -> hashset -> bool
val not_member: ctx -> key -> hashset -> bool
val from_array [n]: ctx -> [n]key -> hashset
val from_array_nodup [n]: ctx -> [n]key -> hashset
val to_array: hashset -> []key
val size: hashset -> i64
val context: hashset -> ctx
val insert [u]: ctx -> hashset -> [u]key -> hashset
}
module mk_hashset_params: (I: integral) -> (U: integral) -> (K: hashkey with uint = U.t) -> (E: rng_engine with int.t = U.t) -> set with key = K.key with ctx = K.ctx
module mk_hashset: {
type key = K.key
type ctx = K.ctx
type~ set [n] = set [n]
val member [n]: K.ctx -> K.key -> set [n] -> bool
val not_member [n]: K.ctx -> K.key -> set [n] -> bool
val from_array [u]: K.ctx -> [u]K.key -> ?[n].set [n]
val from_array_nodup [u]: K.ctx -> [u]K.key -> ?[n].set [n]
val to_array [n]: set [n] -> [n]K.key
val size [n]: set [n] -> i64
val context [n]: set [n] -> K.ctx
val insert [n] [u]: K.ctx -> set [n] -> [u]K.key -> ?[n'].set [n']
}
module mk_hashset_u32: {
type key = K.key
type ctx = K.ctx
type~ set [n] = set [n]
val member [n]: K.ctx -> K.key -> set [n] -> bool
val not_member [n]: K.ctx -> K.key -> set [n] -> bool
val from_array [u]: K.ctx -> [u]K.key -> ?[n].set [n]
val from_array_nodup [u]: K.ctx -> [u]K.key -> ?[n].set [n]
val to_array [n]: set [n] -> [n]K.key
val size [n]: set [n] -> i64
val context [n]: set [n] -> K.ctx
val insert [n] [u]: K.ctx -> set [n] -> [u]K.key -> ?[n'].set [n']
}

Description

↑module type two_level_hashset

An implementation of sets built on two level hashsets.

↑type key

The key type.

↑type ctx

The context type.

↑type hashset [n] [f] [m]

The hashset type.

↑val member [n] [f] [m]: ctx -> key -> hashset [n] [f] [m] -> bool

Check if a key is member of the hashset.

Work: O(1)

Span: O(1)

↑val not_member [n] [f] [m]: ctx -> key -> hashset [n] [f] [m] -> bool

Check if a key is not member of the hashset

Work: O(1)

Span: O(1)

↑val from_array [u]: ctx -> [u]key -> ?[n][f][m].hashset [n] [f] [m]

Given an array keys construct a hashset.

Expected Work: O(n)

Expected Span: O(log n)

↑val from_array_nodup [n]: ctx -> [n]key -> ?[f][m].hashset [n] [f] [m]

Given an array keys construct a hashset. If the given keys contains duplicates then the function call will never finish. Inturn it does less work.

Expected Work: O(n)

Expected Span: O(log n)

↑val to_array [n] [f] [m]: hashset [n] [f] [m] -> [n]key

Convert hashset to an array of keys.

Work: O(1)

Span: O(1)

↑val size [n] [f] [m]: hashset [n] [f] [m] -> i64

The number of elements in the hashset.

Work: O(1)

Span: O(1)

↑val context [n] [f] [m]: hashset [n] [f] [m] -> ctx

Gets the context of the hashmap.

Work: O(1)

Span: O(1)

↑val insert [n] [f] [m] [u]: ctx -> hashset [n] [f] [m] -> [u]key -> ?[n'][f'][m'].hashset [n'] [f'] [m']

Insert new keys into a hashset. If a key already exists in the hashset, the new value will overwrite the old one.

Expected Work: O(n + u)

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

↑module mk_two_level_hashset

Build a set that internally uses mk_two_level_hashmap@term.

↑module type hashset
↑type key
↑type ctx
↑type~ hashset
↑val member: ctx -> key -> hashset -> bool
↑val not_member: ctx -> key -> hashset -> bool
↑val from_array [n]: ctx -> [n]key -> hashset
↑val from_array_nodup [n]: ctx -> [n]key -> hashset
↑val to_array: hashset -> []key
↑val size: hashset -> i64
↑val context: hashset -> ctx
↑val insert [u]: ctx -> hashset -> [u]key -> hashset
↑module mk_hashset_params
↑module mk_hashset
↑module mk_hashset_u32