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
  16 INCLUDE "utils.ml"
  17
  18 include FiniteCofinite_sig
  19
  20 module type HConsBuilder =
  21   functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
  22
  23 module Builder (HCB : HConsBuilder) (E : Ptset.S) :
  24   S with type elt = E.elt and type set = E.t =
  25 struct
  26   type elt = E.elt
  27   type node = Finite of E.t | CoFinite of E.t
  28   type set = E.t
  29   module Node = HCB(struct
  30     type t = node
  31     let equal a b =
  32       match a, b with
  33         Finite s1, Finite s2
  34       | CoFinite s1, CoFinite s2 -> E.equal s1 s2
  35       | (Finite _| CoFinite _), _ -> false
  36
  37     let hash = function
  38       | Finite s -> HASHINT2 (PRIME1, E.hash s)
  39       | CoFinite s -> HASHINT2 (PRIME3, E.hash s)
  40   end)
  41   include Node
  42   let empty = make (Finite E.empty)
  43   let any = make (CoFinite E.empty)
  44   let finite x = make (Finite x)
  45   let cofinite x = make (CoFinite x)
  46
  47   let is_empty t =  match t.node with
  48     | Finite s -> E.is_empty s
  49     | CoFinite _  -> false
  50
  51   let is_any t = match t.node with
  52     | CoFinite s -> E.is_empty s
  53     | Finite _  -> false
  54
  55   let is_finite t = match t.node with
  56     | Finite _ -> true
  57     | CoFinite _ -> false
  58
  59   let kind t = match t.node with
  60     | Finite _ -> `Finite
  61     | CoFinite _  -> `Cofinite
  62
  63   let mem x t = match t.node with
  64     | Finite s -> E.mem x s
  65     | CoFinite s -> not (E.mem x s)
  66
  67   let singleton x = finite (E.singleton x)
  68
  69   let add e t = match t.node with
  70     | Finite s -> finite (E.add e s)
  71     | CoFinite s -> cofinite (E.remove e s)
  72
  73   let remove e t = match t.node with
  74     | Finite s -> finite (E.remove e s)
  75     | CoFinite s -> cofinite (E.add e s)
  76
  77   let union s t = match s.node, t.node with
  78     | Finite s, Finite t -> finite (E.union s t)
  79     | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
  80     | Finite s, CoFinite t -> cofinite (E.diff t s)
  81     | CoFinite s, Finite t-> cofinite (E.diff s t)
  82
  83   let inter s t = match s.node, t.node with
  84     | Finite s, Finite t -> finite (E.inter s t)
  85     | CoFinite s, CoFinite t -> cofinite (E.union s t)
  86     | Finite s, CoFinite t -> finite (E.diff s t)
  87     | CoFinite s, Finite t-> finite (E.diff t s)
  88
  89   let diff s t = match s.node, t.node with
  90     | Finite s, Finite t -> finite (E.diff s t)
  91     | Finite s, CoFinite t -> finite(E.inter s t)
  92     | CoFinite s, Finite t -> cofinite(E.union t s)
  93     | CoFinite s, CoFinite t -> finite (E.diff t s)
  94
  95   let complement t = match t.node with
  96     | Finite s -> cofinite s
  97     | CoFinite s -> finite s
  98
  99   let compare s t = match s.node, t.node with
 100     | Finite s , Finite t -> E.compare s t
 101     | CoFinite s , CoFinite t -> E.compare t s
 102     | Finite _, CoFinite _ -> -1
 103     | CoFinite _, Finite _ -> 1
 104
 105   let subset s t = match s.node, t.node with
 106     | Finite s , Finite t -> E.subset s t
 107     | CoFinite s , CoFinite t -> E.subset t s
 108     | Finite s, CoFinite t -> E.is_empty (E.inter s t)
 109     | CoFinite _, Finite _ -> false
 110
 111   (* given a  list l of type t list,
 112      returns two sets (f,c) where :
 113      - f is the union of all the finite sets of l
 114      - c is the union of all the cofinite sets of l
 115      - f and c are disjoint
 116      Invariant : cup f c = List.fold_left cup empty l
 117      We treat the CoFinite part explicitely :
 118   *)
 119
 120   let kind_split l =
 121
 122     let rec next_finite_cofinite facc cacc = function
 123       | [] -> finite facc, cofinite (E.diff cacc facc)
 124       | { node = Finite s; _ } ::r ->
 125         next_finite_cofinite (E.union s facc) cacc r
 126       | { node = CoFinite _ ; _ } ::r when E.is_empty cacc ->
 127         next_finite_cofinite facc cacc r
 128       | { node = CoFinite s; _ } ::r ->
 129         next_finite_cofinite facc (E.inter cacc s) r
 130     in
 131     let rec first_cofinite facc = function
 132       | [] -> empty,empty
 133       | { node = Finite s ; _ } :: r-> first_cofinite (E.union s facc) r
 134       | { node = CoFinite s ; _ } :: r -> next_finite_cofinite facc s r
 135     in
 136       first_cofinite E.empty l
 137
 138   let exn = FiniteCofinite_sig.InfiniteSet
 139
 140   let fold f t a = match t.node with
 141     | Finite s -> E.fold f s a
 142     | CoFinite _ -> raise exn
 143
 144   let iter f t = match t.node with
 145     | Finite t -> E.iter f t
 146     | CoFinite _ -> raise exn
 147
 148   let for_all f t = match t.node with
 149     | Finite s -> E.for_all f s
 150     | CoFinite _ -> raise exn
 151
 152   let exists f t = match t.node with
 153     | Finite s -> E.exists f s
 154     | CoFinite _ -> raise exn
 155
 156   let filter f t = match t.node with
 157     | Finite s -> finite (E.filter f s)
 158     | CoFinite _ -> raise exn
 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 exn
 163
 164   let cardinal t = match t.node with
 165     | Finite s -> E.cardinal s
 166     | CoFinite _ -> raise exn
 167
 168   let elements t = match t.node with
 169     | Finite s -> E.elements s
 170     | CoFinite _ -> raise exn
 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     | CoFinite _ -> raise exn
 178
 179   let is_singleton t = match t.node with
 180     | Finite s -> E.is_singleton s
 181     | CoFinite _ -> 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 _ , CoFinite _ -> 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     | CoFinite _ -> raise exn
 195
 196   let min_elt s = match s.node with
 197     | Finite s -> E.min_elt s
 198     | CoFinite _ -> raise exn
 199
 200   let max_elt s = match s.node with
 201     | Finite s -> E.min_elt s
 202     | CoFinite _ -> raise exn
 203
 204   let positive t = match t.node with
 205       | Finite x -> x
 206       | CoFinite _ -> E.empty
 207
 208   let negative t = match t.node with
 209       | CoFinite x -> x
 210       | Finite _ -> E.empty
 211
 212   let inj_positive t = finite t
 213   let inj_negative t = cofinite t
 214 end
 215
 216 module Make = Builder(Hcons.Make)
 217 module Weak = Builder(Hcons.Weak)