Data.IdMap

The first parameter prevents identifiers of type Id (a :|: a) which could cause strange runtime behaviour. For example, (left x == right x) should be False in theory, but during runtime (left x) and (right x) are exactly the same identifiers.

Finite maps and sets

type Map i k a = Maplike (M i) k a

Source

Family of finite maps from keys (Id k) to values a. For efficiency reasons, use only with concrete type integers:

 Map I0 k a
 Map I1 k a
 Map I2 k a
 ...

type Set i k = Maplike (S Zero i) k ()

Source

Family of finite sets of keys (Id k). For efficiency reasons, use only with concrete type integers:

 Set I0 k
 Set I1 k
 Set I2 k
 ...

insert :: forall i k a. MaplikeClass i a => Id k -> a -> Maplike i k a -> Maplike i k a

Source

O(1). Insert a new key and value in the map. If the key is already present in the map, the associated value is replaced with the supplied value.

After insertion, the original map may not be used.

delete :: forall i k a. MaplikeClass i a => Id k -> Maplike i k a -> Maplike i k a

Source

O(1). Delete a key and its value from the map. When the key is not a member of the map, the original map is returned.

After deletion, the original map may not be used.

lookUp :: forall i k a. MaplikeClass i a => Id k -> Maplike i k a -> Maybe a

Source

O(1). Look up the value at a key in the map.

member :: MaplikeClass i a => Id k -> Maplike i k a -> Bool

Source

union :: Maplike i k1 a -> Maplike i k2 a -> Maplike i (k1 :|: k2) a

Source

O(0). Union of two maps.

Linearity constraints:

After union, the component maps may also be used.
After insertion into either components, the union map may not be used.
After insertion into the union map, the components may not be used.

Unsafe operations

unsafeInsert :: forall i k a. MaplikeClass i a => Id k -> a -> Maplike i k a -> ()

Source

unsafeEquivalent :: Maplike i k a -> Maplike i k a -> Maplike i k a

Source

Unsafe equality coercion of maps.

The two maps are equal, so every link to the first map could be safely replaced by a link to the second map.

Range of sets and maps

data Sets i k where

Source

Helps to store a range of sets numbered from 0 to i-1. For example, (Sets I3 k) is similar to (Set I2 k, Set I1 k, Set I0 k).

Constructors

PlusSet :: Set i k -> Sets i k -> Sets (Succ i) k

data Maps i k where

Source

Helps to store a range of maps numbered from 1 to i. For example, (Maps1 I3 k) is similar to (forall a . Map I3 k a, forall a . Map I2 k a, forall a . Map I1 k a).

Constructors

PlusMap :: (forall a. Map (Succ i) k a) -> Maps i k -> Maps (Succ i) k

Creation of sets, maps and identifiers

type ICC i k a = Maps i k -> (forall b. Map Zero k b) -> [Id k] -> a

Source

Identifier-consuming computation. i is a type-level integer. A computation of type (ICC i k a) gets i maps numbered from 0 to i-1, an infinite list of different identifiers, and returns a value of type a.

runICC :: I i => (forall k. ICC i k a) -> a

Source

Return the value computed by an identifier-consuming computation. forall k ensures that the identifiers indexed by k are inaccessible to the rest of the program.

type ICCS i k a = Maps i k -> Sets I32 k -> [Id k] -> a

Source

Identifier-consuming computation with sets. i is a type-level integer. A computation of type (ICCS i k a) gets 32 sets numbered from 0 to 31, i maps numbered from 1 to i, an infinite list of different identifiers, and returns a value of type a.

runICCS :: I i => (forall k. ICCS i k a) -> a

Source

Return the value computed by an identifier-consuming computation with sets. forall k ensures that the identifiers indexed by k are inaccessible to the rest of the program.

For internal use

data Maplike i k a

Source

Instances

Functor2 (Maplike i)

Functor (Maplike i k)

class MaplikeClass i x

Source

Instances

I i => MaplikeClass (M i) a

(I i, I j) => MaplikeClass (S j i) ()