extset.mli 6.34 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10 11
(********************************************************************)

12
(** Sets over ordered types *)
13

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
14 15 16 17 18
(** Input signature of the functor {!Extset.Make}. *)
module type OrderedType = Set.OrderedType

(** Output signature of the functor {!Extset.Make}. *)
module type S =
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
  sig
    module M : Extmap.S
    (** The module of association tables over [elt]. *)

    type elt = M.key
    (** The type of set elements. *)

    type t = unit M.t
    (** The type of sets of type [elt]. *)

    val empty: t
    (** The empty set. *)

    val is_empty: t -> bool
    (** Test whether a set is empty or not. *)

    val mem: elt -> t -> bool
    (** [mem x s] returns [true] if [s] contains [x],
        and [false] otherwise. *)

    val add: elt -> t -> t
    (** [add x s] returns a set containing the same elements as
        [s], plus [x]. *)

    val singleton: elt -> t
    (** [singleton x] returns the one-element set that contains [x]. *)

    val remove: elt -> t -> t
    (** [remove x s] returns a set containing the same elements as [s],
        except for [x]. *)

    val merge: (elt -> bool -> bool -> bool) -> t -> t -> t
    (** [merge f s1 s2] computes a set whose elts is a subset of elts
        of [s1] and of [s2]. The presence of each such element is
        determined with the function [f]. *)

    val compare: t -> t -> int
    (** Total ordering between sets. *)

    val equal: t -> t -> bool
    (** [equal s1 s2] tests whether the sets [s1] and [s2] are equal. *)

    val subset: t -> t -> bool
    (** [subset s1 s2] tests whether the set [s1] is a subset of [s2]. *)

    val disjoint: t -> t -> bool
    (** [disjoint s1 s2] tests whether the sets [s1] and [s2]
        are disjoint. *)

    val iter: (elt -> unit) -> t -> unit
    (** [iter f s] applies [f] to all elements of [s].
        The elements are passed to [f] in increasing order with respect
        to the ordering over the type of the elts. *)

    val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
    (** [fold f s a] computes [(f eN ... (f e1 a)...)],
        where [e1 ... eN] are the element of [s] in increasing order. *)

    val for_all: (elt -> bool) -> t -> bool
    (** [for_all p s] checks if all the elements of [s] satisfy
        the predicate [p]. *)

    val exists: (elt -> bool) -> t -> bool
    (** [exists p s] checks if at least one element of [s] satisfies
        the predicate [p]. *)

    val filter: (elt -> bool) -> t -> t
    (** [filter p s] returns the set with all the elements of [s]
        that satisfy predicate [p]. *)

    val partition: (elt -> bool) -> t -> t * t
    (** [partition p s] returns a pair of sets [(s1, s2)], where
        [s1] contains all the elements of [s] that satisfy the
        predicate [p], and [s2] is the map with all the elements
        of [s] that do not satisfy [p]. *)

    val cardinal: t -> int
    (** Return the number of elements in a set. *)

    val elements: t -> elt list
    (** Return the list of all elements of the given set.
        The returned list is sorted in increasing order. *)

    val min_elt: t -> elt
    (** Return the smallest element of the given set or raise
        [Not_found] if the set is empty. *)

    val max_elt: t -> elt
    (** Return the largest element of the given set or raise
        [Not_found] if the set is empty. *)

    val choose: t -> elt
    (** Return one element of the given set, or raise [Not_found] if
        the set is empty. Which element is chosen is unspecified,
        but equal elements will be chosen for equal sets. *)

    val split: elt -> t -> t * bool * t
    (** [split x s] returns a triple [(l, mem, r)], where
        [l] is the set with all the elements of [s] that are
        strictly less than [x];
        [r] is the set with all the elements of [s] that are
        strictly greater than [x];
        [mem] is [true] if [x] belongs to [s] and [false] otherwise. *)

    val change : (bool -> bool) -> elt -> t -> t
    (** [change f x s] returns a set containing the same elements as
        [s], except [x] which is added to [s] if [f (mem x s)] returns
        [true] and removed otherwise. *)

    val union : t -> t -> t
    (** [union f s1 s2] computes the union of two sets *)

    val inter : t -> t -> t
    (** [inter f s1 s2] computes the intersection of two sets *)

    val diff : t -> t -> t
    (** [diff f s1 s2] computes the difference of two sets *)

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
137
    val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
138 139
    (** same as {!fold} but in the order of {!List.fold_left} *)

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
140 141 142 143 144 145 146
    val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
    (** [fold2_inter f s1 s2 a] computes [(f eN ... (f e1 a) ...)],
        where [e1 ... eN] are the elements of [inter s1 s2]
        in increasing order. *)

    val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
    (** [fold2_union f s1 s2 a] computes [(f eN ... (f e1 a) ...)],
147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165
        where [e1 ... eN] are the elements of [union s1 s2]
        in increasing order. *)

    val translate : (elt -> elt) -> t -> t
    (** [translate f s] translates the elements in the set [s] by the
        function [f]. [f] must be strictly monotone on the elements of [s].
        Otherwise it raises invalid_arg *)

    val add_new : exn -> elt -> t -> t
    (** [add_new e x s] adds [x] to [s] if [s] does not contain [x],
        and raises [e] otherwise. *)

    val is_num_elt : int -> t -> bool
    (** check if the map has the given number of elements *)

    val of_list: elt list -> t
    (** construct a set from a list of elements *)
  end

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
166 167 168
module MakeOfMap (M : Extmap.S) : S with module M = M
(** Functor building an implementation of the set structure
    given a totally ordered type. *)
169

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
170 171 172
module Make (Ord : OrderedType) : S with type M.key = Ord.t
(** Functor building an implementation of the set structure
    given a totally ordered type. *)