Transparent

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 168 insertions, 0 deletions

diff --git a/lib/predicate.ml b/lib/predicate.ml
new file mode 100644
index 000000000..1b2ef443b
--- /dev/null
+++ b/lib/predicate.ml
@@ -0,0 +1,99 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                           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.         *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(* Sets over ordered types *)
+
+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
+  end
+
+module Make(Ord: OrderedType) =
+  struct
+    module EltSet = Set.Make(Ord)
+ 
+    (* when bool is false, the denoted set is the complement of
+       the given set *)
+    type elt = Ord.t
+    type t = bool * EltSet.t
+
+    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)
+
+    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
+
+    let equal (b1,s1) (b2,s2) =
+      b1=b2 & EltSet.equal s1 s2
+
+  end
diff --git a/lib/predicate.mli b/lib/predicate.mli
new file mode 100644
index 000000000..73e4ecce9
--- /dev/null
+++ b/lib/predicate.mli
@@ -0,0 +1,69 @@
+
+(* $Id$ *)
+
+(* Module [Pred]: sets over infinite ordered types with complement. *)
+
+(* This module implements the set data structure, given a total ordering
+   function over the set elements. All operations over sets
+   are purely applicative (no side-effects).
+   The implementation uses the Set library. *)
+
+module type OrderedType =
+  sig
+    type t
+    val compare: t -> t -> int
+  end
+          (* The input signature of the functor [Pred.Make].
+             [t] is the type of the set elements.
+             [compare] is a total ordering function over the set elements.
+             This is a two-argument function [f] such that
+             [f e1 e2] is zero if the elements [e1] and [e2] are equal,
+             [f e1 e2] is strictly negative if [e1] is smaller than [e2],
+             and [f e1 e2] is strictly positive if [e1] is greater than [e2].
+             Example: a suitable ordering function is
+             the generic structural comparison function [compare]. *)
+
+module type S =
+  sig
+    type elt
+          (* The type of the set elements. *)
+    type t
+          (* The type of sets. *)
+    val empty: t
+          (* The empty set. *)
+    val full: t
+          (* The whole type. *)
+    val is_empty: t -> bool
+        (* Test whether a set is empty or not. *)
+    val is_full: t -> bool
+        (* Test whether a set contains the whole type or not. *)
+    val mem: elt -> t -> bool
+        (* [mem x s] tests whether [x] belongs to the set [s]. *)
+    val singleton: elt -> t
+        (* [singleton x] returns the one-element set containing only [x]. *)
+    val add: elt -> t -> t
+        (* [add x s] returns a set containing all elements of [s],
+           plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
+    val remove: elt -> t -> t
+        (* [remove x s] returns a set containing all elements of [s],
+           except [x]. If [x] was not in [s], [s] is returned unchanged. *)
+    val union: t -> t -> t
+    val inter: t -> t -> t
+    val diff: t -> t -> t
+    val complement: t -> t
+        (* Union, intersection, difference and set complement. *)
+    val equal: t -> t -> bool
+        (* [equal s1 s2] tests whether the sets [s1] and [s2] are
+           equal, that is, contain equal elements. *)
+    val subset: t -> t -> bool
+        (* [subset s1 s2] tests whether the set [s1] is a subset of
+           the set [s2]. *)
+    val elements: t -> bool * elt list
+        (* Gives a finite representation of the predicate: if the
+           boolean is false, then the predicate is given in extension.
+           if it is true, then the complement is given *)
+  end
+
+module Make(Ord: OrderedType): (S with type elt = Ord.t)
+        (* Functor building an implementation of the set structure
+           given a totally ordered type. *)