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

diff --git a/clib/cList.mli b/clib/cList.mli
new file mode 100644
index 000000000..f87db04cf
--- /dev/null
+++ b/clib/cList.mli
@@ -0,0 +1,263 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+type 'a cmp = 'a -> 'a -> int
+type 'a eq = 'a -> 'a -> bool
+
+(** Module type [S] is the one from OCaml Stdlib. *)
+module type S = module type of List
+
+module type ExtS =
+sig
+  include S
+
+  val compare : 'a cmp -> 'a list cmp
+  (** Lexicographic order on lists. *)
+
+  val equal : 'a eq -> 'a list eq
+  (** Lifts equality to list type. *)
+
+  val is_empty : 'a list -> bool
+  (** Checks whether a list is empty *)
+
+  val init : int -> (int -> 'a) -> 'a list
+  (** [init n f] constructs the list [f 0; ... ; f (n - 1)]. *)
+
+  val mem_f : 'a eq -> 'a -> 'a list -> bool
+  (* Same as [List.mem], for some specific equality *)
+
+  val add_set : 'a eq -> 'a -> 'a list -> 'a list
+  (** [add_set x l] adds [x] in [l] if it is not already there, or returns [l]
+      otherwise. *)
+
+  val eq_set : 'a eq -> 'a list eq
+  (** Test equality up to permutation (but considering multiple occurrences) *)
+
+  val intersect : 'a eq -> 'a list -> 'a list -> 'a list
+  val union : 'a eq -> 'a list -> 'a list -> 'a list
+  val unionq : 'a list -> 'a list -> 'a list
+  val subtract : 'a eq -> 'a list -> 'a list -> 'a list
+  val subtractq : 'a list -> 'a list -> 'a list
+
+  val interval : int -> int -> int list
+  (** [interval i j] creates the list [[i; i + 1; ...; j]], or [[]] when 
+      [j <= i]. *)
+
+  val make : int -> 'a -> 'a list
+  (** [make n x] returns a list made of [n] times [x]. Raise
+      [Invalid_argument "List.make"] if [n] is negative. *)
+
+  val assign : 'a list -> int -> 'a -> 'a list
+  (** [assign l i x] sets the [i]-th element of [l] to [x], starting from [0]. *)
+
+  val distinct : 'a list -> bool
+  (** Return [true] if all elements of the list are distinct. *)
+
+  val distinct_f : 'a cmp -> 'a list -> bool
+
+  val duplicates : 'a eq -> 'a list -> 'a list
+  (** Return the list of unique elements which appear at least twice. Elements
+      are kept in the order of their first appearance. *)
+
+  val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
+  val map_filter : ('a -> 'b option) -> 'a list -> 'b list
+  val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
+
+  val filter_with : bool list -> 'a list -> 'a list
+  (** [filter_with b a] selects elements of [a] whose corresponding element in
+      [b] is [true]. Raise [Invalid_argument _] when sizes differ. *)
+
+  val smartmap : ('a -> 'a) -> 'a list -> 'a list
+  (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
+    [f ai == ai], then [smartmap f l == l] *)
+
+  val map_left : ('a -> 'b) -> 'a list -> 'b list
+  (** As [map] but ensures the left-to-right order of evaluation. *)
+
+  val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+  (** As [map] but with the index, which starts from [0]. *)
+
+  val map2_i :
+    (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
+  val map3 :
+    ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
+  val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list ->
+    'd list -> 'e list
+  val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
+  val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
+
+  val map_of_array : ('a -> 'b) -> 'a array -> 'b list
+  (** [map_of_array f a] behaves as [List.map f (Array.to_list a)] *)
+
+  val smartfilter : ('a -> bool) -> 'a list -> 'a list
+  (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
+    [f ai = true], then [smartfilter f l == l] *)
+
+  val extend : bool list -> 'a -> 'a list -> 'a list
+(** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n];
+    it extends [a1..an] by inserting [a] at the position of [false] in [l] *)
+  val count : ('a -> bool) -> 'a list -> int
+
+  val index : 'a eq -> 'a -> 'a list -> int
+  (** [index] returns the 1st index of an element in a list (counting from 1). *)
+
+  val index0 : 'a eq -> 'a -> 'a list -> int
+  (** [index0] behaves as [index] except that it starts counting at 0. *)
+
+  val iteri :  (int -> 'a -> unit) -> 'a list -> unit
+  (** As [iter] but with the index argument (starting from 0). *)
+
+  val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c
+  (** acts like [fold_left f acc s] while [f] returns
+      [Cont acc']; it stops returning [c] as soon as [f] returns [Stop c]. *)
+
+  val fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
+  val fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
+  val fold_right_and_left :
+      ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
+  val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
+  val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
+  val except : 'a eq -> 'a -> 'a list -> 'a list
+  val remove : 'a eq -> 'a -> 'a list -> 'a list
+
+  val remove_first : ('a -> bool) -> 'a list -> 'a list
+  (** Remove the first element satisfying a predicate, or raise [Not_found] *)
+
+  val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
+  (** Remove and return the first element satisfying a predicate,
+      or raise [Not_found] *)
+
+  val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
+  (** Insert at the (first) position so that if the list is ordered wrt to the
+      total order given as argument, the order is preserved *)
+
+  val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+  val sep_last : 'a list -> 'a * 'a list
+
+  val find_map : ('a -> 'b option) -> 'a list -> 'b
+  (** Returns the first element that is mapped to [Some _]. Raise [Not_found] if
+      there is none. *)
+
+  val uniquize : 'a list -> 'a list
+  (** Return the list of elements without duplicates.
+      This is the list unchanged if there was none. *)
+
+  val sort_uniquize : 'a cmp -> 'a list -> 'a list
+  (** Return a sorted and de-duplicated version of a list,
+      according to some comparison function. *)
+
+  val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list
+  (** Merge two sorted lists and preserves the uniqueness property. *)
+
+  val subset : 'a list -> 'a list -> bool
+
+  val chop : int -> 'a list -> 'a list * 'a list
+  (** [chop i l] splits [l] into two lists [(l1,l2)] such that
+      [l1++l2=l] and [l1] has length [i].  It raises [Failure] when [i]
+      is negative or greater than the length of [l] *)
+
+  exception IndexOutOfRange
+  val goto: int -> 'a list -> 'a list * 'a list
+  (** [goto i l] splits [l] into two lists [(l1,l2)] such that
+      [(List.rev l1)++l2=l] and [l1] has length [i].  It raises
+      [IndexOutOfRange] when [i] is negative or greater than the
+      length of [l]. *)
+
+
+  val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
+  val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
+  val firstn : int -> 'a list -> 'a list
+  val last : 'a list -> 'a
+  val lastn : int -> 'a list -> 'a list
+  val skipn : int -> 'a list -> 'a list
+  val skipn_at_least : int -> 'a list -> 'a list
+
+  val addn : int -> 'a -> 'a list -> 'a list
+  (** [addn n x l] adds [n] times [x] on the left of [l]. *)
+
+  val prefix_of : 'a eq -> 'a list -> 'a list -> bool
+  (** [prefix_of l1 l2] returns [true] if [l1] is a prefix of [l2], [false]
+      otherwise. *)
+
+  val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list
+  (** [drop_prefix p l] returns [t] if [l=p++t] else return [l]. *)
+
+  val drop_last : 'a list -> 'a list
+
+  val map_append : ('a -> 'b list) -> 'a list -> 'b list
+  (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)]. *)
+
+  val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
+  (** As [map_append]. Raises [Invalid_argument _] if the two lists don't have 
+      the same length. *)
+
+  val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
+
+  val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+  (** [fold_left_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
+    where [(e_i,k_i)=f e_{i-1} l_i] *)
+
+  val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+  (** Same, folding on the right *)
+
+  val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
+  (** Same with two lists, folding on the left *)
+
+  val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
+  (** Same with two lists, folding on the right *)
+
+  val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
+  (** Same with three lists, folding on the left *)
+
+  val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
+  (** Same with four lists, folding on the left *)
+
+  val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+  (* [@@ocaml.deprecated "Same as [fold_left_map]"] *)
+  (** @deprecated Same as [fold_left_map] *)
+
+  val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+  (** @deprecated Same as [fold_right_map] *)
+
+  val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
+  val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
+  val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
+  val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool
+
+  val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+  (** A generic cartesian product: for any operator (**),
+    [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
+    and so on if there are more elements in the lists. *)
+
+  val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
+  (** [cartesians] is an n-ary cartesian product: it iterates
+    [cartesian] over a list of lists.  *)
+
+  val combinations : 'a list list -> 'a list list
+  (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
+
+  val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
+
+  val cartesians_filter :
+    ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
+  (** Keep only those products that do not return None *)
+
+  val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
+
+  module type MonoS = sig
+    type elt
+    val equal : elt list -> elt list -> bool
+    val mem : elt -> elt list -> bool
+    val assoc : elt -> (elt * 'a) list -> 'a
+    val mem_assoc : elt -> (elt * 'a) list -> bool
+    val remove_assoc : elt -> (elt * 'a) list -> (elt * 'a) list
+    val mem_assoc_sym : elt -> ('a * elt) list -> bool
+  end
+end
+
+include ExtS