--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-01-30 19:09:01 CET by Kim Nguyen>
+*)
+
+INCLUDE "utils.ml"
+
+include Sigs.FINITECOFINITE
+
+module type HConsBuilder =
+ functor (H : Sigs.AUX.HashedType) -> Hcons.S with type data = H.t
+
+module Builder (HCB : HConsBuilder) (E : Ptset.S) :
+ S with type elt = E.elt and type set = E.t =
+struct
+ type elt = E.elt
+ type node = Finite of E.t | CoFinite of E.t
+ type set = E.t
+ module Node = HCB(struct
+ type t = node
+ let equal a b =
+ match a, b with
+ Finite (s1), Finite (s2)
+ | CoFinite (s1), CoFinite (s2) -> E.equal s1 s2
+ | _ -> false
+
+ let hash = function
+ | Finite s -> HASHINT2 (PRIME1, E.hash s)
+ | CoFinite s -> HASHINT2 (PRIME3, E.hash s)
+ end)
+ include Node
+ let empty = make (Finite E.empty)
+ let any = make (CoFinite E.empty)
+ let finite x = make (Finite x)
+ let cofinite x = make (CoFinite x)
+
+ let is_empty = function
+ | { node = Finite s } when E.is_empty s -> true
+ | _ -> false
+
+ let is_any = function
+ | { node = CoFinite s } when E.is_empty s -> true
+ | _ -> false
+
+ let is_finite t = match t.node with
+ | Finite _ -> true | _ -> false
+
+ let kind t = match t.node with
+ | Finite _ -> `Finite
+ | _ -> `Cofinite
+
+ let mem x t = match t.node with
+ | Finite s -> E.mem x s
+ | CoFinite s -> not (E.mem x s)
+
+ let singleton x = finite (E.singleton x)
+
+ let add e t = match t.node with
+ | Finite s -> finite (E.add e s)
+ | CoFinite s -> cofinite (E.remove e s)
+
+ let remove e t = match t.node with
+ | Finite s -> finite (E.remove e s)
+ | CoFinite s -> cofinite (E.add e s)
+
+ let union s t = match s.node, t.node with
+ | Finite s, Finite t -> finite (E.union s t)
+ | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
+ | Finite s, CoFinite t -> cofinite (E.diff t s)
+ | CoFinite s, Finite t-> cofinite (E.diff s t)
+
+ let inter s t = match s.node, t.node with
+ | Finite s, Finite t -> finite (E.inter s t)
+ | CoFinite s, CoFinite t -> cofinite (E.union s t)
+ | Finite s, CoFinite t -> finite (E.diff s t)
+ | CoFinite s, Finite t-> finite (E.diff t s)
+
+ let diff s t = match s.node, t.node with
+ | Finite s, Finite t -> finite (E.diff s t)
+ | Finite s, CoFinite t -> finite(E.inter s t)
+ | CoFinite s, Finite t -> cofinite(E.union t s)
+ | CoFinite s, CoFinite t -> finite (E.diff t s)
+
+ let complement t = match t.node with
+ | Finite s -> cofinite s
+ | CoFinite s -> finite s
+
+ let compare s t = match s.node, t.node with
+ | Finite s , Finite t -> E.compare s t
+ | CoFinite s , CoFinite t -> E.compare t s
+ | Finite _, CoFinite _ -> -1
+ | CoFinite _, Finite _ -> 1
+
+ let subset s t = match s.node, t.node with
+ | Finite s , Finite t -> E.subset s t
+ | CoFinite s , CoFinite t -> E.subset t s
+ | Finite s, CoFinite t -> E.is_empty (E.inter s t)
+ | CoFinite _, Finite _ -> false
+
+ (* given a list l of type t list,
+ returns two sets (f,c) where :
+ - f is the union of all the finite sets of l
+ - c is the union of all the cofinite sets of l
+ - f and c are disjoint
+ Invariant : cup f c = List.fold_left cup empty l
+ We treat the CoFinite part explicitely :
+ *)
+
+ let kind_split l =
+
+ let rec next_finite_cofinite facc cacc = function
+ | [] -> finite facc, cofinite (E.diff cacc facc)
+ | { node = Finite s } ::r ->
+ next_finite_cofinite (E.union s facc) cacc r
+ | { node = CoFinite _ } ::r when E.is_empty cacc ->
+ next_finite_cofinite facc cacc r
+ | { node = CoFinite s } ::r ->
+ next_finite_cofinite facc (E.inter cacc s) r
+ in
+ let rec first_cofinite facc = function
+ | [] -> empty,empty
+ | { node = Finite s } :: r-> first_cofinite (E.union s facc) r
+ | { node = CoFinite s } :: r -> next_finite_cofinite facc s r
+ in
+ first_cofinite E.empty l
+
+ let exn = Sigs.FINITECOFINITE.InfiniteSet
+
+ let fold f t a = match t.node with
+ | Finite s -> E.fold f s a
+ | CoFinite _ -> raise exn
+
+ let iter f t = match t.node with
+ | Finite t -> E.iter f t
+ | CoFinite _ -> raise exn
+
+ let for_all f t = match t.node with
+ | Finite s -> E.for_all f s
+ | CoFinite _ -> raise exn
+
+ let exists f t = match t.node with
+ | Finite s -> E.exists f s
+ | CoFinite _ -> raise exn
+
+ let filter f t = match t.node with
+ | Finite s -> finite (E.filter f s)
+ | CoFinite _ -> raise exn
+
+ let partition f t = match t.node with
+ | Finite s -> let a,b = E.partition f s in finite a,finite b
+ | CoFinite _ -> raise exn
+
+ let cardinal t = match t.node with
+ | Finite s -> E.cardinal s
+ | CoFinite _ -> raise exn
+
+ let elements t = match t.node with
+ | Finite s -> E.elements s
+ | CoFinite _ -> raise exn
+
+ let from_list l =
+ finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
+
+ let choose t = match t.node with
+ Finite s -> E.choose s
+ | _ -> raise exn
+
+ let is_singleton t = match t.node with
+ | Finite s -> E.is_singleton s
+ | _ -> false
+
+ let intersect s t = match s.node, t.node with
+ | Finite s, Finite t -> E.intersect s t
+ | CoFinite s, Finite t -> not (E.subset t s)
+ | Finite s, CoFinite t -> not (E.subset s t)
+ | CoFinite s, CoFinite t -> true
+
+ let split x s = match s.node with
+ | Finite s ->
+ let s1, b, s2 = E.split x s in
+ finite s1, b, finite s2
+
+ | _ -> raise exn
+
+ let min_elt s = match s.node with
+ | Finite s -> E.min_elt s
+ | _ -> raise exn
+
+ let max_elt s = match s.node with
+ | Finite s -> E.min_elt s
+ | _ -> raise exn
+
+ let positive t =
+ match t.node with
+ | Finite x -> x
+ | _ -> E.empty
+
+ let negative t =
+ match t.node with
+ | CoFinite x -> x
+ | _ -> E.empty
+
+ let inj_positive t = finite t
+ let inj_negative t = cofinite t
+end
+
+module Make = Builder(Hcons.Make)
+module Weak = Builder(Hcons.Weak)
projects / tatoo.git / blobdiff