1 (***********************************************************************)
5 (* Kim Nguyen, LRI UMR8623 *)
6 (* Université Paris-Sud & CNRS *)
8 (* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
9 (* Recherche Scientifique. All rights reserved. This file is *)
10 (* distributed under the terms of the GNU Lesser General Public *)
11 (* License, with the special exception on linking described in file *)
14 (***********************************************************************)
16 (** This module contains all the signatures of the project, to avoid
17 code duplication. Each toplevel module (HCONS, PTSET, ...)
18 corresponds to an existing module in the project. The AUX modules
19 regroups common auxiliary signatures.
23 (** The [AUX] module regroups the definitions of common interfaces *)
27 (** Type equipped with an equality and hash function.
28 If [equal a b] then [(hash a) = (hash b)]
30 module type HashedType =
34 (** [hash v] returns an integer in the range [ 0 - 2^30-1 ]
39 val equal : t -> t -> bool
43 (** Type equiped with a total ordering *)
44 module type OrderedType =
48 (** Total ordering on values of type [t]. [compare a b] returns a
49 negative number if [a] is strictly smaller than [b], a positive
50 number if [a] is strictly greater than [b] and 0 if [a] is equal
52 val compare : t -> t -> int
55 (** Type equiped with a pretty-printer *)
56 module type Printable =
59 val print : Format.formatter -> t -> unit
62 (** Type with both total ordering and hashing functions.
63 All modules of that type must enforce than:
64 [equal a b] if and only if [compare a b = 0]
69 include HashedType with type t := t
70 include OrderedType with type t := t
73 (** Signature of a simple HashSet module *)
79 val add : t -> data -> unit
80 val remove : t -> data -> unit
81 val find : t -> data -> data
82 val find_all : t -> data -> data list
84 val mem : t -> data -> bool
87 (** Signature of simple Set module *)
93 val is_empty : t -> bool
94 val mem : elt -> t -> bool
95 val add : elt -> t -> t
96 val singleton : elt -> t
97 val remove : elt -> t -> t
98 val union : t -> t -> t
99 val inter : t -> t -> t
100 val diff : t -> t -> t
101 val compare : t -> t -> int
102 val equal : t -> t -> bool
103 val subset : t -> t -> bool
104 val iter : (elt -> unit) -> t -> unit
105 val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
106 val for_all : (elt -> bool) -> t -> bool
107 val exists : (elt -> bool) -> t -> bool
108 val filter : (elt -> bool) -> t -> t
109 val partition : (elt -> bool) -> t -> t * t
110 val cardinal : t -> int
111 val elements : t -> elt list
112 val min_elt : t -> elt
113 val max_elt : t -> elt
114 val choose : t -> elt
115 val split : elt -> t -> t * bool * t
116 val intersect : t -> t -> bool
117 val is_singleton : t -> bool
118 val from_list : elt list -> t
124 (** Abstract signature of a module implementing an hashconsed datatype *)
125 module type Abstract =
128 (** The type of the data to be hash-consed *)
131 (** The type of hashconsed data *)
134 (** [make v] internalizes the value [v], making it an hashconsed
139 (** [node h] extract the original data from its hashconsed value
143 (** [hash h] returns a hash of [h], such that for every [h1] and
144 [h2], [equal h1 h2] implies [hash h1 = hash h2].
148 (** [uid h] returns a unique identifier *)
151 (** Equality between hashconsed values. Equivalent to [==] *)
152 val equal : t -> t -> bool
154 (** Initializes the internal storage. Any previously hashconsed
155 element is discarded. *)
156 val init : unit -> unit
160 (** Concrete signature of a module implementing an hashconsed datatype *)
164 type t = private { id : Uid.t;
167 include Abstract with type data := data and type t := t
178 include AUX.Set with type t := t
182 module FINITECOFINITE =
184 exception InfiniteSet
188 include AUX.Set with type t := t
191 val is_any : t -> bool
192 val is_finite : t -> bool
193 val kind : t -> [ `Finite | `Cofinite ]
194 val complement : t -> t
195 val kind_split : t list -> t * t
196 val positive : t -> set
197 val negative : t -> set
198 val inj_positive : set -> t
199 val inj_negative : set -> t