src/finiteCofinite.ml

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