Fixpoint3.UniqueInts

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.