src/sigs.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                     Kim Nguyen, LRI UMR8623                         *)
   6 (*                   Université Paris-Sud & CNRS                       *)
   7 (*                                                                     *)
   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   *)
  12 (*  ../LICENSE.                                                        *)
  13 (*                                                                     *)
  14 (***********************************************************************)
  15
  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.
  20 *)
  21
  22
  23 (** The [AUX] module regroups the definitions of common interfaces *)
  24 module  AUX =
  25 struct
  26
  27   (** Type equipped with an equality and hash function.
  28       If [equal a b] then [(hash a) = (hash b)]
  29   *)
  30   module type HashedType =
  31   sig
  32     type t
  33
  34     (** [hash v] returns an integer in the range [ 0 - 2^30-1 ]
  35     *)
  36     val hash : t -> int
  37
  38     (** Equality *)
  39     val equal : t -> t -> bool
  40
  41   end
  42
  43   (** Type equiped with a total ordering *)
  44   module type OrderedType =
  45   sig
  46     type t
  47
  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
  51         to [b].  *)
  52     val compare : t -> t -> int
  53   end
  54
  55   (** Type equiped with a pretty-printer *)
  56   module type Printable =
  57   sig
  58     type t
  59     val print : Format.formatter -> t -> unit
  60   end
  61
  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]
  65   *)
  66   module type Type =
  67   sig
  68     type t
  69     include HashedType with type t := t
  70     include OrderedType with type t := t
  71   end
  72
  73   (** Signature of a simple HashSet module *)
  74   module type HashSet =
  75   sig
  76     type data
  77     type t
  78     val create : int -> t
  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
  83     val clear : t -> unit
  84     val mem : t -> data -> bool
  85   end
  86
  87   (** Signature of simple Set module *)
  88   module type Set =
  89   sig
  90     type elt
  91     type t
  92     val empty : t
  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
 119   end
 120 end
 121
 122 module  HCONS =
 123 struct
 124   (** Abstract signature of a module implementing an hashconsed datatype *)
 125   module type Abstract =
 126   sig
 127
 128     (** The type of the data to be hash-consed *)
 129     type data
 130
 131     (** The type of hashconsed data *)
 132     type t
 133
 134     (** [make v] internalizes the value [v], making it an hashconsed
 135         value.
 136     *)
 137     val make : data -> t
 138
 139     (** [node h] extract the original data from its hashconsed value
 140     *)
 141     val node : t -> data
 142
 143     (** [hash h] returns a hash of [h], such that for every [h1] and
 144         [h2], [equal h1 h2] implies [hash h1 = hash h2].
 145     *)
 146     val hash : t -> int
 147
 148     (** [uid h] returns a unique identifier *)
 149     val uid : t -> Uid.t
 150
 151     (** Equality between hashconsed values. Equivalent to [==] *)
 152     val equal : t -> t -> bool
 153
 154     (** Initializes the internal storage. Any previously hashconsed
 155         element is discarded. *)
 156     val init : unit -> unit
 157   end
 158
 159
 160   (** Concrete signature of a module implementing an hashconsed datatype *)
 161   module type S =
 162   sig
 163     type data
 164     type t = private { id   : Uid.t;
 165                        hash : int;
 166                        node : data }
 167     include Abstract with type data := data and type t := t
 168   end
 169
 170 end
 171
 172
 173 module PTSET =
 174 struct
 175   module type S =
 176   sig
 177     include HCONS.S
 178     include AUX.Set with type t := t
 179   end
 180 end
 181
 182 module FINITECOFINITE =
 183 struct
 184   exception InfiniteSet
 185   module type S =
 186   sig
 187     include HCONS.S
 188     include AUX.Set with type t := t
 189     type set
 190     val any : 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
 200   end
 201 end