1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(************************************************************************)
(* *)
(* Objective Caml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Library General Public License. *)
(* *)
(************************************************************************)
module type OrderedType =
sig
type t
val compare: t -> t -> int
end
module type S =
sig
type elt
type t
val empty: t
val full: t
val is_empty: t -> bool
val is_full: t -> bool
val mem: elt -> t -> bool
val singleton: elt -> t
val add: elt -> t -> t
val remove: elt -> t -> t
val union: t -> t -> t
val inter: t -> t -> t
val diff: t -> t -> t
val complement: t -> t
val equal: t -> t -> bool
val subset: t -> t -> bool
val elements: t -> bool * elt list
val is_finite : t -> bool
end
module Make(Ord: OrderedType) =
struct
module EltSet = Set.Make(Ord)
type elt = Ord.t
(* (false, s) represents a set which is equal to the set s
(true, s) represents a set which is equal to the complement of set s *)
type t = bool * EltSet.t
let is_finite (b,_) = not b
let elements (b,s) = (b, EltSet.elements s)
let empty = (false,EltSet.empty)
let full = (true,EltSet.empty)
(* assumes the set is infinite *)
let is_empty (b,s) = not b && EltSet.is_empty s
let is_full (b,s) = b && EltSet.is_empty s
let mem x (b,s) =
if b then not (EltSet.mem x s) else EltSet.mem x s
let singleton x = (false,EltSet.singleton x)
let add x (b,s) =
if b then (b,EltSet.remove x s)
else (b,EltSet.add x s)
let remove x (b,s) =
if b then (b,EltSet.add x s)
else (b,EltSet.remove x s)
let complement (b,s) = (not b, s)
let union s1 s2 =
match (s1,s2) with
((false,p1),(false,p2)) -> (false,EltSet.union p1 p2)
| ((true,n1),(true,n2)) -> (true,EltSet.inter n1 n2)
| ((false,p1),(true,n2)) -> (true,EltSet.diff n2 p1)
| ((true,n1),(false,p2)) -> (true,EltSet.diff n1 p2)
let inter s1 s2 =
complement (union (complement s1) (complement s2))
let diff s1 s2 = inter s1 (complement s2)
(* assumes the set is infinite *)
let subset s1 s2 =
match (s1,s2) with
((false,p1),(false,p2)) -> EltSet.subset p1 p2
| ((true,n1),(true,n2)) -> EltSet.subset n2 n1
| ((false,p1),(true,n2)) -> EltSet.is_empty (EltSet.inter p1 n2)
| ((true,_),(false,_)) -> false
(* assumes the set is infinite *)
let equal (b1,s1) (b2,s2) =
b1=b2 && EltSet.equal s1 s2
end
|
