1 files changed, 82 insertions, 0 deletions
diff --git a/lib/acyclicGraph.mli b/lib/acyclicGraph.mli
new file mode 100644
index 0000000000..b53a4c018f
--- /dev/null
+++ b/lib/acyclicGraph.mli
@@ -0,0 +1,82 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Graphs representing strict orders *)
+
+type constraint_type = Lt | Le | Eq
+
+module type Point = sig
+  type t
+
+  module Set : CSig.SetS with type elt = t
+  module Map : CMap.ExtS with type key = t and module Set := Set
+
+  module Constraint : CSet.S with type elt = (t * constraint_type * t)
+
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+
+  type explanation = (constraint_type * t) list
+  val error_inconsistency : constraint_type -> t -> t -> explanation lazy_t option -> 'a
+
+  val pr : t -> Pp.t
+end
+
+module Make (Point:Point) : sig
+
+  type t
+
+  val empty : t
+
+  val check_invariants : required_canonical:(Point.t -> bool) -> t -> unit
+
+  exception AlreadyDeclared
+  val add : ?rank:int -> Point.t -> t -> t
+  (** All points must be pre-declared through this function before
+     they can be mentioned in the others. NB: use a large [rank] to
+     keep the node canonical *)
+
+  exception Undeclared of Point.t
+  val check_declared : t -> Point.Set.t -> unit
+  (** @raise Undeclared if one of the points is not present in the graph. *)
+
+  type 'a check_function = t -> 'a -> 'a -> bool
+
+  val check_eq : Point.t check_function
+  val check_leq : Point.t check_function
+  val check_lt : Point.t check_function
+
+  val enforce_eq : Point.t -> Point.t -> t -> t
+  val enforce_leq : Point.t -> Point.t -> t -> t
+  val enforce_lt : Point.t -> Point.t -> t -> t
+
+  val constraints_of : t -> Point.Constraint.t * Point.Set.t list
+
+  val constraints_for : kept:Point.Set.t -> t -> Point.Constraint.t
+
+  val domain : t -> Point.Set.t
+
+  val choose : (Point.t -> bool) -> t -> Point.t -> Point.t option
+
+  val sort : (int -> Point.t) -> Point.t list -> t -> t
+  (** [sort mk first g] builds a totally ordered graph. The output
+     graph should imply the input graph (and the implication will be
+     strict most of the time), but is not necessarily minimal. The
+     lowest points in the result are identified with [first].
+     Moreover, it adds levels [Type.n] to identify the points (not in
+     [first]) at level n. An artificial constraint (last first < mk
+     (length first)) is added to ensure that they are not merged.
+     Note: the result is unspecified if the input graph already
+     contains [mk n] nodes. *)
+
+  val pr : (Point.t -> Pp.t) -> t -> Pp.t
+
+  val dump : (constraint_type -> Point.t -> Point.t -> unit) -> t -> unit
+end