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