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
 155     (** Initializes the internal storage. Any previously hashconsed
 156         element is discarded. *)
 157     val init : unit -> unit
 158   end
 159
 160
 161   (** Concrete signature of a module implementing an hashconsed datatype *)
 162   module type S =
 163   sig
 164     type data
 165     type t = private { id   : Uid.t;
 166                        hash : int;
 167                        node : data }
 168     include Abstract with type data := data and type t := t
 169   end
 170
 171 end
 172
 173
 174 module PTSET =
 175 struct
 176   module type S =
 177   sig
 178     include HCONS.S
 179     include AUX.Set with type t := t
 180   end
 181 end
 182
 183 module FINITECOFINITE =
 184 struct
 185   exception InfiniteSet
 186   module type S =
 187   sig
 188     include HCONS.S
 189     include AUX.Set with type t := t
 190     type set
 191     val any : t
 192     val is_any : t -> bool
 193     val is_finite : t -> bool
 194     val kind : t -> [ `Finite | `Cofinite ]
 195     val complement : t -> t
 196     val kind_split : t list -> t * t
 197     val positive : t -> set
 198     val negative : t -> set
 199     val inj_positive : set -> t
 200     val inj_negative : set -> t
 201   end
 202 end