X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=finiteCofinite.ml;fp=finiteCofinite.ml;h=32f0e4887a16f45370303f2d34267bf052933b7e;hb=d04661689691b4587cfc45a35e98604fcdc2b878;hp=0000000000000000000000000000000000000000;hpb=f84dd2f6de7d5da16da729dc2e91cbdeb3585d75;p=SXSI%2Fxpathcomp.git diff --git a/finiteCofinite.ml b/finiteCofinite.ml new file mode 100644 index 0000000..32f0e48 --- /dev/null +++ b/finiteCofinite.ml @@ -0,0 +1,183 @@ +(******************************************************************************) +(* SXSI : XPath evaluator *) +(* Kim Nguyen (Kim.Nguyen@nicta.com.au) *) +(* Copyright NICTA 2008 *) +(* Distributed under the terms of the LGPL (see LICENCE) *) +(******************************************************************************) + +exception InfiniteSet +module type S = +sig + type elt + type t + val empty : t + val any : t + val is_empty : t -> bool + val is_any : t -> bool + val is_finite : t -> bool + val kind : t -> [ `Finite | `Cofinite ] + val singleton : elt -> t + val mem : elt -> t -> bool + val add : elt -> t -> t + val remove : elt -> t -> t + val cup : t -> t -> t + val cap : t -> t -> t + val diff : t -> t -> t + val neg : t -> t + val compare : t -> t -> int + val subset : t -> t -> bool + val kind_split : t list -> t * t + 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 from_list : elt list -> t + val choose : t -> elt + val hash : t -> int + val equal : t -> t -> bool +end + +module Make (E : Sigs.Set) : S with type elt = E.elt = +struct + + type elt = E.elt + type t = Finite of E.t | CoFinite of E.t + + + let empty = Finite E.empty + let any = CoFinite E.empty + + let is_empty = function + Finite s when E.is_empty s -> true + | _ -> false + + let is_any = function + CoFinite s when E.is_empty s -> true + | _ -> false + + let is_finite = function + | Finite _ -> true | _ -> false + + let kind = function + Finite _ -> `Finite + | _ -> `Cofinite + + let mem x = function 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 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 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 compare s t = match (s,t) 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 + | 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) + | CoFinite _, Finite _ -> false + + (* given a list l of type t list, + returns two sets (f,c) where : + - f is the union of all the finite sets of l + - c is the union of all the cofinite sets of l + - f and c are disjoint + Invariant : cup f c = List.fold_left cup empty l + + We treat the CoFinite part explicitely : + *) + + 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 + 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 + in + first_cofinite E.empty l + + let fold f t a = match t with + | Finite s -> E.fold f s a + | CoFinite _ -> raise InfiniteSet + + let for_all f = function + | Finite s -> E.for_all f s + | CoFinite _ -> raise InfiniteSet + + let exists f = function + | Finite s -> E.exists f s + | CoFinite _ -> raise InfiniteSet + + let filter f = function + | 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 + | CoFinite _ -> raise InfiniteSet + + let cardinal = function + | Finite s -> E.cardinal s + | CoFinite _ -> raise InfiniteSet + + let elements = function + | 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) + + let choose = function + 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 hash = + function Finite x -> (E.hash x) + | CoFinite x -> ( ~-(E.hash x) land max_int) + +end +