src/finiteCofinite.ml

   1 (******************************************************************************)
   2 (*  SXSI : XPath evaluator                                                    *)
   3 (*  Kim Nguyen (Kim.Nguyen@nicta.com.au)                                      *)
   4 (*  Copyright NICTA 2008                                                      *)
   5 (*  Distributed under the terms of the LGPL (see LICENCE)                     *)
   6 (******************************************************************************)
   7 INCLUDE "utils.ml"
   8
   9 exception InfiniteSet
  10 module type S =
  11 sig
  12   type elt
  13   type t
  14   type set
  15   val empty : t
  16   val any : t
  17   val is_empty : t -> bool
  18   val is_any : t -> bool
  19   val is_finite : t -> bool
  20   val kind : t -> [ `Finite | `Cofinite ]
  21   val singleton : elt -> t
  22   val mem : elt -> t -> bool
  23   val add : elt -> t -> t
  24   val remove : elt -> t -> t
  25   val cup : t -> t -> t
  26   val cap : t -> t -> t
  27   val diff : t -> t -> t
  28   val neg : t -> t
  29   val compare : t -> t -> int
  30   val subset : t -> t -> bool
  31   val kind_split : t list -> t * t
  32   val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
  33   val for_all : (elt -> bool) -> t -> bool
  34   val exists : (elt -> bool) -> t -> bool
  35   val filter : (elt -> bool) -> t -> t
  36   val partition : (elt -> bool) -> t -> t * t
  37   val cardinal : t -> int
  38   val elements : t -> elt list
  39   val from_list : elt list -> t
  40   val choose : t -> elt
  41   val hash : t -> int
  42   val equal : t -> t -> bool
  43   val uid : t -> Uid.t
  44   val positive : t -> set
  45   val negative : t -> set
  46   val inj_positive : set -> t
  47   val inj_negative : set -> t
  48 end
  49
  50 module Make (E : Ptset.S) : S with type elt = E.elt and type set = E.t =
  51 struct
  52
  53   type elt = E.elt
  54   type node = Finite of E.t | CoFinite of E.t
  55   type set = E.t
  56   module Node = Hcons.Make(struct
  57                              type t = node
  58                              let equal a b =
  59                                match a,b with
  60                                   (Finite(s1),Finite(s2))
  61                                  | (CoFinite(s1),CoFinite(s2)) -> E.equal s1 s2
  62                                  | _ -> false
  63                              let hash = function
  64                                Finite (s) -> (E.hash s) lsl 1
  65                              | CoFinite(s) -> ((E.hash s) lsl 1 ) + 1
  66                            end)
  67   type t = Node.t
  68   let empty = Node.make (Finite E.empty)
  69   let any = Node.make (CoFinite E.empty)
  70   let finite x = Node.make (Finite x)
  71   let cofinite x = Node.make (CoFinite x)
  72
  73   let is_empty =  function
  74       { Node.node = Finite s } when E.is_empty s -> true
  75     | _ -> false
  76
  77   let is_any = function
  78       { Node.node = CoFinite s } when E.is_empty s -> true
  79     | _ -> false
  80
  81   let is_finite t = match t.Node.node with
  82     | Finite _ -> true | _ -> false
  83
  84   let kind t = match t.Node.node with
  85       Finite _ -> `Finite
  86     | _ -> `Cofinite
  87
  88   let mem x t = match t.Node.node with
  89     | Finite s -> E.mem x s
  90     | CoFinite s -> not (E.mem x s)
  91
  92   let singleton x = finite (E.singleton x)
  93
  94   let add e t = match t.Node.node with
  95     | Finite s -> finite (E.add e s)
  96     | CoFinite s -> cofinite (E.remove e s)
  97
  98   let remove e t = match t.Node.node with
  99     | Finite s -> finite (E.remove e s)
 100     | CoFinite s -> cofinite (E.add e s)
 101
 102   let cup s t = match (s.Node.node,t.Node.node) with
 103     | Finite s, Finite t -> finite (E.union s t)
 104     | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
 105     | Finite s, CoFinite t -> cofinite (E.diff t s)
 106     | CoFinite s, Finite t-> cofinite (E.diff s t)
 107
 108   let cap s t = match (s.Node.node,t.Node.node) with
 109     | Finite s, Finite t -> finite (E.inter s t)
 110     | CoFinite s, CoFinite t -> cofinite (E.union s t)
 111     | Finite s, CoFinite t -> finite (E.diff s t)
 112     | CoFinite s, Finite t-> finite (E.diff t s)
 113
 114   let diff s t = match (s.Node.node,t.Node.node) with
 115     | Finite s, Finite t -> finite (E.diff s t)
 116     | Finite s, CoFinite t -> finite(E.inter s t)
 117     | CoFinite s, Finite t -> cofinite(E.union t s)
 118     | CoFinite s, CoFinite t -> finite (E.diff t s)
 119
 120   let neg t = match t.Node.node with
 121     | Finite s -> cofinite s
 122     | CoFinite s -> finite s
 123
 124   let compare s t = match (s.Node.node,t.Node.node) with
 125     | Finite s , Finite t -> E.compare s t
 126     | CoFinite s , CoFinite t -> E.compare t s
 127     | Finite _, CoFinite _ -> -1
 128     | CoFinite _, Finite _ -> 1
 129
 130   let subset s t = match (s.Node.node,t.Node.node) with
 131     | Finite s , Finite t -> E.subset s t
 132     | CoFinite s , CoFinite t -> E.subset t s
 133     | Finite s, CoFinite t -> E.is_empty (E.inter s t)
 134     | CoFinite _, Finite _ -> false
 135
 136         (* given a  list l of type t list,
 137            returns two sets (f,c) where :
 138            - f is the union of all the finite sets of l
 139            - c is the union of all the cofinite sets of l
 140            - f and c are disjoint
 141            Invariant : cup f c = List.fold_left cup empty l
 142
 143            We treat the CoFinite part explicitely :
 144         *)
 145
 146   let kind_split l =
 147
 148     let rec next_finite_cofinite facc cacc = function
 149       | [] -> finite facc, cofinite (E.diff cacc facc)
 150       | { Node.node = Finite s } ::r -> next_finite_cofinite (E.union s facc) cacc r
 151       | { Node.node = CoFinite _ } ::r when E.is_empty cacc -> next_finite_cofinite facc cacc r
 152       | { Node.node = CoFinite s } ::r -> next_finite_cofinite facc (E.inter cacc s) r
 153     in
 154     let rec first_cofinite facc = function
 155       | [] -> empty,empty
 156       | { Node.node = Finite s } :: r-> first_cofinite (E.union s facc) r
 157       | { Node.node = CoFinite s } :: r -> next_finite_cofinite facc s r
 158     in
 159       first_cofinite E.empty l
 160
 161   let fold f t a = match t.Node.node with
 162     | Finite s -> E.fold f s a
 163     | CoFinite _ -> raise InfiniteSet
 164
 165   let for_all f t = match t.Node.node with
 166     | Finite s -> E.for_all f s
 167     | CoFinite _ -> raise InfiniteSet
 168
 169   let exists f t = match t.Node.node with
 170     | Finite s -> E.exists f s
 171     | CoFinite _ -> raise InfiniteSet
 172
 173   let filter f t = match t.Node.node with
 174     | Finite s -> finite (E.filter f s)
 175     | CoFinite _ -> raise InfiniteSet
 176
 177   let partition f t = match t.Node.node with
 178     | Finite s -> let a,b = E.partition f s in finite a,finite b
 179     | CoFinite _ -> raise InfiniteSet
 180
 181   let cardinal t = match t.Node.node with
 182     | Finite s -> E.cardinal s
 183     | CoFinite _ -> raise InfiniteSet
 184
 185   let elements t = match t.Node.node with
 186     | Finite s -> E.elements s
 187     | CoFinite _ -> raise InfiniteSet
 188
 189   let from_list l =
 190     finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
 191
 192   let choose t = match t.Node.node with
 193       Finite s -> E.choose s
 194     | _ -> raise InfiniteSet
 195
 196   let equal = (==)
 197
 198   let hash t = t.Node.key
 199
 200   let uid t = t.Node.id
 201
 202
 203   let positive t =
 204     match t.Node.node with
 205       | Finite x -> x
 206       | _ -> E.empty
 207
 208   let negative t =
 209     match t.Node.node with
 210       | CoFinite x -> x
 211       | _ -> E.empty
 212
 213   let inj_positive t = finite t
 214   let inj_negative t = cofinite t
 215 end
 216