Source file `predicate.ml`

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