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]
val member [n] [f]: ctx -> key -> hashset [n] [f] -> bool
val not_member [n] [f]: ctx -> key -> hashset [n] [f] -> bool
val from_array [u]: ctx -> [u]key -> ?[n][f].hashset [n] [f]
val from_array_nodup [n]: ctx -> [n]key -> ?[f].hashset [n] [f]
val to_array [n] [f]: hashset [n] [f] -> [n]key
val size [n] [f]: hashset [n] [f] -> i64
val context [n] [f]: hashset [n] [f] -> ctx
val insert [n] [f] [u]: ctx -> hashset [n] [f] -> [u]key -> ?[n'][f'].hashset [n'] [f']
}
module mk_two_level_hashset: (K: hashkey) -> (E: rng_engine with int.t = u64) -> 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: (K: hashkey) -> (E: rng_engine with int.t = u64) -> set with key = K.key with ctx = K.ctx

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]

The hashset type.

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

Check if a key is member of the hashset.

Work: O(1)

Span: O(1)

↑val not_member [n] [f]: ctx -> key -> hashset [n] [f] -> 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].hashset [n] [f]

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].hashset [n] [f]

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]: hashset [n] [f] -> [n]key

Convert hashset to an array of keys.

Work: O(1)

Span: O(1)

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

The number of elements in the hashset.

Work: O(1)

Span: O(1)

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

Gets the context of the hashmap.

Work: O(1)

Span: O(1)

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

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