(* Copyright NICTA 2008 *)
(* Distributed under the terms of the LGPL (see LICENCE) *)
(******************************************************************************)
+INCLUDE "utils.ml"
exception InfiniteSet
module type S =
val choose : t -> elt
val hash : t -> int
val equal : t -> t -> bool
+ val uid : t -> Uid.t
val positive : t -> set
val negative : t -> set
+ val inj_positive : set -> t
+ val inj_negative : set -> t
end
-module Make (E : Sigs.Set) : S with type elt = E.elt and type set = E.t =
+module Make (E : Ptset.S) : S with type elt = E.elt and type set = E.t =
struct
type elt = E.elt
- type t = Finite of E.t | CoFinite of E.t
+ type node = Finite of E.t | CoFinite of E.t
type set = E.t
-
- let empty = Finite E.empty
- let any = CoFinite E.empty
+ module Node = Hcons.Make(struct
+ type t = node
+ let equal a b =
+ match a,b with
+ (Finite(s1),Finite(s2))
+ | (CoFinite(s1),CoFinite(s2)) -> E.equal s1 s2
+ | _ -> false
+ let hash = function
+ Finite (s) -> (E.hash s) lsl 1
+ | CoFinite(s) -> ((E.hash s) lsl 1 ) lor 1
+ end)
+ type t = Node.t
+ let empty = Node.make (Finite E.empty)
+ let any = Node.make (CoFinite E.empty)
+ let finite x = Node.make (Finite x)
+ let cofinite x = Node.make (CoFinite x)
let is_empty = function
- Finite s when E.is_empty s -> true
+ { Node.node = Finite s } when E.is_empty s -> true
| _ -> false
let is_any = function
- CoFinite s when E.is_empty s -> true
+ { Node.node = CoFinite s } when E.is_empty s -> true
| _ -> false
- let is_finite = function
+ let is_finite t = match t.Node.node with
| Finite _ -> true | _ -> false
- let kind = function
+ let kind t = match t.Node.node with
Finite _ -> `Finite
| _ -> `Cofinite
- let mem x = function Finite s -> E.mem x s
+ let mem x t = match t.Node.node with
+ | Finite s -> E.mem x s
| CoFinite s -> not (E.mem x s)
- let singleton x = Finite (E.singleton x)
- let add e = function
- | Finite s -> Finite (E.add e s)
- | CoFinite s -> CoFinite (E.remove e s)
- let remove e = function
- | Finite s -> Finite (E.remove e s)
- | CoFinite s -> CoFinite (E.add e s)
+ let singleton x = finite (E.singleton x)
+
+ let add e t = match t.Node.node with
+ | Finite s -> finite (E.add e s)
+ | CoFinite s -> cofinite (E.remove e s)
+
+ let remove e t = match t.Node.node with
+ | Finite s -> finite (E.remove e s)
+ | CoFinite s -> cofinite (E.add e s)
- let cup s t = match (s,t) with
- | Finite s, Finite t -> Finite (E.union s t)
- | CoFinite s, CoFinite t -> CoFinite ( E.inter s t)
- | Finite s, CoFinite t -> CoFinite (E.diff t s)
- | CoFinite s, Finite t-> CoFinite (E.diff s t)
-
- let cap s t = match (s,t) with
- | Finite s, Finite t -> Finite (E.inter s t)
- | CoFinite s, CoFinite t -> CoFinite (E.union s t)
- | Finite s, CoFinite t -> Finite (E.diff s t)
- | CoFinite s, Finite t-> Finite (E.diff t s)
+ let cup s t = match (s.Node.node,t.Node.node) with
+ | Finite s, Finite t -> finite (E.union s t)
+ | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
+ | Finite s, CoFinite t -> cofinite (E.diff t s)
+ | CoFinite s, Finite t-> cofinite (E.diff s t)
+
+ let cap s t = match (s.Node.node,t.Node.node) with
+ | Finite s, Finite t -> finite (E.inter s t)
+ | CoFinite s, CoFinite t -> cofinite (E.union s t)
+ | Finite s, CoFinite t -> finite (E.diff s t)
+ | CoFinite s, Finite t-> finite (E.diff t s)
- let diff s t = match (s,t) with
- | Finite s, Finite t -> Finite (E.diff s t)
- | Finite s, CoFinite t -> Finite(E.inter s t)
- | CoFinite s, Finite t -> CoFinite(E.union t s)
- | CoFinite s, CoFinite t -> Finite (E.diff t s)
-
- let neg = function
- | Finite s -> CoFinite s
- | CoFinite s -> Finite s
+ let diff s t = match (s.Node.node,t.Node.node) with
+ | Finite s, Finite t -> finite (E.diff s t)
+ | Finite s, CoFinite t -> finite(E.inter s t)
+ | CoFinite s, Finite t -> cofinite(E.union t s)
+ | CoFinite s, CoFinite t -> finite (E.diff t s)
+
+ let neg t = match t.Node.node with
+ | Finite s -> cofinite s
+ | CoFinite s -> finite s
- let compare s t = match (s,t) with
+ let compare s t = match (s.Node.node,t.Node.node) with
| Finite s , Finite t -> E.compare s t
| CoFinite s , CoFinite t -> E.compare t s
| Finite _, CoFinite _ -> -1
| CoFinite _, Finite _ -> 1
- let subset s t = match (s,t) with
+ let subset s t = match (s.Node.node,t.Node.node) with
| Finite s , Finite t -> E.subset s t
| CoFinite s , CoFinite t -> E.subset t s
| Finite s, CoFinite t -> E.is_empty (E.inter s t)
let kind_split l =
let rec next_finite_cofinite facc cacc = function
- | [] -> Finite facc, CoFinite (E.diff cacc facc)
- | Finite s ::r -> next_finite_cofinite (E.union s facc) cacc r
- | CoFinite _ ::r when E.is_empty cacc -> next_finite_cofinite facc cacc r
- | CoFinite s ::r -> next_finite_cofinite facc (E.inter cacc s) r
+ | [] -> finite facc, cofinite (E.diff cacc facc)
+ | { Node.node = Finite s } ::r -> next_finite_cofinite (E.union s facc) cacc r
+ | { Node.node = CoFinite _ } ::r when E.is_empty cacc -> next_finite_cofinite facc cacc r
+ | { Node.node = CoFinite s } ::r -> next_finite_cofinite facc (E.inter cacc s) r
in
let rec first_cofinite facc = function
| [] -> empty,empty
- | Finite s :: r-> first_cofinite (E.union s facc) r
- | CoFinite s :: r -> next_finite_cofinite facc s r
+ | { Node.node = Finite s } :: r-> first_cofinite (E.union s facc) r
+ | { Node.node = CoFinite s } :: r -> next_finite_cofinite facc s r
in
first_cofinite E.empty l
- let fold f t a = match t with
+ let fold f t a = match t.Node.node with
| Finite s -> E.fold f s a
| CoFinite _ -> raise InfiniteSet
- let for_all f = function
+ let for_all f t = match t.Node.node with
| Finite s -> E.for_all f s
| CoFinite _ -> raise InfiniteSet
- let exists f = function
+ let exists f t = match t.Node.node with
| Finite s -> E.exists f s
| CoFinite _ -> raise InfiniteSet
- let filter f = function
- | Finite s -> Finite (E.filter f s)
+ let filter f t = match t.Node.node with
+ | Finite s -> finite (E.filter f s)
| CoFinite _ -> raise InfiniteSet
- let partition f = function
- | Finite s -> let a,b = E.partition f s in Finite a,Finite b
+ let partition f t = match t.Node.node with
+ | Finite s -> let a,b = E.partition f s in finite a,finite b
| CoFinite _ -> raise InfiniteSet
- let cardinal = function
+ let cardinal t = match t.Node.node with
| Finite s -> E.cardinal s
| CoFinite _ -> raise InfiniteSet
- let elements = function
+ let elements t = match t.Node.node with
| Finite s -> E.elements s
| CoFinite _ -> raise InfiniteSet
let from_list l =
- Finite(List.fold_left (fun x a -> E.add a x ) E.empty l)
+ finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
- let choose = function
+ let choose t = match t.Node.node with
Finite s -> E.choose s
| _ -> raise InfiniteSet
- let equal a b =
- match a,b with
- | Finite x, Finite y | CoFinite x, CoFinite y -> E.equal x y
- | _ -> false
+ let equal = (==)
+
+ let hash t = t.Node.key
- let hash =
- function Finite x -> (E.hash x)
- | CoFinite x -> ( ~-(E.hash x) land max_int)
+ let uid t = t.Node.id
+
- let positive =
- function
+ let positive t =
+ match t.Node.node with
| Finite x -> x
| _ -> E.empty
- let negative =
- function
+ let negative t =
+ match t.Node.node with
| CoFinite x -> x
| _ -> E.empty
+ let inj_positive t = finite t
+ let inj_negative t = cofinite t
end