From f5e7e53901bfc30b6234e6026a2c984bfceff694 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Mon, 4 Mar 2013 23:34:44 +0100 Subject: [PATCH] Split the sig.ml module in *_sig.ml (one for each module) --- src/auto/formula.ml | 6 +- src/auto/formula.mli | 4 +- src/auto/state.mli | 4 +- src/utils.mlpack | 5 +- src/utils/common_sig.ml | 108 +++++++++++++++ src/utils/finiteCofinite.ml | 8 +- src/utils/finiteCofinite.mli | 4 +- src/utils/finiteCofinite_sig.ml | 36 +++++ src/utils/hcons.ml | 10 +- src/utils/hcons.mli | 12 +- src/utils/hcons_sig.ml | 68 +++++++++ src/utils/misc.ml | 8 +- src/utils/ptset.ml | 8 +- src/utils/ptset.mli | 4 +- src/utils/ptset_sig.ml | 24 ++++ src/utils/qName.mli | 6 +- src/utils/qNameSet.mli | 14 +- src/utils/sigs.ml | 237 -------------------------------- 18 files changed, 284 insertions(+), 282 deletions(-) create mode 100644 src/utils/common_sig.ml create mode 100644 src/utils/finiteCofinite_sig.ml create mode 100644 src/utils/hcons_sig.ml create mode 100644 src/utils/ptset_sig.ml delete mode 100644 src/utils/sigs.ml diff --git a/src/auto/formula.ml b/src/auto/formula.ml index 27bd19a..a27ffc6 100644 --- a/src/auto/formula.ml +++ b/src/auto/formula.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -34,7 +34,7 @@ sig val eval : ctx -> t -> bool val neg : t -> t include Hcons.Abstract with type t := t - include Sigs.AUX.Printable with type t := t + include Common_sig.Printable with type t := t end type ('formula,'pred) expr = @@ -58,7 +58,7 @@ struct module rec Node : Hcons.S with type data = Data.t = Hcons.Make (Data) - and Data : Hashtbl.HashedType with type t = Node.t node = + and Data : Common_sig.HashedType with type t = Node.t node = struct type t = Node.t node let equal x y = diff --git a/src/auto/formula.mli b/src/auto/formula.mli index a537b2c..78df01c 100644 --- a/src/auto/formula.mli +++ b/src/auto/formula.mli @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) module type PREDICATE = @@ -24,7 +24,7 @@ sig val eval : ctx -> t -> bool val neg : t -> t include Utils.Hcons.Abstract with type t := t - include Utils.Sigs.AUX.Printable with type t := t + include Utils.Common_sig.Printable with type t := t end type ('formula,'pred) expr = diff --git a/src/auto/state.mli b/src/auto/state.mli index f86ddcd..89d67cd 100644 --- a/src/auto/state.mli +++ b/src/auto/state.mli @@ -14,12 +14,12 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) (** Implementation of states *) -include Sigs.AUX.Type with type t = int +include Common_sig.Type with type t = int val make : unit -> t (** Generate a fresh state *) diff --git a/src/utils.mlpack b/src/utils.mlpack index 27622d0..8115b79 100644 --- a/src/utils.mlpack +++ b/src/utils.mlpack @@ -1,9 +1,12 @@ +utils/Common_sig utils/FiniteCofinite +utils/FiniteCofinite_sig utils/Hcons +utils/Hcons_sig utils/Misc utils/Pretty +utils/Ptset_sig utils/Ptset utils/QName utils/QNameSet -utils/Sigs utils/Uid diff --git a/src/utils/common_sig.ml b/src/utils/common_sig.ml new file mode 100644 index 0000000..37437e4 --- /dev/null +++ b/src/utils/common_sig.ml @@ -0,0 +1,108 @@ +(***********************************************************************) +(* *) +(* 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. *) +(* *) +(***********************************************************************) + +(* + Time-stamp: +*) + +(** 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 + +module type Type = +sig + type t + include HashedType with type t := t + include OrderedType with type t := t +end + +(** Type equiped with a pretty-printer *) +module type Printable = +sig + type t + val print : Format.formatter -> t -> unit +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 diff --git a/src/utils/finiteCofinite.ml b/src/utils/finiteCofinite.ml index 8fcf33d..2bfe70c 100644 --- a/src/utils/finiteCofinite.ml +++ b/src/utils/finiteCofinite.ml @@ -14,15 +14,15 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" -include Sigs.FINITECOFINITE +include FiniteCofinite_sig module type HConsBuilder = - functor (H : Sigs.AUX.HashedType) -> Hcons.S with type data = H.t + functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t module Builder (HCB : HConsBuilder) (E : Ptset.S) : S with type elt = E.elt and type set = E.t = @@ -139,7 +139,7 @@ struct in first_cofinite E.empty l - let exn = Sigs.FINITECOFINITE.InfiniteSet + let exn = FiniteCofinite_sig.InfiniteSet let fold f t a = match t.node with | Finite s -> E.fold f s a diff --git a/src/utils/finiteCofinite.mli b/src/utils/finiteCofinite.mli index 44ec882..cd92cda 100644 --- a/src/utils/finiteCofinite.mli +++ b/src/utils/finiteCofinite.mli @@ -14,13 +14,13 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) (** Implementation of hashconsed finite or cofinite sets. *) -include module type of Sigs.FINITECOFINITE +include module type of FiniteCofinite_sig (** Output signature of the {!FiniteCofinite.Make} and {!FiniteCofinite.Weak} functors.*) diff --git a/src/utils/finiteCofinite_sig.ml b/src/utils/finiteCofinite_sig.ml new file mode 100644 index 0000000..da17049 --- /dev/null +++ b/src/utils/finiteCofinite_sig.ml @@ -0,0 +1,36 @@ +(***********************************************************************) +(* *) +(* 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. *) +(* *) +(***********************************************************************) + +(* + Time-stamp: +*) + +exception InfiniteSet +module type S = +sig + include Hcons.S + include Common_sig.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 diff --git a/src/utils/hcons.ml b/src/utils/hcons.ml index eba8bac..3fc3e71 100644 --- a/src/utils/hcons.ml +++ b/src/utils/hcons.ml @@ -14,17 +14,17 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) -include Sigs.HCONS +include Hcons_sig module type TableBuilder = functor - (H : Sigs.AUX.HashedType) -> - Sigs.AUX.HashSet with type data = H.t + (H : Common_sig.HashedType) -> + Common_sig.HashSet with type data = H.t -module Builder (TB : TableBuilder) (H : Sigs.AUX.HashedType) = +module Builder (TB : TableBuilder) (H : Common_sig.HashedType) = struct type data = H.t type t = { id : Uid.t; diff --git a/src/utils/hcons.mli b/src/utils/hcons.mli index c1e8c00..b4049a0 100644 --- a/src/utils/hcons.mli +++ b/src/utils/hcons.mli @@ -14,25 +14,25 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) (** Implementation of generic hashconsing. *) -include module type of Sigs.HCONS +include module type of Hcons_sig (** Output signature of the functor {!Hcons.Make} *) -module Make (H : Sigs.AUX.HashedType) : S with type data = H.t +module Make (H : Common_sig.HashedType) : S with type data = H.t (** Functor building an implementation of hashconsed values for a given - implementation of {!Sigs.HashedType}. Hashconsed values are + implementation of {!Common_sig.HashedType}. Hashconsed values are persistent: the are kept in memory even if no external reference remain. Calling [init()] explicitely will reclaim the space. *) -module Weak (H : Sigs.AUX.HashedType) : S with type data = H.t +module Weak (H : Common_sig.HashedType) : S with type data = H.t (** Functor building an implementation of hashconsed values for a given - implementation of {!Sigs.HashedType}. Hashconsed values have a + implementation of {!Common_sig.HashedType}. Hashconsed values have a weak semantics: they may be reclaimed as soon as no external reference to them exists. The space may still be reclaimed explicitely by calling [init]. diff --git a/src/utils/hcons_sig.ml b/src/utils/hcons_sig.ml new file mode 100644 index 0000000..599819c --- /dev/null +++ b/src/utils/hcons_sig.ml @@ -0,0 +1,68 @@ +(***********************************************************************) +(* *) +(* 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. *) +(* *) +(***********************************************************************) + +(* + Time-stamp: +*) + + (** 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 + + (** Create a dummy (non-hashconsed) node with a boggus identifer + and hash *) + val dummy : data -> t +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 diff --git a/src/utils/misc.ml b/src/utils/misc.ml index 960ec46..f8156b0 100644 --- a/src/utils/misc.ml +++ b/src/utils/misc.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) (** Various generic signatures and generic module and functor definitions @@ -22,7 +22,7 @@ INCLUDE "utils.ml" module HashSet (H : Hashtbl.HashedType) : - Sigs.AUX.HashSet with type data = H.t = + Common_sig.HashSet with type data = H.t = struct module T = Hashtbl.Make(H) type data = H.t @@ -36,8 +36,8 @@ struct let mem = T.mem end -module Pair (X : Sigs.AUX.Type) (Y : Sigs.AUX.Type) : - Sigs.AUX.Type with type t = X.t * Y.t = +module Pair (X : Common_sig.Type) (Y : Common_sig.Type) : + Common_sig.Type with type t = X.t * Y.t = struct type t = X.t * Y.t let hash (x, y) = HASHINT2(X.hash x, Y.hash y) diff --git a/src/utils/ptset.ml b/src/utils/ptset.ml index 68876d4..3de13bc 100644 --- a/src/utils/ptset.ml +++ b/src/utils/ptset.ml @@ -15,7 +15,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) (* Modified by Kim Nguyen *) @@ -26,10 +26,10 @@ INCLUDE "utils.ml" -include Sigs.PTSET +include Ptset_sig module type HConsBuilder = - functor (H : Sigs.AUX.HashedType) -> Hcons.S with type data = H.t + functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) : S with type elt = H.t = @@ -42,7 +42,7 @@ struct | Branch of int * int * 'a * 'a module rec Node : Hcons.S with type data = Data.t = HCB(Data) - and Data : Sigs.AUX.HashedType with type t = Node.t set = + and Data : Common_sig.HashedType with type t = Node.t set = struct type t = Node.t set let equal x y = diff --git a/src/utils/ptset.mli b/src/utils/ptset.mli index dc80b4a..f4f53f7 100644 --- a/src/utils/ptset.mli +++ b/src/utils/ptset.mli @@ -14,10 +14,10 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) -include module type of Sigs.PTSET +include module type of Ptset_sig module Make (H : Hcons.Abstract) : S with type elt = H.t (** Builds an implementation of hashconsed sets of hashconsed elements. diff --git a/src/utils/ptset_sig.ml b/src/utils/ptset_sig.ml new file mode 100644 index 0000000..f37f6ba --- /dev/null +++ b/src/utils/ptset_sig.ml @@ -0,0 +1,24 @@ +(***********************************************************************) +(* *) +(* 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. *) +(* *) +(***********************************************************************) + +(* + Time-stamp: +*) + +module type S = +sig + include Hcons.S + include Common_sig.Set with type t := t +end diff --git a/src/utils/qName.mli b/src/utils/qName.mli index 4ffaa41..3d6c899 100644 --- a/src/utils/qName.mli +++ b/src/utils/qName.mli @@ -14,13 +14,13 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) (** Implementation of qualified names as hashconsed strings *) -include Sigs.HCONS.S with type data = string -include Sigs.AUX.Printable with type t := t +include Hcons.S with type data = string +include Common_sig.Printable with type t := t val of_string : string -> t diff --git a/src/utils/qNameSet.mli b/src/utils/qNameSet.mli index ae182b6..175ba26 100644 --- a/src/utils/qNameSet.mli +++ b/src/utils/qNameSet.mli @@ -14,17 +14,17 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) (** Implementation of sets of Qualified Names that can be finite or cofinite *) include FiniteCofinite.S with type elt = QName.t -include Sigs.AUX.Printable with type t := t +include Common_sig.Printable with type t := t -module Weak : - sig - include FiniteCofinite.S with type elt = QName.t - include Sigs.AUX.Printable with type t := t - end +module Weak : +sig + include FiniteCofinite.S with type elt = QName.t + include Common_sig.Printable with type t := t +end diff --git a/src/utils/sigs.ml b/src/utils/sigs.ml deleted file mode 100644 index 1022404..0000000 --- a/src/utils/sigs.ml +++ /dev/null @@ -1,237 +0,0 @@ -(***********************************************************************) -(* *) -(* 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. *) -(* *) -(***********************************************************************) - -(* - Time-stamp: -*) - -(** 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 - - (** Create a dummy (non-hashconsed) node with a boggus identifer - and hash *) - val dummy : data -> t - 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 - -module FORMULA = -struct - module type ATOM = - sig - type t - type ctx - val eval : ctx -> t -> bool - val neg : t -> t - include HCONS.S with type t := t - include AUX.Printable with type t := t - end - module type S = - sig - module Atom : ATOM - include HCONS.S - include AUX.Printable with type t := t - val of_bool : bool -> t - val true_ : t - val false_ : t - val or_ : t -> t -> t - val and_ : t -> t -> t - val not_ : t -> t - val diff_ : t -> t -> t - val eval : Atom.ctx -> t -> bool - end - -end -- 2.17.1