Usable version:

[tatoo.git] / src / sigs.ml

diff --git a/src/sigs.ml b/src/sigs.ml
new file mode 100644 (file)
index 0000000..3664d4e
--- /dev/null
+++ b/src/sigs.ml
@@ -0,0 +1,126 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Various generic signatures *)
+
+module type HashedType =
+sig
+  type t
+  val hash : t -> int
+    (** [hash v] returns an integer in the range
+        [ 0 - 2^30-1 ]
+    *)
+  val equal : t -> t -> bool
+    (** Equality *)
+end
+(** Type equipped with an equality and hash function.
+    If [equal a b] then [(hash a) = (hash b)]
+*)
+
+
+module type OrderedType =
+sig
+  type t
+  val compare : t -> t -> int
+    (** Total ordering on values of type [t].
+        [compare a b] returns a negative number if [a] is strictly
+        smaller than [b], a positive number if [a] is strictly greater
+        than [b] and 0 if [a] is equal to [b].
+    *)
+end
+(** Type equiped with a total ordering *)
+
+module type Printable =
+sig
+  type t
+  val print : Format.formatter -> t -> unit
+end
+  (** Type equiped with a pretty-printer *)
+
+
+module type Type =
+sig
+  type t
+  include HashedType with type t := t
+  include OrderedType with type t := t
+end
+  (** Type with both total ordering and hashing functions.
+      All modules of that type must enforce than:
+      [equal a b] if and only if [compare a b = 0]
+  *)
+
+module type HashSet =
+sig
+  type data
+  type t
+  val create : int -> t
+  val add : t -> data -> unit
+  val remove : t -> data -> unit
+  val find : t -> data -> data
+  val find_all : t -> data -> data list
+  val clear : t -> unit
+  val mem : t -> data -> bool
+end
+(** Signature of a simple HashSet module *)
+module type Set =
+sig
+  type elt
+  type t
+  val empty : t
+  val is_empty : t -> bool
+  val mem : elt -> t -> bool
+  val add : elt -> t -> t
+  val singleton : elt -> t
+  val remove : elt -> t -> t
+  val union : t -> t -> t
+  val inter : t -> t -> t
+  val diff : t -> t -> t
+  val compare : t -> t -> int
+  val equal : t -> t -> bool
+  val subset : t -> t -> bool
+  val iter : (elt -> unit) -> t -> unit
+  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+  val for_all : (elt -> bool) -> t -> bool
+  val exists : (elt -> bool) -> t -> bool
+  val filter : (elt -> bool) -> t -> t
+  val partition : (elt -> bool) -> t -> t * t
+  val cardinal : t -> int
+  val elements : t -> elt list
+  val min_elt : t -> elt
+  val max_elt : t -> elt
+  val choose : t -> elt
+  val split : elt -> t -> t * bool * t
+  val intersect : t -> t -> bool
+  val is_singleton : t -> bool
+  val from_list : elt list -> t
+end
+
+exception InfiniteSet
+
+module type FiniteCofiniteSet =
+sig
+  include Set
+  type set
+  val any : t
+  val is_any : t -> bool
+  val is_finite : t -> bool
+  val kind : t -> [ `Finite | `Cofinite ]
+  val complement : t -> t
+  val kind_split : t list -> t * t
+  val positive : t -> set
+  val negative : t -> set
+  val inj_positive : set -> t
+  val inj_negative : set -> t
+end