+++ /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-03-05 01:50:21 CET by Kim Nguyen>
-*)
-
-INCLUDE "utils.ml"
-
-include FiniteCofinite_sig
-
-module type HConsBuilder =
- functor (H : Common_sig.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
- | (Finite _| CoFinite _), _ -> 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 t = match t.node with
- | Finite s -> E.is_empty s
- | CoFinite _ -> false
-
- let is_any t = match t.node with
- | CoFinite s -> E.is_empty s
- | Finite _ -> false
-
- let is_finite t = match t.node with
- | Finite _ -> true
- | CoFinite _ -> false
-
- let kind t = match t.node with
- | Finite _ -> `Finite
- | CoFinite _ -> `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 = FiniteCofinite_sig.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
- | CoFinite _ -> raise exn
-
- let is_singleton t = match t.node with
- | Finite s -> E.is_singleton s
- | CoFinite _ -> 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 _ , CoFinite _ -> 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
-
- | CoFinite _ -> raise exn
-
- let min_elt s = match s.node with
- | Finite s -> E.min_elt s
- | CoFinite _ -> raise exn
-
- let max_elt s = match s.node with
- | Finite s -> E.min_elt s
- | CoFinite _ -> raise exn
-
- let positive t = match t.node with
- | Finite x -> x
- | CoFinite _ -> E.empty
-
- let negative t = match t.node with
- | CoFinite x -> x
- | Finite _ -> 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