Agda.Utils.AssocList

Lookup keys in the same association list often. Use partially applied to create partial function apply m :: k -> Maybe v.

• First time: O(n log n) in the worst case.

• Subsequently: O(log n).

Specification: apply m == (lookup m).

O(n). Delete a binding. The key must be in the domain of the finite map. Otherwise, an internal error is raised.

O(1). Add a new binding. Assumes the binding is not yet in the list.

O(n). Get the domain (list of keys) of the finite map.

O(n). Named in analogy to Data.Map.mapKeysMonotonic. To preserve the invariant, it is sufficient that the key transformation is injective (rather than monotonic).

O(n). Map over an association list, preserving the order.

O(n). If called with a effect-producing function, violation of the invariant could matter here (duplicating effects).

O(n). Update the value at a key. The key must be in the domain of the finite map. Otherwise, an internal error is raised.

O(n). Update the value at a key with a certain function. The key must be in the domain of the finite map. Otherwise, an internal error is raised.

A finite map, represented as a set of pairs.

Invariant: at most one value per key.

\mathcal{O}(n). lookup key assocs looks up a key in an association list. For the result to be Nothing, the list must be finite.

Examples

>>> lookup 2 []Nothing

>>> lookup 2 [(1, "first")]Nothing

>>> lookup 2 [(1, "first"), (2, "second"), (3, "third")]Just "second"