[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, 414 insertions, 0 deletions

diff --git a/clib/hMap.ml b/clib/hMap.ml
new file mode 100644
index 000000000..37079af78
--- /dev/null
+++ b/clib/hMap.ml
@@ -0,0 +1,414 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module type HashedType =
+sig
+  type t
+  val compare : t -> t -> int
+  val hash : t -> int
+end
+
+module SetMake(M : HashedType) =
+struct
+  (** Hash Sets use hashes to prevent doing too many comparison tests. They
+      associate to each hash the set of keys having that hash.
+
+      Invariants:
+
+      1. There is no empty set in the intmap.
+      2. All values in the same set have the same hash, which is the int to
+         which it is associated in the intmap.
+  *)
+
+  module Set = Set.Make(M)
+
+  type elt = M.t
+
+  type t = Set.t Int.Map.t
+
+  let empty = Int.Map.empty
+
+  let is_empty = Int.Map.is_empty
+
+  let mem x s =
+    let h = M.hash x in
+    try
+      let m = Int.Map.find h s in
+      Set.mem x m
+    with Not_found -> false
+
+  let add x s =
+    let h = M.hash x in
+    try
+      let m = Int.Map.find h s in
+      let m = Set.add x m in
+      Int.Map.set h m s
+    with Not_found ->
+      let m = Set.singleton x in
+      Int.Map.add h m s
+
+  let singleton x =
+    let h = M.hash x in
+    let m = Set.singleton x in
+    Int.Map.singleton h m
+
+  let remove x s =
+    let h = M.hash x in
+    try
+      let m = Int.Map.find h s in
+      let m = Set.remove x m in
+      if Set.is_empty m then
+        Int.Map.remove h s
+      else
+        Int.Map.set h m s
+    with Not_found -> s
+
+  let height s = Int.Map.height s
+
+  let is_smaller s1 s2 = height s1 <= height s2 + 3
+
+  (** Assumes s1 << s2 *)
+  let fast_union s1 s2 =
+    let fold h s accu =
+      try Int.Map.modify h (fun _ s' -> Set.fold Set.add s s') accu
+      with Not_found -> Int.Map.add h s accu
+    in
+    Int.Map.fold fold s1 s2
+
+  let union s1 s2 =
+    if is_smaller s1 s2 then fast_union s1 s2
+    else if is_smaller s2 s1 then fast_union s2 s1
+    else
+      let fu _ m1 m2 = match m1, m2 with
+      | None, None -> None
+      | (Some _ as m), None | None, (Some _ as m) -> m
+      | Some m1, Some m2 -> Some (Set.union m1 m2)
+      in
+      Int.Map.merge fu s1 s2
+
+  (** Assumes s1 << s2 *)
+  let fast_inter s1 s2 =
+    let fold h s accu =
+      try
+        let s' = Int.Map.find h s2 in
+        let si = Set.filter (fun e -> Set.mem e s') s in
+        if Set.is_empty si then accu
+        else Int.Map.add h si accu
+     with Not_found -> accu
+    in
+    Int.Map.fold fold s1 Int.Map.empty
+
+  let inter s1 s2 =
+    if is_smaller s1 s2 then fast_inter s1 s2
+    else if is_smaller s2 s1 then fast_inter s2 s1
+    else
+      let fu _ m1 m2 = match m1, m2 with
+      | None, None -> None
+      | Some _, None | None, Some _ -> None
+      | Some m1, Some m2 ->
+        let m = Set.inter m1 m2 in
+        if Set.is_empty m then None else Some m
+      in
+      Int.Map.merge fu s1 s2
+
+  (** Assumes s1 << s2 *)
+  let fast_diff_l s1 s2 =
+    let fold h s accu =
+      try
+        let s' = Int.Map.find h s2 in
+        let si = Set.filter (fun e -> not (Set.mem e s')) s in
+        if Set.is_empty si then accu
+        else Int.Map.add h si accu
+     with Not_found -> Int.Map.add h s accu
+    in
+    Int.Map.fold fold s1 Int.Map.empty
+
+  (** Assumes s2 << s1 *)
+  let fast_diff_r s1 s2 =
+    let fold h s accu =
+      try
+        let s' = Int.Map.find h accu in
+        let si = Set.filter (fun e -> not (Set.mem e s)) s' in
+        if Set.is_empty si then Int.Map.remove h accu
+        else Int.Map.set h si accu
+     with Not_found -> accu
+    in
+    Int.Map.fold fold s2 s1
+
+  let diff s1 s2 =
+    if is_smaller s1 s2 then fast_diff_l s1 s2
+    else if is_smaller s2 s2 then fast_diff_r s1 s2
+    else
+      let fu _ m1 m2 = match m1, m2 with
+      | None, None -> None
+      | (Some _ as m), None -> m
+      | None, Some _ -> None
+      | Some m1, Some m2 ->
+        let m = Set.diff m1 m2 in
+        if Set.is_empty m then None else Some m
+      in
+      Int.Map.merge fu s1 s2
+
+  let compare s1 s2 = Int.Map.compare Set.compare s1 s2
+
+  let equal s1 s2 = Int.Map.equal Set.equal s1 s2
+
+  let subset s1 s2 =
+    let check h m1 =
+      let m2 = try Int.Map.find h s2 with Not_found -> Set.empty in
+      Set.subset m1 m2
+    in
+    Int.Map.for_all check s1
+
+  let iter f s =
+    let fi _ m = Set.iter f m in
+    Int.Map.iter fi s
+
+  let fold f s accu =
+    let ff _ m accu = Set.fold f m accu in
+    Int.Map.fold ff s accu
+
+  let for_all f s =
+    let ff _ m = Set.for_all f m in
+    Int.Map.for_all ff s
+
+  let exists f s =
+    let fe _ m = Set.exists f m in
+    Int.Map.exists fe s
+
+  let filter f s =
+    let ff m = Set.filter f m in
+    let s = Int.Map.map ff s in
+    Int.Map.filter (fun _ m -> not (Set.is_empty m)) s
+
+  let partition f s =
+    let fold h m (sl, sr) =
+      let (ml, mr) = Set.partition f m in
+      let sl = if Set.is_empty ml then sl else Int.Map.add h ml sl in
+      let sr = if Set.is_empty mr then sr else Int.Map.add h mr sr in
+      (sl, sr)
+    in
+    Int.Map.fold fold s (Int.Map.empty, Int.Map.empty)
+
+  let cardinal s =
+    let fold _ m accu = accu + Set.cardinal m in
+    Int.Map.fold fold s 0
+
+  let elements s =
+    let fold _ m accu = Set.fold (fun x accu -> x :: accu) m accu in
+    Int.Map.fold fold s []
+
+  let min_elt _ = assert false (** Cannot be implemented efficiently *)
+
+  let max_elt _ = assert false (** Cannot be implemented efficiently *)
+
+  let choose s =
+    let (_, m) = Int.Map.choose s in
+    Set.choose m
+
+  let split s x = assert false (** Cannot be implemented efficiently *)
+
+end
+
+module Make(M : HashedType) =
+struct
+  (** This module is essentially the same as SetMake, except that we have maps
+      instead of sets in the intmap. Invariants are the same. *)
+  module Set = SetMake(M)
+  module Map = CMap.Make(M)
+
+  type key = M.t
+
+  type 'a t = 'a Map.t Int.Map.t
+
+  let empty = Int.Map.empty
+
+  let is_empty = Int.Map.is_empty
+
+  let mem k s =
+    let h = M.hash k in
+    try
+      let m = Int.Map.find h s in
+      Map.mem k m
+    with Not_found -> false
+
+  let add k x s =
+    let h = M.hash k in
+    try
+      let m = Int.Map.find h s in
+      let m = Map.add k x m in
+      Int.Map.set h m s
+    with Not_found ->
+      let m = Map.singleton k x in
+      Int.Map.add h m s
+
+  (* when Coq requires OCaml 4.06 or later, the module type
+     CSig.MapS may include the signature of OCaml's "update",
+     requiring an implementation here, which could be just:
+
+       let update k f s = assert false (* not implemented *)
+
+  *)
+
+  let singleton k x =
+    let h = M.hash k in
+    Int.Map.singleton h (Map.singleton k x)
+
+  let remove k s =
+    let h = M.hash k in
+    try
+      let m = Int.Map.find h s in
+      let m = Map.remove k m in
+      if Map.is_empty m then
+        Int.Map.remove h s
+      else
+        Int.Map.set h m s
+    with Not_found -> s
+
+  let merge f s1 s2 =
+    let fm h m1 m2 = match m1, m2 with
+    | None, None -> None
+    | Some m, None ->
+      let m = Map.merge f m Map.empty in
+      if Map.is_empty m then None
+      else Some m
+    | None, Some m ->
+      let m = Map.merge f Map.empty m in
+      if Map.is_empty m then None
+      else Some m
+    | Some m1, Some m2 ->
+      let m = Map.merge f m1 m2 in
+      if Map.is_empty m then None
+      else Some m
+    in
+    Int.Map.merge fm s1 s2
+
+  let compare f s1 s2 =
+    let fc m1 m2 = Map.compare f m1 m2 in
+    Int.Map.compare fc s1 s2
+
+  let equal f s1 s2 =
+    let fe m1 m2 = Map.equal f m1 m2 in
+    Int.Map.equal fe s1 s2
+
+  let iter f s =
+    let fi _ m = Map.iter f m in
+    Int.Map.iter fi s
+
+  let fold f s accu =
+    let ff _ m accu = Map.fold f m accu in
+    Int.Map.fold ff s accu
+
+  let for_all f s =
+    let ff _ m = Map.for_all f m in
+    Int.Map.for_all ff s
+
+  let exists f s =
+    let fe _ m = Map.exists f m in
+    Int.Map.exists fe s
+
+  let filter f s =
+    let ff m = Map.filter f m in
+    let s = Int.Map.map ff s in
+    Int.Map.filter (fun _ m -> not (Map.is_empty m)) s
+
+  let partition f s =
+    let fold h m (sl, sr) =
+      let (ml, mr) = Map.partition f m in
+      let sl = if Map.is_empty ml then sl else Int.Map.add h ml sl in
+      let sr = if Map.is_empty mr then sr else Int.Map.add h mr sr in
+      (sl, sr)
+    in
+    Int.Map.fold fold s (Int.Map.empty, Int.Map.empty)
+
+  let cardinal s =
+    let fold _ m accu = accu + Map.cardinal m in
+    Int.Map.fold fold s 0
+
+  let bindings s =
+    let fold _ m accu = Map.fold (fun k x accu -> (k, x) :: accu) m accu in
+    Int.Map.fold fold s []
+
+  let min_binding _ = assert false (** Cannot be implemented efficiently *)
+
+  let max_binding _ = assert false (** Cannot be implemented efficiently *)
+
+  let fold_left _ _ _ = assert false (** Cannot be implemented efficiently *)
+
+  let fold_right _ _ _ = assert false (** Cannot be implemented efficiently *)
+
+  let choose s =
+    let (_, m) = Int.Map.choose s in
+    Map.choose m
+
+  let find k s =
+    let h = M.hash k in
+    let m = Int.Map.find h s in
+    Map.find k m
+
+  let get k s = try find k s with Not_found -> assert false
+
+  let split k s = assert false (** Cannot be implemented efficiently *)
+
+  let map f s =
+    let fs m = Map.map f m in
+    Int.Map.map fs s
+
+  let mapi f s =
+    let fs m = Map.mapi f m in
+    Int.Map.map fs s
+
+  let modify k f s =
+    let h = M.hash k in
+    let m = Int.Map.find h s in
+    let m = Map.modify k f m in
+    Int.Map.set h m s
+
+  let bind f s =
+    let fb m = Map.bind f m in
+    Int.Map.map fb s
+
+  let domain s = Int.Map.map Map.domain s
+
+  let set k x s =
+    let h = M.hash k in
+    let m = Int.Map.find h s in
+    let m = Map.set k x m in
+    Int.Map.set h m s
+
+  let smartmap f s =
+    let fs m = Map.smartmap f m in
+    Int.Map.smartmap fs s
+
+  let smartmapi f s =
+    let fs m = Map.smartmapi f m in
+    Int.Map.smartmap fs s
+
+  let height s = Int.Map.height s
+
+  module Unsafe =
+  struct
+    let map f s =
+      let fs m = Map.Unsafe.map f m in
+      Int.Map.map fs s
+  end
+
+  module Monad(M : CMap.MonadS) =
+  struct
+    module IntM = Int.Map.Monad(M)
+    module ExtM = Map.Monad(M)
+
+    let fold f s accu =
+      let ff _ m accu = ExtM.fold f m accu in
+      IntM.fold ff s accu
+
+    let fold_left _ _ _ = assert false
+    let fold_right _ _ _ = assert false
+  end
+
+end