-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
-(* Original file : *)
-
+(* Original file: *)
(***********************************************************************)
(* *)
(* Copyright (C) Jean-Christophe Filliatre *)
(***********************************************************************)
(* Modified by Kim Nguyen *)
-(* The Patricia trees are themselves deeply hashconsed. The module
- provides a Make (and Weak) functor to build hashconsed patricia
- trees whose elements are Abstract hashconsed values. This allows
- to build sets of integers without boxing them in an hacons structure
+(* The Patricia trees are themselves deeply hash-consed. The module
+ provides a Make (and Weak) functor to build hash-consed patricia
+ trees whose elements are Abstract hash-consed values.
*)
+
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 =
match x,y with
- Empty,Empty -> true
+ | Empty,Empty -> true
| Leaf k1, Leaf k2 -> k1 == k2
- | Branch(b1,i1,l1,r1),Branch(b2,i2,l2,r2) ->
- b1 == b2 && i1 == i2 && (Node.equal l1 l2) && (Node.equal r1 r2)
+ | Branch(b1,i1,l1,r1), Branch(b2,i2,l2,r2) ->
+ b1 == b2 && i1 == i2 && (Node.equal l1 l2) && (Node.equal r1 r2)
| _ -> false
let hash = function
- | Empty -> 0
- | Leaf i -> HASHINT2 (PRIME1, Uid.to_int (H.uid i))
- | Branch (b,i,l,r) ->
+ | Empty -> 0
+ | Leaf i -> HASHINT2 (PRIME1, Uid.to_int (H.uid i))
+ | Branch (b,i,l,r) ->
HASHINT4(b, i, Uid.to_int l.Node.id, Uid.to_int r.Node.id)
end
let leaf k = Node.make (Leaf k)
- (* To enforce the invariant that a branch contains two non empty
- sub-trees *)
+ (* To enforce the invariant that a branch contains two non empty
+ sub-trees *)
let branch_ne p m t0 t1 =
if (is_empty t0) then t1
else if is_empty t1 then t0 else branch p m t0 t1
- (******** from here on, only use the smart constructors ************)
+ (******** from here on, only use the smart constructors ************)
let zero_bit k m = (k land m) == 0
let is_singleton n =
match Node.node n with Leaf _ -> true
- | _ -> false
+ | _ -> false
let mem (k:elt) n =
let kid = Uid.to_int (H.uid k) in
let rec loop n = match Node.node n with
- | Empty -> false
- | Leaf j -> k == j
- | Branch (p, _, l, r) -> if kid <= p then loop l else loop r
+ | Empty -> false
+ | Leaf j -> k == j
+ | Branch (p, _, l, r) -> if kid <= p then loop l else loop r
in loop n
let rec min_elt n = match Node.node n with
- | Empty -> raise Not_found
- | Leaf k -> k
- | Branch (_,_,s,_) -> min_elt s
+ | Empty -> raise Not_found
+ | Leaf k -> k
+ | Branch (_,_,s,_) -> min_elt s
let rec max_elt n = match Node.node n with
- | Empty -> raise Not_found
- | Leaf k -> k
- | Branch (_,_,_,t) -> max_elt t
+ | Empty -> raise Not_found
+ | Leaf k -> k
+ | Branch (_,_,_,t) -> max_elt t
let elements s =
let rec elements_aux acc n = match Node.node n with
- | Empty -> acc
- | Leaf k -> k :: acc
- | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
+ | Empty -> acc
+ | Leaf k -> k :: acc
+ | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
in
- elements_aux [] s
+ elements_aux [] s
let mask k m = (k lor (m-1)) land (lnot m)
let rec loop i =
if i = 0 then 1 else if x lsr i = 1 then 1 lsl i else loop (i-1)
in
- loop 7
+ loop 7
let hbit = Array.init 256 naive_highest_bit
-(*
- external clz : int -> int = "caml_clz" "noalloc"
- external leading_bit : int -> int = "caml_leading_bit" "noalloc"
-*)
+ (*
+ external clz : int -> int = "caml_clz" "noalloc"
+ external leading_bit : int -> int = "caml_leading_bit" "noalloc"
+ *)
let highest_bit x =
try
let n = (x) lsr 24 in
if n != 0 then hbit.(n) lsl 24
else let n = (x) lsr 16 in if n != 0 then hbit.(n) lsl 16
- else let n = (x) lsr 8 in if n != 0 then hbit.(n) lsl 8
- else hbit.(x)
+ else let n = (x) lsr 8 in if n != 0 then hbit.(n) lsl 8
+ else hbit.(x)
with
_ -> raise (Invalid_argument ("highest_bit " ^ (string_of_int x)))
let join p0 t0 p1 t1 =
let m = branching_bit p0 p1 in
let msk = mask p0 m in
- if zero_bit p0 m then
- branch_ne msk m t0 t1
- else
- branch_ne msk m t1 t0
+ if zero_bit p0 m then
+ branch_ne msk m t0 t1
+ else
+ branch_ne msk m t1 t0
let match_prefix k p m = (mask k m) == p
let add k t =
let kid = Uid.to_int (H.uid k) in
- assert (kid >=0);
+ assert (kid >=0);
let rec ins n = match Node.node n with
- | Empty -> leaf k
- | Leaf j -> if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n
- | Branch (p,m,t0,t1) ->
+ | Empty -> leaf k
+ | Leaf j -> if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n
+ | Branch (p,m,t0,t1) ->
if match_prefix kid p m then
- if zero_bit kid m then
- branch_ne p m (ins t0) t1
- else
- branch_ne p m t0 (ins t1)
+ if zero_bit kid m then
+ branch_ne p m (ins t0) t1
+ else
+ branch_ne p m t0 (ins t1)
else
- join kid (leaf k) p n
+ join kid (leaf k) p n
in
ins t
let remove k t =
let kid = Uid.to_int(H.uid k) in
let rec rmv n = match Node.node n with
- | Empty -> empty
- | Leaf j -> if k == j then empty else n
- | Branch (p,m,t0,t1) ->
+ | Empty -> empty
+ | Leaf j -> if k == j then empty else n
+ | Branch (p,m,t0,t1) ->
if match_prefix kid p m then
- if zero_bit kid m then
- branch_ne p m (rmv t0) t1
- else
- branch_ne p m t0 (rmv t1)
+ if zero_bit kid m then
+ branch_ne p m (rmv t0) t1
else
- n
+ branch_ne p m t0 (rmv t1)
+ else
+ n
in
rmv t
- (* should run in O(1) thanks to Hash consing *)
+ (* should run in O(1) thanks to Hash consing *)
let equal a b = Node.equal a b
then s
else
match Node.node s, Node.node t with
- | Empty, _ -> t
- | _, Empty -> s
- | Leaf k, _ -> add k t
- | _, Leaf k -> add k s
- | Branch (p,m,s0,s1), Branch (q,n,t0,t1) ->
+ | Empty, _ -> t
+ | _, Empty -> s
+ | Leaf k, _ -> add k t
+ | _, Leaf k -> add k s
+ | Branch (p,m,s0,s1), Branch (q,n,t0,t1) ->
if m == n && match_prefix q p m then
- branch p m (merge s0 t0) (merge s1 t1)
+ branch p m (merge s0 t0) (merge s1 t1)
else if m > n && match_prefix q p m then
- if zero_bit q m then
- branch_ne p m (merge s0 t) s1
- else
- branch_ne p m s0 (merge s1 t)
+ if zero_bit q m then
+ branch_ne p m (merge s0 t) s1
+ else
+ branch_ne p m s0 (merge s1 t)
else if m < n && match_prefix p q n then
- if zero_bit p n then
- branch_ne q n (merge s t0) t1
- else
- branch_ne q n t0 (merge s t1)
+ if zero_bit p n then
+ branch_ne q n (merge s t0) t1
else
- (* The prefixes disagree. *)
- join p s q t
+ branch_ne q n t0 (merge s t1)
+ else
+ (* The prefixes disagree. *)
+ join p s q t
let rec subset s1 s2 = (equal s1 s2) ||
match (Node.node s1,Node.node s2) with
- | Empty, _ -> true
- | _, Empty -> false
- | Leaf k1, _ -> mem k1 s2
- | Branch _, Leaf _ -> false
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+ | Empty, _ -> true
+ | _, Empty -> false
+ | Leaf k1, _ -> mem k1 s2
+ | Branch _, Leaf _ -> false
+ | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then
- subset l1 l2 && subset r1 r2
+ subset l1 l2 && subset r1 r2
else if m1 < m2 && match_prefix p1 p2 m2 then
- if zero_bit p1 m2 then
- subset l1 l2 && subset r1 l2
- else
- subset l1 r2 && subset r1 r2
+ if zero_bit p1 m2 then
+ subset l1 l2 && subset r1 l2
+ else
+ subset l1 r2 && subset r1 r2
else
- false
+ false
let union s1 s2 = merge s1 s2
- (* Todo replace with e Memo Module *)
+ (* Todo replace with e Memo Module *)
let rec inter s1 s2 =
if equal s1 s2
then s1
else
- match (Node.node s1,Node.node s2) with
- | Empty, _ -> empty
- | _, Empty -> empty
- | Leaf k1, _ -> if mem k1 s2 then s1 else empty
- | _, Leaf k2 -> if mem k2 s1 then s2 else empty
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+ match (Node.node s1,Node.node s2) with
+ | Empty, _ -> empty
+ | _, Empty -> empty
+ | Leaf k1, _ -> if mem k1 s2 then s1 else empty
+ | _, Leaf k2 -> if mem k2 s1 then s2 else empty
+ | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then
- merge (inter l1 l2) (inter r1 r2)
+ merge (inter l1 l2) (inter r1 r2)
else if m1 > m2 && match_prefix p2 p1 m1 then
- inter (if zero_bit p2 m1 then l1 else r1) s2
+ inter (if zero_bit p2 m1 then l1 else r1) s2
else if m1 < m2 && match_prefix p1 p2 m2 then
- inter s1 (if zero_bit p1 m2 then l2 else r2)
+ inter s1 (if zero_bit p1 m2 then l2 else r2)
else
- empty
+ empty
let rec diff s1 s2 =
if equal s1 s2
then empty
else
- match (Node.node s1,Node.node s2) with
- | Empty, _ -> empty
- | _, Empty -> s1
- | Leaf k1, _ -> if mem k1 s2 then empty else s1
- | _, Leaf k2 -> remove k2 s1
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+ match (Node.node s1,Node.node s2) with
+ | Empty, _ -> empty
+ | _, Empty -> s1
+ | Leaf k1, _ -> if mem k1 s2 then empty else s1
+ | _, Leaf k2 -> remove k2 s1
+ | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then
- merge (diff l1 l2) (diff r1 r2)
+ merge (diff l1 l2) (diff r1 r2)
else if m1 > m2 && match_prefix p2 p1 m1 then
- if zero_bit p2 m1 then
- merge (diff l1 s2) r1
- else
- merge l1 (diff r1 s2)
+ if zero_bit p2 m1 then
+ merge (diff l1 s2) r1
+ else
+ merge l1 (diff r1 s2)
else if m1 < m2 && match_prefix p1 p2 m2 then
- if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
+ if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
else
- s1
+ s1
-(*s All the following operations ([cardinal], [iter], [fold], [for_all],
+ (*s All the following operations ([cardinal], [iter], [fold], [for_all],
[exists], [filter], [partition], [choose], [elements]) are
implemented as for any other kind of binary trees. *)
-let rec cardinal n = match Node.node n with
+ let rec cardinal n = match Node.node n with
| Empty -> 0
| Leaf _ -> 1
| Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
-let rec iter f n = match Node.node n with
+ let rec iter f n = match Node.node n with
| Empty -> ()
| Leaf k -> f k
| Branch (_,_,t0,t1) -> iter f t0; iter f t1
-let rec fold f s accu = match Node.node s with
+ let rec fold f s accu = match Node.node s with
| Empty -> accu
| Leaf k -> f k accu
| Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
-let rec for_all p n = match Node.node n with
+ let rec for_all p n = match Node.node n with
| Empty -> true
| Leaf k -> p k
| Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1
-let rec exists p n = match Node.node n with
+ let rec exists p n = match Node.node n with
| Empty -> false
| Leaf k -> p k
| Branch (_,_,t0,t1) -> exists p t0 || exists p t1
-let rec filter pr n = match Node.node n with
+ let rec filter pr n = match Node.node n with
| Empty -> empty
| Leaf k -> if pr k then n else empty
| Branch (p,m,t0,t1) -> branch_ne p m (filter pr t0) (filter pr t1)
-let partition p s =
- let rec part (t,f as acc) n = match Node.node n with
+ let partition p s =
+ let rec part (t,f as acc) n = match Node.node n with
| Empty -> acc
| Leaf k -> if p k then (add k t, f) else (t, add k f)
| Branch (_,_,t0,t1) -> part (part acc t0) t1
- in
- part (empty, empty) s
+ in
+ part (empty, empty) s
-let rec choose n = match Node.node n with
+ let rec choose n = match Node.node n with
| Empty -> raise Not_found
| Leaf k -> k
| Branch (_, _,t0,_) -> choose t0 (* we know that [t0] is non-empty *)
-let split x s =
- let coll k (l, b, r) =
- if k < x then add k l, b, r
- else if k > x then l, b, add k r
- else l, true, r
- in
- fold coll s (empty, false, empty)
-
-(*s Additional functions w.r.t to [Set.S]. *)
-
-let rec intersect s1 s2 = (equal s1 s2) ||
- match (Node.node s1,Node.node s2) with
- | Empty, _ -> false
- | _, Empty -> false
- | Leaf k1, _ -> mem k1 s2
- | _, Leaf k2 -> mem k2 s1
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
+ let split x s =
+ let coll k (l, b, r) =
+ if k < x then add k l, b, r
+ else if k > x then l, b, add k r
+ else l, true, r
+ in
+ fold coll s (empty, false, empty)
+
+ (*s Additional functions w.r.t to [Set.S]. *)
+
+ let rec intersect s1 s2 = (equal s1 s2) ||
+ match (Node.node s1,Node.node s2) with
+ | Empty, _ -> false
+ | _, Empty -> false
+ | Leaf k1, _ -> mem k1 s2
+ | _, Leaf k2 -> mem k2 s1
+ | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+ if m1 == m2 && p1 == p2 then
intersect l1 l2 || intersect r1 r2
- else if m1 < m2 && match_prefix p2 p1 m1 then
+ else if m1 < m2 && match_prefix p2 p1 m1 then
intersect (if zero_bit p2 m1 then l1 else r1) s2
- else if m1 > m2 && match_prefix p1 p2 m2 then
+ else if m1 > m2 && match_prefix p1 p2 m2 then
intersect s1 (if zero_bit p1 m2 then l2 else r2)
- else
+ else
false
-let from_list l = List.fold_left (fun acc e -> add e acc) empty l
+ let from_list l = List.fold_left (fun acc e -> add e acc) empty l
end
module PosInt
=
- struct
- include Make(Hcons.PosInt)
- let print ppf s =
- Format.pp_print_string ppf "{ ";
- iter (fun i -> Format.fprintf ppf "%i " i) s;
- Format.pp_print_string ppf "}";
- Format.pp_print_flush ppf ()
- end
+struct
+ include Make(Hcons.PosInt)
+ let print ppf s =
+ Format.pp_print_string ppf "{ ";
+ iter (fun i -> Format.fprintf ppf "%i " i) s;
+ Format.pp_print_string ppf "}";
+ Format.pp_print_flush ppf ()
+end
(* *)
(***********************************************************************)
-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