Library

Module

Module type

Parameter

Class

Class type

The GADT of certificate request extensions, as defined in PKCS 9 (RFC 2985).

`include Gmap.S with type 'a key = 'a k`

`type 'a key = 'a k`

The type for map keys whose lookup value is `'a`

.

### Constructors

`val empty : t`

`empty`

is the empty map.

`singleton key value`

creates a one-element map that contains a binding `value`

for `key`

.

### Basic operations

`val is_empty : t -> bool`

`is_empty m`

returns `true`

if the map `m`

is empty, `false`

otherwise.

`val cardinal : t -> int`

`cardinal m`

returns the number of bindings of the map `m`

.

### Lookup operations

`find key m`

returns `Some v`

if the binding of `key`

in `m`

is `v`

, or `None`

if `key`

is not bound `m`

.

### Insertion and removal operations

`add_unless_bound key value m`

returns `Some m'`

, a map containing the same bindings as `m`

, plus a binding of `key`

to `value`

. Or, `None`

if `key`

was already bound in `m`

.

`add key value m`

returns a map containing the same bindings as `m`

, plus a binding of `key`

to `value`

. If `key`

was already bound in `m`

, the previous binding disappears.

`remove key m`

returns a map containing the same bindings as `m`

, except for `key`

which is not bound in the returned map. If `key`

was not bound in `m`

, `m`

is returned unchanged.

`update k f m`

returns a map containing the same bindings as `m`

, except for the binding `v`

of `k`

. Depending the value of `v`

, which is `f (find k m)`

, the binding of `k`

is added, removed, or updated.

### Bindings

### Selection of bindings

`bindings m`

returns the list of all bindings in the given map `m`

. The list is sorted with respect to the ordering over the type of the keys.

### Higher-order functions

The function type for the equal operation, using a record type for "first-class" semi-explicit polymorphism.

`equal p m m'`

tests whether the maps `m`

and `m'`

are equal, that is contain equal keys and associate them with equal data. `p`

is the equality predicate used to compare the data associated with the keys.

The function type for the map operation, using a record type for "first-class" semi-explicit polymorphism.

`map f m`

returns a map with the same domain as `m`

, where the associated binding `b`

has been replaced by the result of the application of `f`

to `b`

. The bindings are passed to `f`

in increasing order with respect to the ordering over the type of the keys.

`iter f m`

applies `f`

to all bindings in `m`

. The bindings are passed in increasing order with respect to the ordering over the type of keys.

`fold f m acc`

computes `(f bN .. (f b1 acc))`

, where `b1 .. bN`

are the bindings of `m`

in increasing order with respect to the ordering over the type of the keys.

`for_all p m`

checks if all bindings of the map `m`

satisfy the predicate `p`

.

`exists p m`

checks if at least one binding of the map `m`

satisfies `p`

.

`filter p m`

returns the map with all the bindings in `m`

that satisfy `p`

.

The function type for the merge operation, using a record type for "first-class" semi-explicit polymorphism.

`merge f m m'`

computes a map whose keys is a subset of keys of `m`

and `m'`

. The presence of each such binding, and the corresponding value, is determined with the function `f`

.

The function type for the union operation, using a record type for "first-class" semi-explicit polymorphism.