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-01-30 19:07:19 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   end
 162
 163
 164   (** Concrete signature of a module implementing an hashconsed datatype *)
 165   module type S =
 166   sig
 167     type data
 168     type t = private { id   : Uid.t;
 169                        hash : int;
 170                        node : data }
 171     include Abstract with type data := data and type t := t
 172   end
 173
 174 end
 175
 176
 177 module PTSET =
 178 struct
 179   module type S =
 180   sig
 181     include HCONS.S
 182     include AUX.Set with type t := t
 183   end
 184 end
 185
 186 module FINITECOFINITE =
 187 struct
 188   exception InfiniteSet
 189   module type S =
 190   sig
 191     include HCONS.S
 192     include AUX.Set with type t := t
 193     type set
 194     val any : t
 195     val is_any : t -> bool
 196     val is_finite : t -> bool
 197     val kind : t -> [ `Finite | `Cofinite ]
 198     val complement : t -> t
 199     val kind_split : t list -> t * t
 200     val positive : t -> set
 201     val negative : t -> set
 202     val inj_positive : set -> t
 203     val inj_negative : set -> t
 204   end
 205 end
 206
 207 module FORMULA =
 208 struct
 209   module type ATOM =
 210   sig
 211     type t
 212     type ctx
 213     val eval : ctx -> t -> bool
 214     val neg : t -> t
 215     include HCONS.S with type t := t
 216     include AUX.Printable with type t := t
 217   end
 218   module type S =
 219   sig
 220     module Atom : ATOM
 221     include HCONS.S
 222     include AUX.Printable with type t := t
 223     val of_bool : bool -> t
 224     val true_ : t
 225     val false_ : t
 226     val or_ : t -> t -> t
 227     val and_ : t -> t -> t
 228     val not_ : t -> t
 229     val diff_ : t -> t -> t
 230     val eval : Atom.ctx -> t -> bool
 231   end
 232
 233 end