From f5d90fb688bc1a9b29815fc33c369856e6c51a67 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Mon, 24 Sep 2012 18:25:40 +0200 Subject: [PATCH] Refactor the code to have a unique place for signature definition. 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. --- HACKING | 3 +- src/finiteCofinite.ml | 34 +++--- src/finiteCofinite.mli | 7 +- src/formula.ml | 34 +++--- src/formula.mli | 21 ++-- src/hcons.ml | 41 ++----- src/hcons.mli | 47 +------- src/ptset.ml | 10 +- src/ptset.mli | 10 +- src/qName.mli | 4 +- src/sigs.ml | 266 ++++++++++++++++++++++++++--------------- src/state.mli | 2 +- src/utils.ml | 7 +- 13 files changed, 249 insertions(+), 237 deletions(-) diff --git a/HACKING b/HACKING index 12ca0e5..5ddab53 100644 --- a/HACKING +++ b/HACKING @@ -1,4 +1,5 @@ -To build: +Building instructions +--------------------- ocamlbuild src/test.native diff --git a/src/finiteCofinite.ml b/src/finiteCofinite.ml index 1c8e6ef..d3d0f13 100644 --- a/src/finiteCofinite.ml +++ b/src/finiteCofinite.ml @@ -14,14 +14,10 @@ (***********************************************************************) 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 = @@ -137,44 +133,46 @@ struct 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 @@ -191,15 +189,15 @@ struct 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 diff --git a/src/finiteCofinite.mli b/src/finiteCofinite.mli index 198e6e2..9b036c4 100644 --- a/src/finiteCofinite.mli +++ b/src/finiteCofinite.mli @@ -16,11 +16,8 @@ (** 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.*) diff --git a/src/formula.ml b/src/formula.ml index f7eae85..1dd0f14 100644 --- a/src/formula.ml +++ b/src/formula.ml @@ -15,18 +15,18 @@ 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" @@ -37,12 +37,13 @@ module rec Node : Hcons.S 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 = @@ -54,7 +55,8 @@ module rec Node : Hcons.S | 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 @@ -62,13 +64,14 @@ let hash x = x.Node.key 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 @@ -85,7 +88,8 @@ let rec print ?(parent=false) ppf f = (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 = diff --git a/src/formula.mli b/src/formula.mli index 46cbe65..9b2659f 100644 --- a/src/formula.mli +++ b/src/formula.mli @@ -18,17 +18,19 @@ 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 @@ -43,8 +45,9 @@ val equal : t -> t -> bool 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 *) diff --git a/src/hcons.ml b/src/hcons.ml index d421d03..a820e08 100644 --- a/src/hcons.ml +++ b/src/hcons.ml @@ -13,45 +13,23 @@ (* *) (***********************************************************************) -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 @@ -68,7 +46,7 @@ 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 @@ -88,9 +66,14 @@ struct 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 diff --git a/src/hcons.mli b/src/hcons.mli index af5618e..6b11bce 100644 --- a/src/hcons.mli +++ b/src/hcons.mli @@ -15,59 +15,18 @@ (** 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 diff --git a/src/ptset.ml b/src/ptset.ml index 9576993..af046a8 100644 --- a/src/ptset.ml +++ b/src/ptset.ml @@ -23,14 +23,10 @@ *) 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 = @@ -43,7 +39,7 @@ struct | 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 = diff --git a/src/ptset.mli b/src/ptset.mli index df38255..28e00d1 100644 --- a/src/ptset.mli +++ b/src/ptset.mli @@ -13,12 +13,8 @@ (* *) (***********************************************************************) -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. @@ -30,5 +26,5 @@ module Weak (H : Hcons.Abstract) : S with type elt = H.t 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 *) diff --git a/src/qName.mli b/src/qName.mli index 36bf022..fa448bc 100644 --- a/src/qName.mli +++ b/src/qName.mli @@ -15,8 +15,8 @@ (** 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 diff --git a/src/sigs.ml b/src/sigs.ml index 3664d4e..dc98baf 100644 --- a/src/sigs.ml +++ b/src/sigs.ml @@ -13,114 +13,190 @@ (* *) (***********************************************************************) -(** 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 diff --git a/src/state.mli b/src/state.mli index ef54518..8c126be 100644 --- a/src/state.mli +++ b/src/state.mli @@ -15,7 +15,7 @@ (** 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 *) diff --git a/src/utils.ml b/src/utils.ml index 2c3772d..1224f2a 100644 --- a/src/utils.ml +++ b/src/utils.ml @@ -17,9 +17,8 @@ *) 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 @@ -33,8 +32,8 @@ struct 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) -- 2.17.1