(***********************************************************************) (* *) (* TAToo *) (* *) (* Kim Nguyen, LRI UMR8623 *) (* Université Paris-Sud & CNRS *) (* *) (* Copyright 2010-2012 Université Paris-Sud and Centre National de la *) (* Recherche Scientifique. All rights reserved. This file is *) (* distributed under the terms of the GNU Lesser General Public *) (* License, with the special exception on linking described in file *) (* ../LICENSE. *) (* *) (***********************************************************************) (* Time-stamp: *) INCLUDE "utils.ml" include FiniteCofinite_sig module type HConsBuilder = functor (H : Common_sig.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 = struct type elt = E.elt type node = Finite of E.t | CoFinite of E.t type set = E.t module Node = HCB(struct type t = node let equal a b = match a, b with Finite s1, Finite s2 | CoFinite s1, CoFinite s2 -> E.equal s1 s2 | (Finite _| CoFinite _), _ -> false let hash = function | Finite s -> HASHINT2 (PRIME1, E.hash s) | CoFinite s -> HASHINT2 (PRIME3, E.hash s) end) include Node let empty = make (Finite E.empty) let any = make (CoFinite E.empty) let finite x = make (Finite x) let cofinite x = make (CoFinite x) let is_empty t = match t.node with | Finite s -> E.is_empty s | CoFinite _ -> false let is_any t = match t.node with | CoFinite s -> E.is_empty s | Finite _ -> false let is_finite t = match t.node with | Finite _ -> true | CoFinite _ -> false let kind t = match t.node with | Finite _ -> `Finite | CoFinite _ -> `Cofinite let mem x t = match t.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 t = match t.node with | Finite s -> finite (E.add e s) | CoFinite s -> cofinite (E.remove e s) let remove e t = match t.node with | Finite s -> finite (E.remove e s) | CoFinite s -> cofinite (E.add e s) let union s t = match s.node, t.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 inter s t = match s.node, t.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.node, t.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 complement t = match t.node with | Finite s -> cofinite s | CoFinite s -> finite s let compare s t = match s.node, t.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.node, t.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) | 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) | { node = Finite s; _ } ::r -> next_finite_cofinite (E.union s facc) cacc r | { node = CoFinite _ ; _ } ::r when E.is_empty cacc -> next_finite_cofinite facc cacc r | { node = CoFinite s; _ } ::r -> next_finite_cofinite facc (E.inter cacc s) r in let rec first_cofinite facc = function | [] -> empty,empty | { node = Finite s ; _ } :: r-> first_cofinite (E.union s facc) r | { node = CoFinite s ; _ } :: r -> next_finite_cofinite facc s r in first_cofinite E.empty l let exn = FiniteCofinite_sig.InfiniteSet let fold f t a = match t.node with | Finite s -> E.fold f s a | CoFinite _ -> raise exn let iter f t = match t.node with | Finite t -> E.iter f t | CoFinite _ -> raise exn let for_all f t = match t.node with | Finite s -> E.for_all f s | CoFinite _ -> raise exn let exists f t = match t.node with | Finite s -> E.exists f s | CoFinite _ -> raise exn let filter f t = match t.node with | Finite s -> finite (E.filter f s) | 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 exn let cardinal t = match t.node with | Finite s -> E.cardinal s | CoFinite _ -> raise exn let elements t = match t.node with | Finite s -> E.elements s | 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 | CoFinite _ -> raise exn let is_singleton t = match t.node with | Finite s -> E.is_singleton s | CoFinite _ -> false let intersect s t = match s.node, t.node with | Finite s, Finite t -> E.intersect s t | CoFinite s, Finite t -> not (E.subset t s) | Finite s, CoFinite t -> not (E.subset s t) | CoFinite _ , CoFinite _ -> true let split x s = match s.node with | Finite s -> let s1, b, s2 = E.split x s in finite s1, b, finite s2 | CoFinite _ -> raise exn let min_elt s = match s.node with | Finite s -> E.min_elt s | CoFinite _ -> raise exn let max_elt s = match s.node with | Finite s -> E.min_elt s | CoFinite _ -> raise exn let positive t = match t.node with | Finite x -> x | CoFinite _ -> E.empty let negative t = match t.node with | CoFinite x -> x | Finite _ -> E.empty let inj_positive t = finite t let inj_negative t = cofinite t end module Make = Builder(Hcons.Make) module Weak = Builder(Hcons.Weak)