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