(***********************************************************************)
(*                                                                     *)
(*                               TAToo                                 *)
(*                                                                     *)
(*                     Kim Nguyen, LRI UMR8623                         *)
(*                   Université Paris-Sud & CNRS                       *)
(*                                                                     *)
(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
(*  Recherche Scientifique. All rights reserved.  This file is         *)
(*  distributed under the terms of the GNU Lesser General Public       *)
(*  License, with the special exception on linking described in file   *)
(*  ../LICENSE.                                                        *)
(*                                                                     *)
(***********************************************************************)

(** 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.
*)


(** 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 ]
    *)
    val hash : t -> int

    (** 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

  (** 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

  (** 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

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


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