A finite map is an efficient purely functional data structure
to store a mapping from keys to values.
In order to store the mapping efficiently, an irreflexive(!) order predicate
has to be given, i.e., the order predicate le
should not satisfy
(le x x)
for some key x
.
Example: To store a mapping from Int > String
, the finite map needs
a Boolean predicate like (<)
.
This version was ported from a corresponding Haskell library
Author: Frank Huch, Bernd Brassel
Version: March 2013
emptyFM
:: (a > a > Bool) > FM a b
The empty finite map. 
unitFM
:: (a > a > Bool) > a > b > FM a b
Construct a finite map with only a single element. 
listToFM
:: (a > a > Bool) > [(a,b)] > FM a b
Builts a finite map from given list of tuples (key,element). 
addToFM
:: FM a b > a > b > FM a b
Throws away any previous binding and stores the new one given. 
addListToFM
:: FM a b > [(a,b)] > FM a b
Throws away any previous bindings and stores the new ones given. 
addToFM_C
:: (a > a > a) > FM b a > b > a > FM b a
Instead of throwing away the old binding, addToFM_C combines the new element with the old one. 
addListToFM_C
:: (a > a > a) > FM b a > [(b,a)] > FM b a
Combine with a list of tuples (key,element), cf. 
delFromFM
:: FM a b > a > FM a b
Deletes key from finite map. 
delListFromFM
:: FM a b > [a] > FM a b
Deletes a list of keys from finite map. 
updFM
:: FM a b > a > (b > b) > FM a b
Applies a function to element bound to given key. 
splitFM
:: FM a b > a > Maybe (FM a b,(a,b))
Combines delFrom and lookup. 
plusFM
:: FM a b > FM a b > FM a b
Efficiently add key/element mappings of two maps into a single one. 
plusFM_C
:: (a > a > a) > FM b a > FM b a > FM b a
Efficiently combine key/element mappings of two maps into a single one, cf. 
minusFM
:: FM a b > FM a b > FM a b
(minusFM a1 a2) deletes from a1 any bindings which are bound in a2 
intersectFM
:: FM a b > FM a b > FM a b
Filters only those keys that are bound in both of the given maps. 
intersectFM_C
:: (a > b > c) > FM d a > FM d b > FM d c
Filters only those keys that are bound in both of the given maps and combines the elements as in addToFM_C. 
foldFM
:: (a > b > c > c) > c > FM a b > c
Folds finite map by given function. 
mapFM
:: (a > b > c) > FM a b > FM a c
Applies a given function on every element in the map. 
filterFM
:: (a > b > Bool) > FM a b > FM a b
Yields a new finite map with only those key/element pairs matching the given predicate. 
sizeFM
:: FM a b > Int
How many elements does given map contain? 
eqFM
:: FM a b > FM a b > Bool
Do two given maps contain the same key/element pairs? 
isEmptyFM
:: FM a b > Bool
Is the given finite map empty? 
elemFM
:: a > FM a b > Bool
Does given map contain given key? 
lookupFM
:: FM a b > a > Maybe b
Retrieves element bound to given key 
lookupWithDefaultFM
:: FM a b > b > a > b
Retrieves element bound to given key. 
keyOrder
:: FM a b > a > a > Bool
Retrieves the ordering on which the given finite map is built. 
minFM
:: FM a b > Maybe (a,b)
Retrieves the smallest key/element pair in the finite map according to the basic key ordering. 
maxFM
:: FM a b > Maybe (a,b)
Retrieves the greatest key/element pair in the finite map according to the basic key ordering. 
fmToList
:: FM a b > [(a,b)]
Builds a list of key/element pairs. 
keysFM
:: FM a b > [a]
Retrieves a list of keys contained in finite map. 
eltsFM
:: FM a b > [b]
Retrieves a list of elements contained in finite map. 
fmToListPreOrder
:: FM a b > [(a,b)]
Retrieves list of key/element pairs in preorder of the internal tree. 
fmSortBy
:: (a > a > Bool) > [a] > [a]
Sorts a given list by inserting and retrieving from finite map. 
showFM
:: FM a b > String
Transforms a finite map into a string. 
readFM
:: (a > a > Bool) > String > FM a b
Transforms a string representation of a finite map into a finite map. 
Constructors:
The empty finite map.

Construct a finite map with only a single element.

Builts a finite map from given list of tuples (key,element). For multiple occurences of key, the last corresponding element of the list is taken.

Throws away any previous binding and stores the new one given. 
Throws away any previous bindings and stores the new ones given. The items are added starting with the first one in the list 
Instead of throwing away the old binding, addToFM_C combines the new element with the old one.

Combine with a list of tuples (key,element), cf. addToFM_C 
Deletes key from finite map. Deletion doesn't complain if you try to delete something which isn't there 
Deletes a list of keys from finite map. Deletion doesn't complain if you try to delete something which isn't there 
Efficiently add key/element mappings of two maps into a single one. Bindings in right argument shadow those in the left 
Efficiently combine key/element mappings of two maps into a single one, cf. addToFM_C 
(minusFM a1 a2) deletes from a1 any bindings which are bound in a2 
Filters only those keys that are bound in both of the given maps. The elements will be taken from the second map. 
Filters only those keys that are bound in both of the given maps and combines the elements as in addToFM_C. 
Yields a new finite map with only those key/element pairs matching the given predicate. 
How many elements does given map contain?

Retrieves element bound to given key. If the element is not contained in map, return default value. 
Retrieves the ordering on which the given finite map is built.

Retrieves the smallest key/element pair in the finite map according to the basic key ordering. 
Retrieves the greatest key/element pair in the finite map according to the basic key ordering. 
Builds a list of key/element pairs. The list is ordered by the initially given irreflexive order predicate on keys. 
Retrieves a list of keys contained in finite map. The list is ordered by the initially given irreflexive order predicate on keys. 
Retrieves a list of elements contained in finite map. The list is ordered by the initially given irreflexive order predicate on keys. 
Retrieves list of key/element pairs in preorder of the internal tree. Useful for lists that will be retransformed into a tree or to match any elements regardless of basic order.

Sorts a given list by inserting and retrieving from finite map. Duplicates are deleted. 
Transforms a finite map into a string. For efficiency reasons, the tree structure is shown which is valid for reading only if one uses the same ordering predicate. 