1
(**************************************************************************)
5
(* Fran�ois Pottier and Yann R�gis-Gianas, INRIA Rocquencourt *)
7
(* Copyright 2005 Institut National de Recherche en Informatique et *)
8
(* en Automatique. All rights reserved. This file is distributed *)
9
(* under the terms of the Q Public License version 1.0, with the *)
10
(* change described in file LICENSE. *)
12
(**************************************************************************)
16
(* Keys are assumed to have a natural total order. *)
20
(* The type of maps whose data have type ['a]. *)
28
(* [lookup k m] looks up the value associated to the key [k] in the
29
map [m], and raises [Not_found] if no value is bound to [k]. *)
31
val lookup: key -> 'a t -> 'a
33
(* [add k d m] returns a map whose bindings are all bindings in [m],
34
plus a binding of the key [k] to the datum [d]. If a binding
35
already exists for [k], it is overridden. *)
37
val add: key -> 'a -> 'a t -> 'a t
39
(* [strict_add k d m] returns a set whose elements are all elements
40
of [s], plus [x]. returns a map whose bindings are all bindings
41
in [m], plus a binding of the key [k] to the datum [d]. If a
42
binding already exists for [k] then [Unchanged] is raised. *)
46
val strict_add: key -> 'a -> 'a t -> 'a t
48
(* [fine_add decide k d m] returns a map whose bindings are all
49
bindings in [m], plus a binding of the key [k] to the datum
50
[d]. If a binding from [k] to [d0] already exists, then the
51
resulting map contains a binding from [k] to [decide d0 d]. *)
53
type 'a decision = 'a -> 'a -> 'a
55
val fine_add: 'a decision -> key -> 'a -> 'a t -> 'a t
57
(* [singleton k d] returns a map whose only binding is from [k] to [d]. *)
59
val singleton: key -> 'a -> 'a t
61
(* [is_empty m] returns [true] if and only if the map [m] defines no
64
val is_empty: 'a t -> bool
66
(* [is_singleton s] returns [Some x] if [s] is a singleton
67
containing [x] as its only element; otherwise, it returns
70
val is_singleton: 'a t -> (key * 'a) option
72
(* [cardinal m] returns [m]'s cardinal, that is, the number of keys
73
it binds, or, in other words, the cardinal of its domain. *)
75
val cardinal: 'a t -> int
77
(* [lookup_and_remove k m] looks up the value [v] associated to the
78
key [k] in the map [m], and raises [Not_found] if no value is
79
bound to [k]. The call returns the value [v], together with the
80
map [m] deprived from the binding from [k] to [v]. *)
82
val lookup_and_remove: key -> 'a t -> 'a * 'a t
84
(* [remove k m] is the map [m] deprived from any binding for [k]. *)
86
val remove: key -> 'a t -> 'a t
88
(* [union m1 m2] returns the union of the maps [m1] and
89
[m2]. Bindings in [m2] take precedence over those in [m1]. *)
91
val union: 'a t -> 'a t -> 'a t
93
(* [fine_union decide m1 m2] returns the union of the maps [m1] and
94
[m2]. If a key [k] is bound to [x1] (resp. [x2]) within [m1]
95
(resp. [m2]), then [decide] is called. It is passed [x1] and
96
[x2], and must return the value that shall be bound to [k] in the
99
val fine_union: 'a decision -> 'a t -> 'a t -> 'a t
101
(* [iter f m] invokes [f k x], in turn, for each binding from key
102
[k] to element [x] in the map [m]. Keys are presented to [f] in
105
val iter: (key -> 'a -> unit) -> 'a t -> unit
107
(* [fold f m seed] invokes [f k d accu], in turn, for each binding
108
from key [k] to datum [d] in the map [m]. Keys are presented to
109
[f] in increasing order. The initial value of [accu] is [seed];
110
then, at each new call, its value is the value returned by the
111
previous invocation of [f]. The value returned by [fold] is the
112
final value of [accu]. *)
114
val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
116
(* [fold_rev] performs exactly the same job as [fold], but presents
117
keys to [f] in the opposite order. *)
119
val fold_rev: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
121
(* It is valid to evaluate [iter2 f m1 m2] if and only if [m1] and
122
[m2] have equal domains. Doing so invokes [f k x1 x2], in turn,
123
for each key [k] bound to [x1] in [m1] and to [x2] in
124
[m2]. Bindings are presented to [f] in increasing order. *)
126
val iter2: (key -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit
128
(* [map f m] returns the map obtained by composing the map [m] with
129
the function [f]; that is, the map $k\mapsto f(m(k))$. *)
131
val map: ('a -> 'b) -> 'a t -> 'b t
133
(* [endo_map] is similar to [map], but attempts to physically share
134
its result with its input. This saves memory when [f] is the
135
identity function. *)
137
val endo_map: ('a -> 'a) -> 'a t -> 'a t
139
(* A map's domain is a set. Thus, to be able to perform operations
140
on domains, we need set operations, provided by the [Domain]
141
sub-module. The two-way connection between maps and their domains
142
is given by two additional functions, [domain] and
143
[lift]. [domain m] returns [m]'s domain. [lift f s] returns the
144
map $k\mapsto f(k)$, where $k$ ranges over a set of keys [s]. *)
146
module Domain : GSet.S with type element = key
148
val domain: 'a t -> Domain.t
149
val lift: (key -> 'a) -> Domain.t -> 'a t
151
(* [corestrict m d] performs a co-restriction of the map [m] to the
152
domain [d]. That is, it returns the map $k\mapsto m(k)$, where
153
$k$ ranges over all keys bound in [m] but \emph{not} present in
156
val corestrict: 'a t -> Domain.t -> 'a t