From a2ec08199d023b102df7806db8ed1e71c3ed27ce Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 4 Dec 2018 16:22:18 +0100
Subject: Make ugraph implementation abstract wrt universe specifics

This should give better visibility of universe specific operations vs
generic graph operations.
---
 lib/acyclicGraph.mli | 73 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 73 insertions(+)
 create mode 100644 lib/acyclicGraph.mli

(limited to 'lib/acyclicGraph.mli')

diff --git a/lib/acyclicGraph.mli b/lib/acyclicGraph.mli
new file mode 100644
index 0000000000..8a2eb7098f
--- /dev/null
+++ b/lib/acyclicGraph.mli
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*         *   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 (Level:Point) : sig
+
+  type t
+
+  val empty : t
+
+  val check_invariants : required_canonical:(Level.t -> bool) -> t -> unit
+
+  exception AlreadyDeclared
+  val add : ?rank:int -> Level.t -> t -> t
+  (** Use a large [rank] to keep the node canonical *)
+
+  exception Undeclared of Level.t
+  val check_declared : t -> Level.Set.t -> unit
+
+  type 'a check_function = t -> 'a -> 'a -> bool
+
+  val check_eq : Level.t check_function
+  val check_leq : Level.t check_function
+  val check_lt : Level.t check_function
+
+  val enforce_eq : Level.t -> Level.t -> t -> t
+  val enforce_leq : Level.t -> Level.t -> t -> t
+  val enforce_lt : Level.t -> Level.t -> t -> t
+
+  val constraints_of : t -> Level.Constraint.t * Level.Set.t list
+
+  val constraints_for : kept:Level.Set.t -> t -> Level.Constraint.t
+
+  val domain : t -> Level.Set.t
+
+  val choose : (Level.t -> bool) -> t -> Level.t -> Level.t option
+
+  val sort : (int -> Level.t) -> Level.t list -> t -> t
+  (** [sort make_dummy points g] sorts [g]. The [points] are the first
+     in the result graph. If the graph is bigger than the list, the
+     rest is named according to [make_dummy]. *)
+
+  val pr : (Level.t -> Pp.t) -> t -> Pp.t
+
+  val dump : (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit
+end
-- 
cgit v1.2.3


From fb18cf6bf7d7142bf3fab3d7d811f2cecd527f12 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 5 Dec 2018 14:51:20 +0100
Subject: Remove universe specific terminology from acyclicgraph

This means removing [univ], [level] and derived abbreviations like
[lvl].

We keep using u, v for variable names as doing otherwise would be too
intrusive, and it's not overly universe specific.
---
 lib/acyclicGraph.mli | 48 +++++++++++++++++++++++++++---------------------
 1 file changed, 27 insertions(+), 21 deletions(-)

(limited to 'lib/acyclicGraph.mli')

diff --git a/lib/acyclicGraph.mli b/lib/acyclicGraph.mli
index 8a2eb7098f..13a12b51cd 100644
--- a/lib/acyclicGraph.mli
+++ b/lib/acyclicGraph.mli
@@ -29,45 +29,51 @@ module type Point = sig
   val pr : t -> Pp.t
 end
 
-module Make (Level:Point) : sig
+module Make (Point:Point) : sig
 
   type t
 
   val empty : t
 
-  val check_invariants : required_canonical:(Level.t -> bool) -> t -> unit
+  val check_invariants : required_canonical:(Point.t -> bool) -> t -> unit
 
   exception AlreadyDeclared
-  val add : ?rank:int -> Level.t -> t -> t
+  val add : ?rank:int -> Point.t -> t -> t
   (** Use a large [rank] to keep the node canonical *)
 
-  exception Undeclared of Level.t
-  val check_declared : t -> Level.Set.t -> unit
+  exception Undeclared of Point.t
+  val check_declared : t -> Point.Set.t -> unit
 
   type 'a check_function = t -> 'a -> 'a -> bool
 
-  val check_eq : Level.t check_function
-  val check_leq : Level.t check_function
-  val check_lt : Level.t check_function
+  val check_eq : Point.t check_function
+  val check_leq : Point.t check_function
+  val check_lt : Point.t check_function
 
-  val enforce_eq : Level.t -> Level.t -> t -> t
-  val enforce_leq : Level.t -> Level.t -> t -> t
-  val enforce_lt : Level.t -> Level.t -> t -> t
+  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 -> Level.Constraint.t * Level.Set.t list
+  val constraints_of : t -> Point.Constraint.t * Point.Set.t list
 
-  val constraints_for : kept:Level.Set.t -> t -> Level.Constraint.t
+  val constraints_for : kept:Point.Set.t -> t -> Point.Constraint.t
 
-  val domain : t -> Level.Set.t
+  val domain : t -> Point.Set.t
 
-  val choose : (Level.t -> bool) -> t -> Level.t -> Level.t option
+  val choose : (Point.t -> bool) -> t -> Point.t -> Point.t option
 
-  val sort : (int -> Level.t) -> Level.t list -> t -> t
-  (** [sort make_dummy points g] sorts [g]. The [points] are the first
-     in the result graph. If the graph is bigger than the list, the
-     rest is named according to [make_dummy]. *)
+  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 : (Level.t -> Pp.t) -> t -> Pp.t
+  val pr : (Point.t -> Pp.t) -> t -> Pp.t
 
-  val dump : (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit
+  val dump : (constraint_type -> Point.t -> Point.t -> unit) -> t -> unit
 end
-- 
cgit v1.2.3


From 1199cbc1a45e378e41f4b159c4c62db598173716 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 18 Dec 2018 10:53:31 +0100
Subject: Add comment to acyclicgraph API

---
 lib/acyclicGraph.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'lib/acyclicGraph.mli')

diff --git a/lib/acyclicGraph.mli b/lib/acyclicGraph.mli
index 13a12b51cd..b53a4c018f 100644
--- a/lib/acyclicGraph.mli
+++ b/lib/acyclicGraph.mli
@@ -39,10 +39,13 @@ module Make (Point:Point) : sig
 
   exception AlreadyDeclared
   val add : ?rank:int -> Point.t -> t -> t
-  (** Use a large [rank] to keep the node canonical *)
+  (** 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
 
-- 
cgit v1.2.3