From 404a041fce68b4f7072de0b91b4e136f04250482 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2020 13:23:05 +0100
Subject: Cosmetic cleaning of uState.ml and related: a bit of doc, more unity
 in naming.

Also some dead code.

If no typo is introduced, there should be no semantic changes.
---
 engine/uState.mli | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

(limited to 'engine/uState.mli')

diff --git a/engine/uState.mli b/engine/uState.mli
index 7fec03e3b2..bb26f0f821 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -23,25 +23,27 @@ type t
 
 (** {5 Constructors} *)
 
+(** Different ways to create a new universe state *)
+
 val empty : t
 
 val make : lbound:UGraph.Bound.t -> UGraph.t -> t
 
 val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
 
-val from_env : Environ.env -> t
-
-val is_empty : t -> bool
+val of_binders : UnivNames.universe_binders -> t
 
-val union : t -> t -> t
+val from_env : Environ.env -> t
 
 val of_context_set : Univ.ContextSet.t -> t
 
-val of_binders : UnivNames.universe_binders -> t
+(** Misc *)
 
-val universe_binders : t -> UnivNames.universe_binders
+val is_empty : t -> bool
+
+val union : t -> t -> t
 
-(** {5 Projections} *)
+(** {5 Projections and other destructors} *)
 
 val context_set : t -> Univ.ContextSet.t
 (** The local context of the state, i.e. a set of bound variables together
@@ -69,6 +71,9 @@ val context : t -> Univ.UContext.t
 val univ_entry : poly:bool -> t -> Entries.universes_entry
 (** Pick from {!context} or {!context_set} based on [poly]. *)
 
+val universe_binders : t -> UnivNames.universe_binders
+(** Return names of universes, inventing names if needed *)
+
 (** {5 Constraints handling} *)
 
 val add_constraints : t -> Univ.Constraint.t -> t
@@ -115,7 +120,7 @@ val emit_side_effects : Safe_typing.private_constants -> t -> t
 val demote_global_univs : Environ.env -> t -> t
 (** Removes from the uctx_local part of the UState the universes and constraints
     that are present in the universe graph in the input env (supposedly the
-    global ones *)
+    global ones) *)
 
 val demote_seff_univs : Univ.LSet.t -> t -> t
 (** Mark the universes as not local any more, because they have been
@@ -123,6 +128,11 @@ val demote_seff_univs : Univ.LSet.t -> t -> t
    emit_side_effects instead. *)
 
 val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
+(** Declare a new local universe; use rigid if a global or bound
+    universe; use flexible for a universe existential variable; use
+    univ_flexible_alg for a universe existential variable allowed to
+    be instantiated with an algebraic universe *)
+
 val add_global_univ : t -> Univ.Level.t -> t
 
 (** [make_flexible_variable g algebraic l]
-- 
cgit v1.2.3


From 4814c482eb83f4c21b6ecf2b1b9235b513221181 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2020 14:34:17 +0100
Subject: Factorizing UState.make* through UState.from_env, to highlight the
 similarity.

An alternative could also be to split the initialization of the
environment and the declaration of initial "binders".
---
 engine/uState.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'engine/uState.mli')

diff --git a/engine/uState.mli b/engine/uState.mli
index bb26f0f821..d79447f6a9 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -28,12 +28,14 @@ type t
 val empty : t
 
 val make : lbound:UGraph.Bound.t -> UGraph.t -> t
+[@@ocaml.deprecated "Use from_env"]
 
 val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
+[@@ocaml.deprecated "Use from_env"]
 
 val of_binders : UnivNames.universe_binders -> t
 
-val from_env : Environ.env -> t
+val from_env : ?binders:lident list -> Environ.env -> t
 
 val of_context_set : Univ.ContextSet.t -> t
 
-- 
cgit v1.2.3


From e7b39c73f48279980f8ea2238632bfbf6e3d4178 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2020 14:56:19 +0100
Subject: Documentation of the main entry points of uState.mli.

---
 engine/uState.mli | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'engine/uState.mli')

diff --git a/engine/uState.mli b/engine/uState.mli
index d79447f6a9..bd3aac0d8b 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -33,11 +33,16 @@ val make : lbound:UGraph.Bound.t -> UGraph.t -> t
 val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
 [@@ocaml.deprecated "Use from_env"]
 
-val of_binders : UnivNames.universe_binders -> t
-
 val from_env : ?binders:lident list -> Environ.env -> t
+(** Main entry point at the beginning of a declaration declaring the
+    binding names as rigid universes. *)
+
+val of_binders : UnivNames.universe_binders -> t
+(** Main entry point when only names matter, e.g. for printing. *)
 
 val of_context_set : Univ.ContextSet.t -> t
+(** Main entry point when starting from the instance of a global
+    reference, e.g. when building a scheme. *)
 
 (** Misc *)
 
-- 
cgit v1.2.3