[lib] Split auxiliary libraries into Coq-specific and general.

Up to this point the `lib` directory contained two different library
archives, `clib.cma` and `lib.cma`, which a rough splitting between
Coq-specific libraries and general-purpose ones.

We know split the directory in two, as to make the distinction clear:

- `clib`: contains libraries that are not Coq specific and implement
  common data structures and programming patterns. These libraries
  could be eventually replace with external dependencies and the rest
  of the code base wouldn't notice much.

- `lib`: contains Coq-specific common libraries in widespread use
  along the codebase, but that are not considered part of other
  components. Examples are printing, error handling, or flags.

In some cases we have coupling due to utility files depending on Coq
specific flags, however this commit doesn't modify any files, but only
moves them around, further cleanup is welcome, as indeed a few files
in `lib` should likely be placed in `clib`.

Also note that `Deque` is not used ATM.

1 files changed, 98 insertions, 0 deletions

diff --git a/clib/predicate.ml b/clib/predicate.ml
new file mode 100644
index 000000000..1aa7db6af
--- /dev/null
+++ b/clib/predicate.ml
@@ -0,0 +1,98 @@
+(************************************************************************)
+(*                                                                     *)
+(*                           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
+  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 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