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 (***********************************************************************)
17 Time-stamp: <Last modified on 2013-01-30 19:07:19 CET by Kim Nguyen>
20 (** This module contains all the signatures of the project, to avoid
21 code duplication. Each toplevel module (HCONS, PTSET, ...)
22 corresponds to an existing module in the project. The AUX modules
23 regroups common auxiliary signatures.
27 (** The [AUX] module regroups the definitions of common interfaces *)
31 (** Type equipped with an equality and hash function.
32 If [equal a b] then [(hash a) = (hash b)]
34 module type HashedType =
38 (** [hash v] returns an integer in the range [ 0 - 2^30-1 ]
43 val equal : t -> t -> bool
47 (** Type equiped with a total ordering *)
48 module type OrderedType =
52 (** Total ordering on values of type [t]. [compare a b] returns a
53 negative number if [a] is strictly smaller than [b], a positive
54 number if [a] is strictly greater than [b] and 0 if [a] is equal
56 val compare : t -> t -> int
59 (** Type equiped with a pretty-printer *)
60 module type Printable =
63 val print : Format.formatter -> t -> unit
66 (** Type with both total ordering and hashing functions.
67 All modules of that type must enforce than:
68 [equal a b] if and only if [compare a b = 0]
73 include HashedType with type t := t
74 include OrderedType with type t := t
77 (** Signature of a simple HashSet module *)
83 val add : t -> data -> unit
84 val remove : t -> data -> unit
85 val find : t -> data -> data
86 val find_all : t -> data -> data list
88 val mem : t -> data -> bool
91 (** Signature of simple Set module *)
97 val is_empty : t -> bool
98 val mem : elt -> t -> bool
99 val add : elt -> t -> t
100 val singleton : elt -> t
101 val remove : elt -> t -> t
102 val union : t -> t -> t
103 val inter : t -> t -> t
104 val diff : t -> t -> t
105 val compare : t -> t -> int
106 val equal : t -> t -> bool
107 val subset : t -> t -> bool
108 val iter : (elt -> unit) -> t -> unit
109 val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
110 val for_all : (elt -> bool) -> t -> bool
111 val exists : (elt -> bool) -> t -> bool
112 val filter : (elt -> bool) -> t -> t
113 val partition : (elt -> bool) -> t -> t * t
114 val cardinal : t -> int
115 val elements : t -> elt list
116 val min_elt : t -> elt
117 val max_elt : t -> elt
118 val choose : t -> elt
119 val split : elt -> t -> t * bool * t
120 val intersect : t -> t -> bool
121 val is_singleton : t -> bool
122 val from_list : elt list -> t
128 (** Abstract signature of a module implementing an hashconsed datatype *)
129 module type Abstract =
132 (** The type of the data to be hash-consed *)
135 (** The type of hashconsed data *)
138 (** [make v] internalizes the value [v], making it an hashconsed
143 (** [node h] extract the original data from its hashconsed value
147 (** [hash h] returns a hash of [h], such that for every [h1] and
148 [h2], [equal h1 h2] implies [hash h1 = hash h2].
152 (** [uid h] returns a unique identifier *)
155 (** Equality between hashconsed values. Equivalent to [==] *)
156 val equal : t -> t -> bool
158 (** Initializes the internal storage. Any previously hashconsed
159 element is discarded. *)
160 val init : unit -> unit
164 (** Concrete signature of a module implementing an hashconsed datatype *)
168 type t = private { id : Uid.t;
171 include Abstract with type data := data and type t := t
182 include AUX.Set with type t := t
186 module FINITECOFINITE =
188 exception InfiniteSet
192 include AUX.Set with type t := t
195 val is_any : t -> bool
196 val is_finite : t -> bool
197 val kind : t -> [ `Finite | `Cofinite ]
198 val complement : t -> t
199 val kind_split : t list -> t * t
200 val positive : t -> set
201 val negative : t -> set
202 val inj_positive : set -> t
203 val inj_negative : set -> t
213 val eval : ctx -> t -> bool
215 include HCONS.S with type t := t
216 include AUX.Printable with type t := t
222 include AUX.Printable with type t := t
223 val of_bool : bool -> t
226 val or_ : t -> t -> t
227 val and_ : t -> t -> t
229 val diff_ : t -> t -> t
230 val eval : Atom.ctx -> t -> bool