src/util/extmap.mli

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                           Objective Caml                            *)
   4 (*                                                                     *)
   5 (*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
   6 (*                                                                     *)
   7 (*  Copyright 1996 Institut National de Recherche en Informatique et   *)
   8 (*  en Automatique.  All rights reserved.  This file is distributed    *)
   9 (*  under the terms of the GNU Library General Public License, with    *)
  10 (*  the special exception on linking described in file ../LICENSE.     *)
  11 (*                                                                     *)
  12 (***********************************************************************)
  13
  14 (* This file originates from the OCaml v 3.12 Standard Library.
  15    It was extended and modified for the needs of the Why3 project.
  16    It is distributed under the terms of its initial license, which
  17    is provided in the file OCAML-LICENSE. *)
  18
  19 (** {1 Association tables over ordered types}
  20
  21    This module implements applicative association tables, also known as
  22    finite maps or dictionaries, given a total ordering function
  23    over the keys.
  24    All operations over maps are purely applicative (no side-effects).
  25    The implementation uses balanced binary trees, and therefore searching
  26    and insertion take time logarithmic in the size of the map.
  27 *)
  28
  29 (** Input signature of the functor {!Extmap.Make}. *)
  30 module type OrderedType = Map.OrderedType
  31
  32 (** Output signature of the functor {!Extmap.Make}. *)
  33 module type S =
  34   sig
  35     type key
  36     (** The type of the map keys. *)
  37
  38     type (+'a) t
  39     (** The type of maps from type [key] to type ['a]. *)
  40
  41     val empty: 'a t
  42     (** The empty map. *)
  43
  44     val is_empty: 'a t -> bool
  45     (** Test whether a map is empty or not. *)
  46
  47     val mem: key -> 'a t -> bool
  48     (** [mem x m] returns [true] if [m] contains a binding for [x],
  49         and [false] otherwise. *)
  50
  51     val add: key -> 'a -> 'a t -> 'a t
  52     (** [add x y m] returns a map containing the same bindings as
  53         [m], plus a binding of [x] to [y]. If [x] was already bound
  54         in [m], its previous binding disappears. *)
  55
  56     val singleton: key -> 'a -> 'a t
  57     (** [singleton x y] returns the one-element map that contains a binding [y]
  58         for [x]. *)
  59
  60     val remove: key -> 'a t -> 'a t
  61     (** [remove x m] returns a map containing the same bindings as
  62         [m], except for [x] which is unbound in the returned map. *)
  63
  64     val merge:
  65          (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
  66     (** [merge f m1 m2] computes a map whose keys is a subset of keys of [m1]
  67         and of [m2]. The presence of each such binding, and the corresponding
  68         value, is determined with the function [f]. *)
  69
  70     val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
  71     (** [union f m1 m2] computes a map whose keys is a subset of keys
  72         of [m1] and of [m2]. If a binding is present in [m1] (resp. [m2])
  73         and not in [m2] (resp. [m1]) the same binding is present in
  74         the result. The function [f] is called only in ambiguous cases. *)
  75
  76     val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
  77     (** Total ordering between maps.  The first argument is a total ordering
  78         used to compare data associated with equal keys in the two maps. *)
  79
  80     val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
  81     (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are
  82         equal, that is, contain equal keys and associate them with
  83         equal data.  [cmp] is the equality predicate used to compare
  84         the data associated with the keys. *)
  85
  86     val iter: (key -> 'a -> unit) -> 'a t -> unit
  87     (** [iter f m] applies [f] to all bindings in map [m].
  88        [f] receives the key as first argument, and the associated value
  89        as second argument.  The bindings are passed to [f] in increasing
  90        order with respect to the ordering over the type of the keys. *)
  91
  92     val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
  93     (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], where
  94         [k1 ... kN] are the keys of all bindings in [m] (in increasing
  95         order), and [d1 ... dN] are the associated data. *)
  96
  97     val for_all: (key -> 'a -> bool) -> 'a t -> bool
  98     (** [for_all p m] checks if all the bindings of the map
  99         satisfy the predicate [p]. *)
 100
 101     val exists: (key -> 'a -> bool) -> 'a t -> bool
 102     (** [exists p m] checks if at least one binding of the map
 103         satisfy the predicate [p]. *)
 104
 105     val filter: (key -> 'a -> bool) -> 'a t -> 'a t
 106     (** [filter p m] returns the map with all the bindings in [m]
 107         that satisfy predicate [p]. *)
 108
 109     val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
 110     (** [partition p m] returns a pair of maps [(m1, m2)], where
 111         [m1] contains all the bindings of [s] that satisfy the
 112         predicate [p], and [m2] is the map with all the bindings of
 113         [s] that do not satisfy [p]. *)
 114
 115     val cardinal: 'a t -> int
 116     (** Return the number of bindings of a map. *)
 117
 118     val bindings: 'a t -> (key * 'a) list
 119     (** Return the list of all bindings of the given map.
 120         The returned list is sorted in increasing order with respect
 121         to the ordering [Ord.compare], where [Ord] is the argument
 122         given to {!Extmap.Make}. *)
 123
 124     val min_binding: 'a t -> (key * 'a)
 125     (** Return the smallest binding of the given map
 126         (with respect to the [Ord.compare] ordering), or raise
 127         [Not_found] if the map is empty. *)
 128
 129     val max_binding: 'a t -> (key * 'a)
 130     (** Same as {!Extmap.S.min_binding}, but returns the largest
 131         binding of the given map. *)
 132
 133     val choose: 'a t -> (key * 'a)
 134     (** Return one binding of the given map, or raise [Not_found] if
 135         the map is empty. Which binding is chosen is unspecified,
 136         but equal bindings will be chosen for equal maps. *)
 137
 138     val split: key -> 'a t -> 'a t * 'a option * 'a t
 139     (** [split x m] returns a triple [(l, data, r)], where
 140           [l] is the map with all the bindings of [m] whose key
 141         is strictly less than [x];
 142           [r] is the map with all the bindings of [m] whose key
 143         is strictly greater than [x];
 144           [data] is [None] if [m] contains no binding for [x],
 145           or [Some v] if [m] binds [v] to [x]. *)
 146
 147     val find: key -> 'a t -> 'a
 148     (** [find x m] returns the current binding of [x] in [m],
 149         or raises [Not_found] if no such binding exists. *)
 150
 151     val map: ('a -> 'b) -> 'a t -> 'b t
 152     (** [map f m] returns a map with same domain as [m], where
 153         the associated value [a] of all bindings of [m] has been
 154         replaced by the result of the application of [f] to [a].
 155         The bindings are passed to [f] in increasing order
 156         with respect to the ordering over the type of the keys. *)
 157
 158     val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
 159     (** Same as {!Extmap.S.map}, but the function receives as arguments both
 160         the key and the associated value for each binding of the map. *)
 161
 162     val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
 163     (** [change f x m] returns a map containing the same bindings as
 164         [m], except the binding of [x] in [m] is changed from [y] to
 165         [f (Some y)] if [m] contains a binding of [x], otherwise the
 166         binding of [x] becomes [f None].
 167
 168         [change f x m] corresponds to a more efficient way to do
 169         [match (try f (Some (find x m)) with Not_found -> f None) with
 170           | None -> m
 171           | Some v -> add x v] *)
 172
 173     val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
 174     (** [inter f m1 m2] computes a map whose keys is a subset of
 175         the intersection of keys of [m1] and of [m2]. *)
 176
 177     val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
 178     (** [diff f m1 m2] computes a map whose keys is a subset of keys
 179         of [m1]. [f] is applied on key which belongs to [m1] and [m2]
 180         if [f] returns [None] the binding is removed from [m1],
 181         otherwise [Some d1] is returned, the key binds to [d1] in [m1] *)
 182
 183     val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
 184     (** [submap pr m1 m2] verifies that all the keys in [m1] are in [m2]
 185         and that for each such binding [pr] is verified. *)
 186
 187     val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
 188     (** [disjoint pr m1 m2] verifies that for every common key in [m1]
 189         and [m2], [pr] is verified. *)
 190
 191     val set_union : 'a t -> 'a t -> 'a t
 192     (** [set_union = union (fun _ x _ -> Some x)] *)
 193
 194     val set_inter : 'a t -> 'b t -> 'a t
 195     (** [set_inter = inter (fun _ x _ -> Some x)] *)
 196
 197     val set_diff : 'a t -> 'b t -> 'a t
 198     (** [set_diff = diff (fun _ _ _ -> None)] *)
 199
 200     val set_submap : 'a t -> 'b t -> bool
 201     (** [set_submap = submap (fun _ _ _ -> true)] *)
 202
 203     val set_disjoint : 'a t -> 'b t -> bool
 204     (** [set_disjoint = disjoint (fun _ _ _ -> false)] *)
 205
 206     val set_compare : 'a t -> 'b t -> int
 207     (** [set_compare = compare (fun _ _ -> 0)] *)
 208
 209     val set_equal : 'a t -> 'b t -> bool
 210     (** [set_equal = equal (fun _ _ -> true)] *)
 211
 212     val find_def : 'a -> key -> 'a t -> 'a
 213     (** [find_def x d m] returns the current binding of [x] in [m],
 214         or return [d] if no such binding exists. *)
 215
 216     val find_opt : key -> 'a t -> 'a option
 217     (** [find_opt x m] returns the [Some] of the current binding
 218         of [x] in [m], or return [None] if no such binding exists. *)
 219
 220     val find_exn : exn -> key -> 'a t -> 'a
 221     (** [find_exn exn x d m] returns the current binding
 222         of [x] in [m], or raise [exn] if no such binding exists. *)
 223
 224     val map_filter: ('a -> 'b option) -> 'a t -> 'b t
 225     (** Same as {!Extmap.S.map}, but may remove bindings. *)
 226
 227     val mapi_filter: (key -> 'a -> 'b option) -> 'a t -> 'b t
 228     (** Same as {!Extmap.S.mapi}, but may remove bindings. *)
 229
 230     val mapi_fold:
 231       (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
 232     (** fold and map at the same time *)
 233
 234     val mapi_filter_fold:
 235       (key -> 'a -> 'acc -> 'acc * 'b option) -> 'a t -> 'acc -> 'acc * 'b t
 236     (** Same as {!Extmap.S.mapi_fold}, but may remove bindings. *)
 237
 238     val fold_left: ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
 239     (** same as {!fold} but in the order of [List.fold_left] *)
 240
 241     val fold2_inter: (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
 242     (** fold the common keys of two map at the same time *)
 243
 244     val fold2_union:
 245       (key -> 'a option -> 'b option -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
 246     (** fold the keys which appear in one of the two maps *)
 247
 248     val translate : (key -> key) -> 'a t -> 'a t
 249     (** [translate f m] translates the keys in the map [m] by the
 250         function [f]. [f] must be strictly monotone on the key of [m].
 251         Otherwise it raises invalid_arg *)
 252
 253     val add_new : exn -> key -> 'a -> 'a t -> 'a t
 254     (** [add_new e x v m] binds [x] to [v] in [m] if [x] is not bound,
 255         and raises [e] otherwise. *)
 256
 257     val replace : exn -> key -> 'a -> 'a t -> 'a t
 258     (** [replace e x v m] binds [x] to [v] in [m] if [x] is already bound,
 259         and raises [e] otherwise. *)
 260
 261     val keys: 'a t -> key list
 262     (** Return the list of all keys of the given map.
 263         The returned list is sorted in increasing order with respect
 264         to the ordering [Ord.compare], where [Ord] is the argument
 265         given to {!Extmap.Make}. *)
 266
 267     val values: 'a t -> 'a list
 268     (** Return the list of all values of the given map.
 269         The returned list is sorted in increasing order with respect
 270         to the ordering [Ord.compare] of the keys, where [Ord] is the argument
 271         given to {!Extmap.Make}. *)
 272
 273     val of_list: (key * 'a) list -> 'a t
 274     (** construct a map from a list of bindings. *)
 275
 276     val contains: 'a t -> key -> bool
 277     (** [contains m x] is the same as [mem x m]. *)
 278
 279     val domain : 'a t -> unit t
 280     (** [domain m] returns the set of keys of bindings in [m] *)
 281
 282     val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
 283     (** [subdomain pr m] returns the set of keys of bindings in [m]
 284         that satisfy predicate [pr] *)
 285
 286     val is_num_elt : int -> 'a t -> bool
 287     (** check if the map has the given number of elements *)
 288
 289     type 'a enumeration
 290     (** enumeration: zipper style *)
 291
 292     val val_enum : 'a enumeration -> (key * 'a) option
 293     (** get the current key value pair of the enumeration, return None
 294         if the enumeration reach the end *)
 295
 296     val start_enum : 'a t -> 'a enumeration
 297     (** start the enumeration of the given map *)
 298
 299     val next_enum : 'a enumeration -> 'a enumeration
 300     (** get the next step of the enumeration *)
 301
 302     val start_ge_enum : key -> 'a t -> 'a enumeration
 303     (** start the enumeration of the given map at the first key which
 304         is greater or equal than the given one *)
 305
 306     val next_ge_enum : key -> 'a enumeration -> 'a enumeration
 307     (** get the next (or same) step of the enumeration which key is
 308         greater or equal to the given key *)
 309   end
 310
 311 module Make (Ord : OrderedType) : S with type key = Ord.t
 312 (** Functor building an implementation of the map structure
 313     given a totally ordered type. *)