From 5e4bf04a2081717ca6b6e0b058c4c9e0823d183c Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 23 Feb 2017 15:11:58 +0100
Subject: [PATCH] wip: lattice structure

---
 _oasis                 |  2 +-
 src/data/CCLattice.ml  | 74 ++++++++++++++++++++++++++++++++++++++++++
 src/data/CCLattice.mli | 72 ++++++++++++++++++++++++++++++++++++++++
 3 files changed, 147 insertions(+), 1 deletion(-)
 create mode 100644 src/data/CCLattice.ml
 create mode 100644 src/data/CCLattice.mli

diff --git a/_oasis b/_oasis
index 4ae672b6..8cafa9e2 100644
--- a/_oasis
+++ b/_oasis
@@ -67,7 +67,7 @@ Library "containers_data"
                     CCPersistentHashtbl, CCDeque, CCFQueue, CCBV, CCMixtbl,
                     CCMixmap, CCRingBuffer, CCIntMap, CCPersistentArray,
                     CCMixset, CCGraph, CCHashSet, CCBitField,
-                    CCHashTrie, CCWBTree, CCRAL,
+                    CCHashTrie, CCWBTree, CCRAL, CCLattice,
                     CCImmutArray, CCHet, CCZipper
   BuildDepends:     bytes
   # BuildDepends:     bytes, bisect_ppx
diff --git a/src/data/CCLattice.ml b/src/data/CCLattice.ml
new file mode 100644
index 00000000..e28371ea
--- /dev/null
+++ b/src/data/CCLattice.ml
@@ -0,0 +1,74 @@
+
+(* This file is free software, part of containers. See file "license" for more details. *)
+
+(** {1 Lattice} *)
+
+type 'a sequence = ('a -> unit) -> unit
+
+module type SEMI_LATTICE = sig
+  type t
+
+  val equal : t -> t -> bool
+
+  val leq : t -> t -> bool
+  (** Partial order, which must satisfy:
+      - [leq a b && leq b c => leq a c]
+      - [leq a a]
+  *)
+
+  val meet : t -> t -> t
+  (** Greatest lower bound.
+      Must satisfy:
+      - [leq (meet a b) a]
+      - [leq (meet a b) b]
+      - [meet a a = a]
+      - [meet a b = meet b a]
+  *)
+
+  val bottom : t
+  (** Minimal element, such that forall [x], [leq bottom x].
+      In particular, this means that [meet bottom x = bottom] *)
+end
+
+module type S = sig
+  type key
+
+  type +'a t
+  (** Map from [key] to values of type ['a] *)
+
+  val empty : 'a t
+
+  val find : key -> 'a t -> 'a
+
+  val get : key -> 'a t -> 'a option
+
+  val add : key -> 'a -> 'a t -> 'a t
+
+  val remove : key -> 'a t -> 'a t
+
+  val find_all_leq : key -> 'a t -> (key * 'a) sequence
+  (** [find_all_leq x t] returns all elements of [t] that are smaller
+      or equal to [x] *)
+
+  val to_seq : 'a t -> (key * 'a) sequence
+
+  val of_seq : (key * 'a) sequence -> 'a t
+
+  val to_list : 'a t -> (key * 'a) list
+
+  val of_list : (key * 'a) list -> 'a t
+end
+
+module Make(S : SEMI_LATTICE) = struct
+  type key = S.t
+
+  type bal = int (* -1,0,1 *)
+
+  type +'a t =
+    | Empty
+    | Inner of key * 'a t * 'a t * bal (* AVL balancing *)
+    | Leaf of key * 'a
+
+
+
+end
diff --git a/src/data/CCLattice.mli b/src/data/CCLattice.mli
new file mode 100644
index 00000000..4feaf3a4
--- /dev/null
+++ b/src/data/CCLattice.mli
@@ -0,0 +1,72 @@
+
+(* This file is free software, part of containers. See file "license" for more details. *)
+
+(** {1 Lattice} *)
+
+(** Data structure for efficiently representices (full) lattices.
+    A lattice is a structure with a partial order [a < b],
+    where for every [a,b] that are incomparable, there
+    are [join a b] with [a <= join a b], [b <= join a b] (least upper bound)
+    and [meet a b] with [meet a b <= a], [meet a b <= b] (greatest lower bound).
+
+    We exploit this to make querying for every element larger than [x]
+    fast.
+*)
+
+type 'a sequence = ('a -> unit) -> unit
+
+module type SEMI_LATTICE = sig
+  type t
+
+  val equal : t -> t -> bool
+
+  val leq : t -> t -> bool
+  (** Partial order, which must satisfy:
+      - [leq a b && leq b c => leq a c]
+      - [leq a a]
+  *)
+
+  val meet : t -> t -> t
+  (** Greatest lower bound.
+      Must satisfy:
+      - [leq (meet a b) a]
+      - [leq (meet a b) b]
+      - [meet a a = a]
+      - [meet a b = meet b a]
+  *)
+
+  val bottom : t
+  (** Minimal element, such that forall [x], [leq bottom x].
+      In particular, this means that [meet bottom x = bottom] *)
+end
+
+module type S = sig
+  type key
+
+  type +'a t
+  (** Map from [key] to values of type ['a] *)
+
+  val empty : 'a t
+
+  val find : key -> 'a t -> 'a
+
+  val get : key -> 'a t -> 'a option
+
+  val add : key -> 'a -> 'a t -> 'a t
+
+  val remove : key -> 'a t -> 'a t
+
+  val find_all_leq : key -> 'a t -> (key * 'a) sequence
+  (** [find_all_leq x t] returns all elements of [t] that are smaller
+      or equal to [x] *)
+
+  val to_seq : 'a t -> (key * 'a) sequence
+
+  val of_seq : (key * 'a) sequence -> 'a t
+
+  val to_list : 'a t -> (key * 'a) list
+
+  val of_list : (key * 'a) list -> 'a t
+end
+
+module Make(S : SEMI_LATTICE) : S with type key = S.t