(* *)
(***********************************************************************)
-(** 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)]
+(** This module contains all the signatures of the project, to avoid
+ code duplication. Each toplevel module (HCONS, PTSET, ...)
+ corresponds to an existing module in the project. The AUX modules
+ regroups common auxiliary signatures.
*)
-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].
+(** The [AUX] module regroups the definitions of common interfaces *)
+module AUX =
+struct
+
+ (** Type equipped with an equality and hash function.
+ If [equal a b] then [(hash a) = (hash b)]
+ *)
+ module type HashedType =
+ sig
+ type t
+
+ (** [hash v] returns an integer in the range [ 0 - 2^30-1 ]
*)
-end
-(** Type equiped with a total ordering *)
+ val hash : t -> int
-module type Printable =
-sig
- type t
- val print : Format.formatter -> t -> unit
-end
- (** Type equiped with a pretty-printer *)
+ (** Equality *)
+ val equal : t -> t -> bool
+ end
+
+ (** Type equiped with a total ordering *)
+ module type OrderedType =
+ sig
+ type t
+
+ (** 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]. *)
+ val compare : t -> t -> int
+ end
+
+ (** Type equiped with a pretty-printer *)
+ module type Printable =
+ sig
+ type t
+ val print : Format.formatter -> t -> unit
+ end
-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 Type =
+ sig
+ type t
+ include HashedType with type t := t
+ include OrderedType with type t := t
+ end
+
+ (** Signature of a simple HashSet module *)
+ 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 simple Set 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
+end
+
+module HCONS =
+struct
+ (** Abstract signature of a module implementing an hashconsed datatype *)
+ module type Abstract =
+ sig
+
+ (** The type of the data to be hash-consed *)
+ type data
+
+ (** The type of hashconsed data *)
+ type t
+
+ (** [make v] internalizes the value [v], making it an hashconsed
+ value.
+ *)
+ val make : data -> t
+
+ (** [node h] extract the original data from its hashconsed value
+ *)
+ val node : t -> data
+
+ (** [hash h] returns a hash of [h], such that for every [h1] and
+ [h2], [equal h1 h2] implies [hash h1 = hash h2].
+ *)
+ val hash : t -> int
+
+ (** [uid h] returns a unique identifier *)
+ val uid : t -> Uid.t
+
+ (** Equality between hashconsed values. Equivalent to [==] *)
+ val equal : t -> t -> bool
+
+ (** Initializes the internal storage. Any previously hashconsed
+ element is discarded. *)
+ val init : unit -> unit
+ end
+
+
+ (** Concrete signature of a module implementing an hashconsed datatype *)
+ module type S =
+ sig
+ type data
+ type t = private { id : Uid.t;
+ hash : int;
+ node : data }
+ include Abstract with type data := data and type t := t
+ end
-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
+
+
+module PTSET =
+struct
+ module type S =
+ sig
+ include HCONS.S
+ include AUX.Set with type t := t
+ end
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
+module FINITECOFINITE =
+struct
+ exception InfiniteSet
+ module type S =
+ sig
+ include HCONS.S
+ include AUX.Set with type t := t
+ 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
end
projects / tatoo.git / blobdiff