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-03-05 00:35:26 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       | (Finite _| CoFinite _), _ -> 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 t =  match t.node with
  52     | Finite s -> E.is_empty s
  53     | CoFinite _  -> false
  54
  55   let is_any t = match t.node with
  56     | CoFinite s -> E.is_empty s
  57     | Finite _  -> false
  58
  59   let is_finite t = match t.node with
  60     | Finite _ -> true
  61     | CoFinite _ -> false
  62
  63   let kind t = match t.node with
  64     | Finite _ -> `Finite
  65     | CoFinite _  -> `Cofinite
  66
  67   let mem x t = match t.node with
  68     | Finite s -> E.mem x s
  69     | CoFinite s -> not (E.mem x s)
  70
  71   let singleton x = finite (E.singleton x)
  72
  73   let add e t = match t.node with
  74     | Finite s -> finite (E.add e s)
  75     | CoFinite s -> cofinite (E.remove e s)
  76
  77   let remove e t = match t.node with
  78     | Finite s -> finite (E.remove e s)
  79     | CoFinite s -> cofinite (E.add e s)
  80
  81   let union s t = match s.node, t.node with
  82     | Finite s, Finite t -> finite (E.union s t)
  83     | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
  84     | Finite s, CoFinite t -> cofinite (E.diff t s)
  85     | CoFinite s, Finite t-> cofinite (E.diff s t)
  86
  87   let inter s t = match s.node, t.node with
  88     | Finite s, Finite t -> finite (E.inter s t)
  89     | CoFinite s, CoFinite t -> cofinite (E.union s t)
  90     | Finite s, CoFinite t -> finite (E.diff s t)
  91     | CoFinite s, Finite t-> finite (E.diff t s)
  92
  93   let diff s t = match s.node, t.node with
  94     | Finite s, Finite t -> finite (E.diff s t)
  95     | Finite s, CoFinite t -> finite(E.inter s t)
  96     | CoFinite s, Finite t -> cofinite(E.union t s)
  97     | CoFinite s, CoFinite t -> finite (E.diff t s)
  98
  99   let complement t = match t.node with
 100     | Finite s -> cofinite s
 101     | CoFinite s -> finite s
 102
 103   let compare s t = match s.node, t.node with
 104     | Finite s , Finite t -> E.compare s t
 105     | CoFinite s , CoFinite t -> E.compare t s
 106     | Finite _, CoFinite _ -> -1
 107     | CoFinite _, Finite _ -> 1
 108
 109   let subset s t = match s.node, t.node with
 110     | Finite s , Finite t -> E.subset s t
 111     | CoFinite s , CoFinite t -> E.subset t s
 112     | Finite s, CoFinite t -> E.is_empty (E.inter s t)
 113     | CoFinite _, Finite _ -> false
 114
 115   (* given a  list l of type t list,
 116      returns two sets (f,c) where :
 117      - f is the union of all the finite sets of l
 118      - c is the union of all the cofinite sets of l
 119      - f and c are disjoint
 120      Invariant : cup f c = List.fold_left cup empty l
 121      We treat the CoFinite part explicitely :
 122   *)
 123
 124   let kind_split l =
 125
 126     let rec next_finite_cofinite facc cacc = function
 127       | [] -> finite facc, cofinite (E.diff cacc facc)
 128       | { node = Finite s; _ } ::r ->
 129         next_finite_cofinite (E.union s facc) cacc r
 130       | { node = CoFinite _ ; _ } ::r when E.is_empty cacc ->
 131         next_finite_cofinite facc cacc r
 132       | { node = CoFinite s; _ } ::r ->
 133         next_finite_cofinite facc (E.inter cacc s) r
 134     in
 135     let rec first_cofinite facc = function
 136       | [] -> empty,empty
 137       | { node = Finite s ; _ } :: r-> first_cofinite (E.union s facc) r
 138       | { node = CoFinite s ; _ } :: r -> next_finite_cofinite facc s r
 139     in
 140       first_cofinite E.empty l
 141
 142   let exn = Sigs.FINITECOFINITE.InfiniteSet
 143
 144   let fold f t a = match t.node with
 145     | Finite s -> E.fold f s a
 146     | CoFinite _ -> raise exn
 147
 148   let iter f t = match t.node with
 149     | Finite t -> E.iter f t
 150     | CoFinite _ -> raise exn
 151
 152   let for_all f t = match t.node with
 153     | Finite s -> E.for_all f s
 154     | CoFinite _ -> raise exn
 155
 156   let exists f t = match t.node with
 157     | Finite s -> E.exists f s
 158     | CoFinite _ -> raise exn
 159
 160   let filter f t = match t.node with
 161     | Finite s -> finite (E.filter f s)
 162     | CoFinite _ -> raise exn
 163
 164   let partition f t = match t.node with
 165     | Finite s -> let a,b = E.partition f s in finite a,finite b
 166     | CoFinite _ -> raise exn
 167
 168   let cardinal t = match t.node with
 169     | Finite s -> E.cardinal s
 170     | CoFinite _ -> raise exn
 171
 172   let elements t = match t.node with
 173     | Finite s -> E.elements s
 174     | CoFinite _ -> raise exn
 175
 176   let from_list l =
 177     finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
 178
 179   let choose t = match t.node with
 180       Finite s -> E.choose s
 181     | CoFinite _ -> raise exn
 182
 183   let is_singleton t = match t.node with
 184     | Finite s -> E.is_singleton s
 185     | CoFinite _ -> false
 186
 187   let intersect s t = match s.node, t.node with
 188     | Finite s, Finite t -> E.intersect s t
 189     | CoFinite s, Finite t -> not (E.subset t s)
 190     | Finite s, CoFinite t -> not (E.subset s t)
 191     | CoFinite _ , CoFinite _ -> true
 192
 193   let split x s = match s.node with
 194     | Finite s ->
 195       let s1, b, s2 = E.split x s in
 196       finite s1, b, finite s2
 197
 198     | CoFinite _ -> raise exn
 199
 200   let min_elt s = match s.node with
 201     | Finite s -> E.min_elt s
 202     | CoFinite _ -> raise exn
 203
 204   let max_elt s = match s.node with
 205     | Finite s -> E.min_elt s
 206     | CoFinite _ -> raise exn
 207
 208   let positive t = match t.node with
 209       | Finite x -> x
 210       | CoFinite _ -> E.empty
 211
 212   let negative t = match t.node with
 213       | CoFinite x -> x
 214       | Finite _ -> E.empty
 215
 216   let inj_positive t = finite t
 217   let inj_negative t = cofinite t
 218 end
 219
 220 module Make = Builder(Hcons.Make)
 221 module Weak = Builder(Hcons.Weak)