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

diff --git a/clib/segmenttree.ml b/clib/segmenttree.ml
new file mode 100644
index 0000000000..d0ded4cb59
--- /dev/null
+++ b/clib/segmenttree.ml
@@ -0,0 +1,138 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** This module is a very simple implementation of "segment trees".
+
+    A segment tree of type ['a t] represents a mapping from a union of
+    disjoint segments to some values of type 'a. 
+*)
+
+(** Misc. functions. *)
+let list_iteri f l =
+  let rec loop i = function
+    | [] -> ()
+    | x :: xs -> f i x; loop (i + 1) xs
+  in
+    loop 0 l
+
+let log2 x = log x /. log 2.
+
+let log2n x = int_of_float (ceil (log2 (float_of_int x))) 
+
+(** We focus on integers but this module can be generalized. *)
+type elt = int
+
+(** A value of type [domain] is interpreted differently given its position 
+    in the tree. On internal nodes, a domain represents the set of 
+    integers which are _not_ in the set of keys handled by the tree. On 
+    leaves, a domain represents the st of integers which are in the set of 
+    keys. *)
+type domain = 
+    (** On internal nodes, a domain [Interval (a, b)] represents 
+	the interval [a + 1; b - 1]. On leaves, it represents [a; b]. 
+	We always have [a] <= [b]. *)
+  | Interval of elt * elt
+      (** On internal node or root, a domain [Universe] represents all
+	  the integers. When the tree is not a trivial root,
+	  [Universe] has no interpretation on leaves. (The lookup
+	  function should never reach the leaves.) *)
+  | Universe
+
+(** We use an array to store the almost complete tree. This array
+    contains at least one element. *)
+type 'a t = (domain * 'a option) array
+
+(** The root is the first item of the array. *)
+
+(** Standard layout for left child. *)
+let left_child i = 2 * i + 1
+
+(** Standard layout for right child. *)
+let right_child i = 2 * i + 2
+
+(** Extract the annotation of a node, be it internal or a leaf. *)
+let value_of i t = match t.(i) with (_, Some x) -> x | _ -> raise Not_found
+
+(** Initialize the array to store [n] leaves. *)
+let create n init = 
+  Array.make (1 lsl (log2n n + 1) - 1) init
+
+(** Make a complete interval tree from a list of disjoint segments. 
+    Precondition : the segments must be sorted. *)
+let make segments = 
+  let nsegments = List.length segments in
+  let tree = create nsegments (Universe, None) in 
+  let leaves_offset = (1 lsl (log2n nsegments)) - 1 in
+
+    (** The algorithm proceeds in two steps using an intermediate tree
+	to store minimum and maximum of each subtree as annotation of
+	the node. *)
+
+    (** We start from leaves: the last level of the tree is initialized
+	with the given segments... *)
+    list_iteri 
+      (fun i ((start, stop), value) ->
+	 let k = leaves_offset + i in
+	 let i = Interval (start, stop) in
+	   tree.(k) <- (i, Some i))
+      segments;
+    (** ... the remaining leaves are initialized with neutral information. *)
+    for k = leaves_offset + nsegments to Array.length tree -1 do 
+      tree.(k) <- (Universe, Some Universe)
+    done;
+    
+    (** We traverse the tree bottom-up and compute the interval and
+	annotation associated to each node from the annotations of its
+	children. *)
+    for k = leaves_offset - 1 downto 0 do
+      let node, annotation = 
+	match value_of (left_child k) tree, value_of (right_child k) tree with
+	  | Interval (left_min, left_max), Interval (right_min, right_max) ->
+	      (Interval (left_max, right_min), Interval (left_min, right_max))
+	  | Interval (min, max), Universe -> 
+	      (Interval (max, max), Interval (min, max))
+	  | Universe, Universe -> Universe, Universe
+	  | Universe, _ -> assert false
+      in
+	tree.(k) <- (node, Some annotation)
+    done;
+
+    (** Finally, annotation are replaced with the image related to each leaf. *)
+    let final_tree = 
+      Array.mapi (fun i (segment, value) -> (segment, None)) tree
+    in
+      list_iteri 
+	(fun i ((start, stop), value) -> 
+	   final_tree.(leaves_offset + i) 
+	   <- (Interval (start, stop), Some value))
+	segments;      
+      final_tree
+
+(** [lookup k t] looks for an image for key [k] in the interval tree [t]. 
+    Raise [Not_found] if it fails. *)
+let lookup k t = 
+  let i = ref 0 in 
+    while (snd t.(!i) = None) do
+      match fst t.(!i) with
+	| Interval (start, stop) -> 
+	    if k <= start then i := left_child !i
+	    else if k >= stop then i:= right_child !i 
+	    else raise Not_found
+	| Universe -> raise Not_found
+    done;
+    match fst t.(!i) with
+      | Interval (start, stop) -> 
+	  if k >= start && k <= stop then
+	    match snd t.(!i) with 
+	      | Some v -> v
+	      | None -> assert false
+	  else 
+	    raise Not_found
+      | Universe -> assert false
+      
+