(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-02-08 13:38:58 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-04 22:52:17 CET by Kim Nguyen>
*)
INCLUDE "utils.ml"
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 =
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 =
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-02-08 18:36:33 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-04 22:47:09 CET by Kim Nguyen>
*)
module type PREDICATE =
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 =
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-01-30 19:07:11 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-04 23:02:21 CET by Kim Nguyen>
*)
(** 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 *)
+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
--- /dev/null
+(***********************************************************************)
+(* *)
+(* 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: <Last modified on 2013-03-04 23:01:55 CET by Kim Nguyen>
+*)
+
+(** 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
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-05 00:35:26 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-05 01:50:21 CET by Kim Nguyen>
*)
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 =
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
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-01-30 19:08:57 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-04 22:44:50 CET by Kim Nguyen>
*)
(** 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.*)
--- /dev/null
+(***********************************************************************)
+(* *)
+(* 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: <Last modified on 2013-03-04 22:44:15 CET by Kim Nguyen>
+*)
+
+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
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-02-06 18:43:46 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-04 22:39:39 CET by Kim Nguyen>
*)
-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;
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-01-30 19:08:42 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-04 23:05:14 CET by Kim Nguyen>
*)
(** 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].
--- /dev/null
+(***********************************************************************)
+(* *)
+(* 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: <Last modified on 2013-03-04 22:36:31 CET by Kim Nguyen>
+*)
+
+ (** 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
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-01-30 19:05:20 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-04 23:00:19 CET by Kim Nguyen>
*)
(** Various generic signatures and generic module and functor definitions
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
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)
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-05 00:37:22 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-05 01:49:52 CET by Kim Nguyen>
*)
(* Modified by Kim Nguyen *)
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 =
| 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 =
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-01-30 19:07:42 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-04 22:42:37 CET by Kim Nguyen>
*)
-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.
--- /dev/null
+(***********************************************************************)
+(* *)
+(* 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: <Last modified on 2013-03-04 23:32:36 CET by Kim Nguyen>
+*)
+
+module type S =
+sig
+ include Hcons.S
+ include Common_sig.Set with type t := t
+end
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-02-14 16:15:23 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-04 22:48:34 CET by Kim Nguyen>
*)
(** 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
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-01-30 19:07:23 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-04 23:03:05 CET by Kim Nguyen>
*)
(** 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
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* 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: <Last modified on 2013-02-05 15:58:13 CET by Kim Nguyen>
-*)
-
-(** 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
projects / tatoo.git / commitdiff