Re-architecture the code to have all signatures in the sigs.ml module.
Any signature which occurs at least twice in the code (e.g. in a.ml
and corresponding a.mli) is put in a module A in Sigs. The signature
can the be included in a.ml and its 'module type of' can be included
in a.mli.
private signatures can stay in the .ml files where they appear.
-To build:
+Building instructions
+---------------------
ocamlbuild src/test.native
(***********************************************************************)
INCLUDE "utils.ml"
-module type S =
- sig
- include Sigs.FiniteCofiniteSet
- include Hcons.S with type t := t
- end
+include Sigs.FINITECOFINITE
module type HConsBuilder =
- functor (H : Sigs.HashedType) -> Hcons.S with type data = H.t
+ functor (H : Sigs.AUX.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 fold f t a = match t.node with
| Finite s -> E.fold f s a
- | CoFinite _ -> raise Sigs.InfiniteSet
+ | CoFinite _ -> raise exn
let iter f t = match t.node with
| Finite t -> E.iter f t
- | CoFinite _ -> raise Sigs.InfiniteSet
+ | CoFinite _ -> raise exn
let for_all f t = match t.node with
| Finite s -> E.for_all f s
- | CoFinite _ -> raise Sigs.InfiniteSet
+ | CoFinite _ -> raise exn
let exists f t = match t.node with
| Finite s -> E.exists f s
- | CoFinite _ -> raise Sigs.InfiniteSet
+ | CoFinite _ -> raise exn
let filter f t = match t.node with
| Finite s -> finite (E.filter f s)
- | CoFinite _ -> raise Sigs.InfiniteSet
+ | CoFinite _ -> raise exn
let partition f t = match t.node with
| Finite s -> let a,b = E.partition f s in finite a,finite b
- | CoFinite _ -> raise Sigs.InfiniteSet
+ | CoFinite _ -> raise exn
let cardinal t = match t.node with
| Finite s -> E.cardinal s
- | CoFinite _ -> raise Sigs.InfiniteSet
+ | CoFinite _ -> raise exn
let elements t = match t.node with
| Finite s -> E.elements s
- | CoFinite _ -> raise Sigs.InfiniteSet
+ | CoFinite _ -> raise exn
let from_list l =
finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
let choose t = match t.node with
Finite s -> E.choose s
- | _ -> raise Sigs.InfiniteSet
+ | _ -> raise exn
let is_singleton t = match t.node with
| Finite s -> E.is_singleton s
let s1, b, s2 = E.split x s in
finite s1, b, finite s2
- | _ -> raise Sigs.InfiniteSet
+ | _ -> raise exn
let min_elt s = match s.node with
| Finite s -> E.min_elt s
- | _ -> raise Sigs.InfiniteSet
+ | _ -> raise exn
let max_elt s = match s.node with
| Finite s -> E.min_elt s
- | _ -> raise Sigs.InfiniteSet
+ | _ -> raise exn
let positive t =
match t.node with
(** Implementation of hashconsed finite or cofinite sets.
*)
-module type S =
-sig
- include Sigs.FiniteCofiniteSet
- include Hcons.S with type t := t
-end
+include module type of Sigs.FINITECOFINITE
+
(** Output signature of the {!FiniteCofinite.Make} and
{!FiniteCofinite.Weak} functors.*)
INCLUDE "utils.ml"
open Format
-type move = [ `Left | `Right ]
-type 'hcons expr =
- | False | True
- | Or of 'hcons * 'hcons
- | And of 'hcons * 'hcons
- | Atom of (move * bool * State.t)
+type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
+type 'formula expr =
+ | False
+ | True
+ | Or of 'formula * 'formula
+ | And of 'formula * 'formula
+ | Move of (move * bool * State.t)
+ | Label of QNameSet.t
type 'hcons node = {
pos : 'hcons expr;
mutable neg : 'hcons;
- st : StateSet.t * StateSet.t;
- size: int; (* Todo check if this is needed *)
}
external hash_const_variant : [> ] -> int = "%identity"
and Data : Hashtbl.HashedType with type t = Node.t node =
struct
type t = Node.t node
- let equal x y = x.size == y.size &&
+ let equal x y = (*x.size == y.size &&*)
match x.pos, y.pos with
| a,b when a == b -> true
| Or(xf1, xf2), Or(yf1, yf2)
| And(xf1, xf2), And(yf1,yf2) -> (xf1 == yf1) && (xf2 == yf2)
- | Atom(d1, p1, s1), Atom(d2 ,p2 ,s2) -> d1 == d2 && p1 == p2 && s1 == s2
+ | Move(d1, p1, s1), Move(d2 ,p2 ,s2) -> d1 == d2 && p1 == p2 && s1 == s2
+ | Label s1, Label s2 -> s1 == s2
| _ -> false
let hash f =
| And (f1, f2) ->
HASHINT3(PRIME3, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
- | Atom(d, p, s) -> HASHINT4(PRIME5, hash_const_variant d,vb p,s)
+ | Move(d, p, s) -> HASHINT4(PRIME5, hash_const_variant d,vb p,s)
+ | Label s -> HASHINT2(PRIME7, Uid.to_int s.QNameSet.id)
end
type t = Node.t
let uid x = x.Node.id
let equal = Node.equal
let expr f = f.Node.node.pos
-let st f = f.Node.node.st
-let size f = f.Node.node.size
+(*let st f = f.Node.node.st*)
+(*let size f = f.Node.node.size*)
let compare f1 f2 = compare f1.Node.id f2.Node.id
let prio f =
match expr f with
| True | False -> 10
- | Atom _ -> 8
+ | Move _ -> 8
+ | Label _ -> 7
| And _ -> 6
| Or _ -> 1
(print ppf f1);
fprintf ppf " %s " Pretty.vee;
(print ppf f2);
- | Atom(dir, b, s) ->
+ | Label s -> fprintf ppf "%a" QNameSet.print s
+ | Move(dir, b, s) ->
let _ = flush_str_formatter() in
let fmt = str_formatter in
let a_str, d_str =
type move = [ `Left |`Right ]
(** Direction for automata predicates *)
-type 'hcons expr =
- False
- | True
- | Or of 'hcons * 'hcons
- | And of 'hcons * 'hcons
- | Atom of (move * bool * State.t)
-
-(** Partial internal representation of a formula,
+type 'formula expr =
+ | False
+ | True
+ | Or of 'formula * 'formula
+ | And of 'formula * 'formula
+ | Move of (move * bool * State.t)
+ | Label of QNameSet.t
+
+(** View of the internal representation of a formula,
used for pattern matching *)
type t
+
(** Abstract type representing hashconsed formulae *)
val hash : t -> int
val expr : t -> t expr
(** Equality over formulae *)
-val st : t -> StateSet.t * StateSet.t
+(*val st : t -> StateSet.t * StateSet.t
(** states occuring left and right, positively or negatively *)
+*)
val compare : t -> t -> int
(** Comparison of formulae *)
(* *)
(***********************************************************************)
-module type Abstract =
- sig
- type data
- type t
- val make : data -> t
- val node : t -> data
- val hash : t -> int
- val uid : t -> Uid.t
- val equal : t -> t -> bool
- val init : unit -> unit
- end
-
-type 'a node = { id : Uid.t;
- key : int;
- node : 'a }
-module type S =
-sig
- type data
- type t = private { id : Uid.t;
- key : int;
- node : data }
- include Abstract with type data := data and type t := t
-end
+include Sigs.HCONS
module type TableBuilder =
functor
- (H : Sigs.HashedType) ->
- Sigs.HashSet with type data = H.t
+ (H : Sigs.AUX.HashedType) ->
+ Sigs.AUX.HashSet with type data = H.t
-module Builder (TB : TableBuilder) (H : Sigs.HashedType) =
+module Builder (TB : TableBuilder) (H : Sigs.AUX.HashedType) =
struct
type data = H.t
type t = { id : Uid.t;
- key : int;
+ hash : int;
node : data }
let uid_make = ref (Uid.make_maker())
let node t = t.node
let uid t = t.id
- let hash t = t.key
+ let hash t = t.hash
let equal t1 t2 = t1 == t2
module HN =
struct
uid_make := Uid.make_maker ()
let make x =
- let cell = { id = Uid.dummy; key = H.hash x; node = x } in
+ let cell = { id = Uid.dummy; hash = H.hash x; node = x } in
try
T.find pool cell
with
let make v =
if v < 0 then raise (Invalid_argument "Hcons.PosInt.make")
else v
+
let node v = v
+
let hash v = v
+
let uid v = Uid.of_int v
+
let equal x y = x == y
+
let init () = ()
end
(** Implementation of generic hashconsing. *)
-module type Abstract =
- sig
- type data
- (** The type of the data to be hashconsed *)
-
- type t
- (** The type of hashconsed data *)
-
- val make : data -> t
- (** [make v] internalizes the value [v], making it an hashconsed
- value.
- *)
-
- val node : t -> data
- (** [node h] extract the original data from its hashconsed value
- *)
-
- val hash : t -> int
- (** [hash h] returns a hash of [h], such that for every [h1] and
- [h2], [equal h1 h2] implies [hash h1 = hash h2].
- *)
-
- val uid : t -> Uid.t
- (** [uid h] returns a unique identifier *)
- val equal : t -> t -> bool
- (** Equality between hashconsed values. Equivalent to [==] *)
-
- val init : unit -> unit
- (** Initializes the internal storage. Any previously hashconsed
- element is discarded. *)
-
- end
-(** Abstract signature of a module implementing an hashconsed datatype *)
-
-module type S =
-sig
- type data
- type t = private { id : Uid.t;
- key : int;
- node : data }
- include Abstract with type data := data and type t := t
-end
+include module type of Sigs.HCONS
(** Output signature of the functor {!Hcons.Make} *)
-module Make (H : Sigs.HashedType) : S with type data = H.t
+module Make (H : Sigs.AUX.HashedType) : S with type data = H.t
(** Functor building an implementation of hashconsed values for a given
implementation of {!Sigs.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.HashedType) : S with type data = H.t
+module Weak (H : Sigs.AUX.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
weak semantics: they may be reclaimed as soon as no external
*)
INCLUDE "utils.ml"
-module type S =
- sig
- include Sigs.Set
- include Hcons.S with type t := t
- end
+include Sigs.PTSET
module type HConsBuilder =
- functor (H : Sigs.HashedType) -> Hcons.S with type data = H.t
+ functor (H : Sigs.AUX.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.HashedType with type t = Node.t set =
+ and Data : Sigs.AUX.HashedType with type t = Node.t set =
struct
type t = Node.t set
let equal x y =
(* *)
(***********************************************************************)
-module type S =
- sig
- include Sigs.Set
- include Hcons.S with type t := t
- end
-(** Output signature of the {!Ptset.Make} and {!Ptset.Weak} functors. *)
+
+include module type of Sigs.PTSET
module Make (H : Hcons.Abstract) : S with type elt = H.t
(** Builds an implementation of hashconsed sets of hashconsed elements.
with weak internal storage. See {!Hcons.Weak}.
*)
-module PosInt : Sigs.Set with type elt = int
+module PosInt : S with type elt = int
(** Implementation of hashconsed sets of positive integers *)
(** Implementation of qualified names as hashconsed strings *)
-include Hcons.S with type data = string
-include Sigs.Printable with type t := t
+include Sigs.HCONS.S with type data = string
+include Sigs.AUX.Printable with type t := t
val of_string : string -> t
(* *)
(***********************************************************************)
-(** Various generic signatures *)
-
-module type HashedType =
-sig
- type t
- val hash : t -> int
- (** [hash v] returns an integer in the range
- [ 0 - 2^30-1 ]
- *)
- val equal : t -> t -> bool
- (** Equality *)
-end
-(** Type equipped with an equality and hash function.
- If [equal a b] then [(hash a) = (hash b)]
+(** 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.
*)
-module type OrderedType =
-sig
- type t
- val compare : t -> t -> int
- (** 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].
+(** 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 ]
*)
-end
-(** Type equiped with a total ordering *)
+ val hash : t -> int
-module type Printable =
-sig
- type t
- val print : Format.formatter -> t -> unit
-end
- (** Type equiped with a pretty-printer *)
+ (** 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
-module type Type =
-sig
- type t
- include HashedType with type t := t
- include OrderedType with type t := t
-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
-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
+ (** 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
-(** Signature of a simple HashSet 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
+
+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
-exception InfiniteSet
-
-module type FiniteCofiniteSet =
-sig
- include Set
- 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
+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
(** Implementation of states *)
-include Sigs.Type with type t = int
+include Sigs.AUX.Type with type t = int
val make : unit -> t
(** Generate a fresh state *)
*)
INCLUDE "utils.ml"
-
module HashSet (H : Hashtbl.HashedType) :
- Sigs.HashSet with type data = H.t =
+ Sigs.AUX.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.Type) (Y : Sigs.Type) :
- Sigs.Type with type t = X.t * Y.t =
+module Pair (X : Sigs.AUX.Type) (Y : Sigs.AUX.Type) :
+ Sigs.AUX.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)
projects / tatoo.git / commitdiff