UniqueInts

struct UniqueInts[k: Type, r: Eff]Source

map: MutMap[k, Int32, r]counter: Counter[r]

The purpose of UniqueInts is to assign unique numbers/identifiers to elements.

Example of use: When generating joins automatically we have data of type (RelSym, Search). These needs to be placed somewhere in memory. For a pair (rel, search) calling createIndex((rel, search)) will return its index if it has been seen before and otherwise return the new index which henceforth will be returned for subsequent queries of (rel, search).

ReverseUniqueInts allows using an index, i, assigned by UniqueInts, and get the value, which UniqueInts assigned index i.

Type for assigning unique integer identifiers to elements, and its functions.

Definitions

def createIndex(val: k, state: UniqueInts[k, r]): Int32 \ r with Order[k]§ Source

Returns the index of val generated by state.

If an index does not exist for val it is created. Otherwise the existing index for val is returned.

def empty(rc: Region[r]): UniqueInts[k, r] \ r§ Source

Returns an empty mapping from k to identifiers.

def get(state: UniqueInts[k, r]): Int32 \ r§ Source

Returns the maximal assigned identifier of state.

def reverse(state: UniqueInts[k, r]): Map[Int32, k] \ r with Order[k]§ Source

Returns an ReverseUniqueInts of state allowing mapping identifiers back to the values they represent.

def toMap(state: UniqueInts[k, r]): Map[k, Int32] \ r§ Source

Returns the current mapping of state as a map.