X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fsigs.ml;h=a3cf635421ec47e7124bfdd0357cf021517245c4;hb=6b66008811639324be623a42037b60e02056772c;hp=3664d4ecfe5e9393082dfb834114d2ce5184aee6;hpb=cba2938d929fd5119b1491686ddc224d5af618c6;p=tatoo.git

diff --git a/src/sigs.ml b/src/sigs.ml
index 3664d4e..a3cf635 100644
--- a/src/sigs.ml
+++ b/src/sigs.ml
@@ -13,114 +13,221 @@
 (*                                                                     *)
 (***********************************************************************)
 
-(** 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)]
+(*
+  Time-stamp: <Last modified on 2013-01-30 19:07:19 CET by Kim Nguyen>
+*)
+
+(** 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
 
-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
+  (** 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
-(** 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  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
+
 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 PTSET =
+struct
+  module type S =
+  sig
+    include HCONS.S
+    include AUX.Set with type t := t
+  end
+end
+
+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
+
+module FORMULA =
+struct
+  module type ATOM =
+  sig
+    type t
+    type ctx
+    val eval : ctx -> t -> bool
+    val neg : t -> t
+    include HCONS.S with type t := t
+    include AUX.Printable with type t := t
+  end
+  module type S =
+  sig
+    module Atom : ATOM
+    include HCONS.S
+    include AUX.Printable with type t := t
+    val of_bool : bool -> t
+    val true_ : t
+    val false_ : t
+    val or_ : t -> t -> t
+    val and_ : t -> t -> t
+    val not_ : t -> t
+    val diff_ : t -> t -> t
+    val eval : Atom.ctx -> t -> bool
+  end
+
 end