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 (*
  17   Time-stamp: <Last modified on 2013-02-05 15:58:13 CET by Kim Nguyen>
  18 *)
  19
  20 (** This module contains all the signatures of the project, to avoid
  21     code duplication. Each toplevel module (HCONS, PTSET, ...)
  22     corresponds to an existing module in the project. The AUX modules
  23     regroups common auxiliary signatures.
  24 *)
  25
  26
  27 (** The [AUX] module regroups the definitions of common interfaces *)
  28 module  AUX =
  29 struct
  30
  31   (** Type equipped with an equality and hash function.
  32       If [equal a b] then [(hash a) = (hash b)]
  33   *)
  34   module type HashedType =
  35   sig
  36     type t
  37
  38     (** [hash v] returns an integer in the range [ 0 - 2^30-1 ]
  39     *)
  40     val hash : t -> int
  41
  42     (** Equality *)
  43     val equal : t -> t -> bool
  44
  45   end
  46
  47   (** Type equiped with a total ordering *)
  48   module type OrderedType =
  49   sig
  50     type t
  51
  52     (** Total ordering on values of type [t].  [compare a b] returns a
  53         negative number if [a] is strictly smaller than [b], a positive
  54         number if [a] is strictly greater than [b] and 0 if [a] is equal
  55         to [b].  *)
  56     val compare : t -> t -> int
  57   end
  58
  59   (** Type equiped with a pretty-printer *)
  60   module type Printable =
  61   sig
  62     type t
  63     val print : Format.formatter -> t -> unit
  64   end
  65
  66   (** Type with both total ordering and hashing functions.
  67       All modules of that type must enforce than:
  68       [equal a b] if and only if [compare a b = 0]
  69   *)
  70   module type Type =
  71   sig
  72     type t
  73     include HashedType with type t := t
  74     include OrderedType with type t := t
  75   end
  76
  77   (** Signature of a simple HashSet module *)
  78   module type HashSet =
  79   sig
  80     type data
  81     type t
  82     val create : int -> t
  83     val add : t -> data -> unit
  84     val remove : t -> data -> unit
  85     val find : t -> data -> data
  86     val find_all : t -> data -> data list
  87     val clear : t -> unit
  88     val mem : t -> data -> bool
  89   end
  90
  91   (** Signature of simple Set module *)
  92   module type Set =
  93   sig
  94     type elt
  95     type t
  96     val empty : t
  97     val is_empty : t -> bool
  98     val mem : elt -> t -> bool
  99     val add : elt -> t -> t
 100     val singleton : elt -> t
 101     val remove : elt -> t -> t
 102     val union : t -> t -> t
 103     val inter : t -> t -> t
 104     val diff : t -> t -> t
 105     val compare : t -> t -> int
 106     val equal : t -> t -> bool
 107     val subset : t -> t -> bool
 108     val iter : (elt -> unit) -> t -> unit
 109     val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
 110     val for_all : (elt -> bool) -> t -> bool
 111     val exists : (elt -> bool) -> t -> bool
 112     val filter : (elt -> bool) -> t -> t
 113     val partition : (elt -> bool) -> t -> t * t
 114     val cardinal : t -> int
 115     val elements : t -> elt list
 116     val min_elt : t -> elt
 117     val max_elt : t -> elt
 118     val choose : t -> elt
 119     val split : elt -> t -> t * bool * t
 120     val intersect : t -> t -> bool
 121     val is_singleton : t -> bool
 122     val from_list : elt list -> t
 123   end
 124 end
 125
 126 module  HCONS =
 127 struct
 128   (** Abstract signature of a module implementing an hashconsed datatype *)
 129   module type Abstract =
 130   sig
 131
 132     (** The type of the data to be hash-consed *)
 133     type data
 134
 135     (** The type of hashconsed data *)
 136     type t
 137
 138     (** [make v] internalizes the value [v], making it an hashconsed
 139         value.
 140     *)
 141     val make : data -> t
 142
 143     (** [node h] extract the original data from its hashconsed value
 144     *)
 145     val node : t -> data
 146
 147     (** [hash h] returns a hash of [h], such that for every [h1] and
 148         [h2], [equal h1 h2] implies [hash h1 = hash h2].
 149     *)
 150     val hash : t -> int
 151
 152     (** [uid h] returns a unique identifier *)
 153     val uid : t -> Uid.t
 154
 155     (** Equality between hashconsed values. Equivalent to [==] *)
 156     val equal : t -> t -> bool
 157
 158     (** Initializes the internal storage. Any previously hashconsed
 159         element is discarded. *)
 160     val init : unit -> unit
 161
 162     (** Create a dummy (non-hashconsed) node with a boggus identifer
 163         and hash *)
 164     val dummy : data -> t
 165   end
 166
 167
 168   (** Concrete signature of a module implementing an hashconsed datatype *)
 169   module type S =
 170   sig
 171     type data
 172     type t = private { id   : Uid.t;
 173                        hash : int;
 174                        node : data }
 175     include Abstract with type data := data and type t := t
 176   end
 177
 178 end
 179
 180
 181 module PTSET =
 182 struct
 183   module type S =
 184   sig
 185     include HCONS.S
 186     include AUX.Set with type t := t
 187   end
 188 end
 189
 190 module FINITECOFINITE =
 191 struct
 192   exception InfiniteSet
 193   module type S =
 194   sig
 195     include HCONS.S
 196     include AUX.Set with type t := t
 197     type set
 198     val any : t
 199     val is_any : t -> bool
 200     val is_finite : t -> bool
 201     val kind : t -> [ `Finite | `Cofinite ]
 202     val complement : t -> t
 203     val kind_split : t list -> t * t
 204     val positive : t -> set
 205     val negative : t -> set
 206     val inj_positive : set -> t
 207     val inj_negative : set -> t
 208   end
 209 end
 210
 211 module FORMULA =
 212 struct
 213   module type ATOM =
 214   sig
 215     type t
 216     type ctx
 217     val eval : ctx -> t -> bool
 218     val neg : t -> t
 219     include HCONS.S with type t := t
 220     include AUX.Printable with type t := t
 221   end
 222   module type S =
 223   sig
 224     module Atom : ATOM
 225     include HCONS.S
 226     include AUX.Printable with type t := t
 227     val of_bool : bool -> t
 228     val true_ : t
 229     val false_ : t
 230     val or_ : t -> t -> t
 231     val and_ : t -> t -> t
 232     val not_ : t -> t
 233     val diff_ : t -> t -> t
 234     val eval : Atom.ctx -> t -> bool
 235   end
 236
 237 end