From f71ef93aa21cd2ed4135588db3a5a3e8b42ceb39 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2020 14:01:00 +0200
Subject: Make explicit that UGraph lower bounds are only of two kinds.

This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.
---
 engine/uState.ml       | 14 +++++++++-----
 engine/uState.mli      |  6 +++---
 engine/univMinim.ml    |  8 ++++++--
 engine/univMinim.mli   |  2 +-
 engine/univops.mli     |  2 +-
 kernel/environ.ml      |  4 ++--
 kernel/environ.mli     |  6 +++---
 kernel/indTyping.ml    |  2 +-
 kernel/uGraph.ml       |  6 ++++++
 kernel/uGraph.mli      | 10 ++++++++--
 library/global.mli     |  2 +-
 vernac/comInductive.ml |  2 +-
 vernac/record.ml       |  2 +-
 13 files changed, 43 insertions(+), 23 deletions(-)

diff --git a/engine/uState.ml b/engine/uState.ml
index 00649ce042..99ac5f2ce8 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -34,7 +34,7 @@ type t =
    (** The subset of unification variables that can be instantiated with
         algebraic universes as they appear in inferred types only. *)
    uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
-   uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *)
+   uctx_universes_lbound : UGraph.Bound.t; (** The lower bound on universes (e.g. Set or Prop) *)
    uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
    uctx_weak_constraints : UPairSet.t
  }
@@ -48,7 +48,7 @@ let empty =
     uctx_univ_variables = LMap.empty;
     uctx_univ_algebraic = LSet.empty;
     uctx_universes = initial_sprop_cumulative;
-    uctx_universes_lbound = Univ.Level.set;
+    uctx_universes_lbound = UGraph.Bound.Set;
     uctx_initial_universes = initial_sprop_cumulative;
     uctx_weak_constraints = UPairSet.empty; }
 
@@ -443,6 +443,10 @@ let check_univ_decl ~poly uctx decl =
       (ContextSet.constraints uctx.uctx_local);
   ctx
 
+let is_bound l lbound = match lbound with
+| UGraph.Bound.Prop -> Level.is_prop l
+| UGraph.Bound.Set -> Level.is_set l
+
 let restrict_universe_context ~lbound (univs, csts) keep =
   let removed = LSet.diff univs keep in
   if LSet.is_empty removed then univs, csts
@@ -455,7 +459,7 @@ let restrict_universe_context ~lbound (univs, csts) keep =
   let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in
   let csts = UGraph.constraints_for ~kept:allkept g in
   let csts = Constraint.filter (fun (l,d,r) ->
-      not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
+      not ((is_bound l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
   (LSet.inter univs keep, csts)
 
 let restrict ctx vars =
@@ -600,10 +604,10 @@ let make_with_initial_binders ~lbound e us =
 
 let add_global_univ uctx u =
   let initial =
-    UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes
+    UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_initial_universes
   in
   let univs =
-    UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes
+    UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_universes
   in
   { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local;
                                      uctx_initial_universes = initial;
diff --git a/engine/uState.mli b/engine/uState.mli
index 6707826aae..533a501b59 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -25,9 +25,9 @@ type t
 
 val empty : t
 
-val make : lbound:Univ.Level.t -> UGraph.t -> t
+val make : lbound:UGraph.Bound.t -> UGraph.t -> t
 
-val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t
+val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
 
 val is_empty : t -> bool
 
@@ -90,7 +90,7 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
    the universes in [keep]. The constraints [csts] are adjusted so
    that transitive constraints between remaining universes (those in
    [keep] and those not in [univs]) are preserved. *)
-val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:UGraph.Bound.t -> ContextSet.t -> LSet.t -> ContextSet.t
 
 (** [restrict uctx ctx] restricts the local universes of [uctx] to
    [ctx] extended by local named universes and side effect universes
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index c05a7a800d..4dd7fe7e70 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -267,12 +267,16 @@ let minimize_univ_variables ctx us algs left right cstrs =
 module UPairs = OrderedType.UnorderedPair(Univ.Level)
 module UPairSet = Set.Make (UPairs)
 
+let is_bound l lbound = match lbound with
+| UGraph.Bound.Prop -> Level.is_prop l
+| UGraph.Bound.Set -> Level.is_set l
+
 (* TODO check is_small/sprop *)
 let normalize_context_set ~lbound g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (* Keep the Prop/Set <= i constraints separate for minimization *)
   let smallles, csts =
-    Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts
+    Constraint.partition (fun (l,d,r) -> d == Le && (is_bound l lbound || Level.is_sprop l)) csts
   in
   let smallles = if get_set_minimization ()
     then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles
@@ -299,7 +303,7 @@ let normalize_context_set ~lbound g ctx us algs weak =
   (* We ignore the trivial Prop/Set <= i constraints. *)
   let noneqs =
     Constraint.filter
-      (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) ||
+      (fun (l,d,r) -> not ((d == Le && is_bound l lbound) ||
                            (Level.is_prop l && d == Lt && Level.is_set r)))
       csts
   in
diff --git a/engine/univMinim.mli b/engine/univMinim.mli
index 2a46d87609..58853e47b8 100644
--- a/engine/univMinim.mli
+++ b/engine/univMinim.mli
@@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t)
     (a global one if there is one) and transitively saturate
     the constraints w.r.t to the equalities. *)
 
-val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t ->
+val normalize_context_set : lbound:UGraph.Bound.t -> UGraph.t -> ContextSet.t ->
   universe_opt_subst (* The defined and undefined variables *) ->
   LSet.t (* univ variables that can be substituted by algebraics *) ->
   UPairSet.t (* weak equality constraints *) ->
diff --git a/engine/univops.mli b/engine/univops.mli
index 02a731ad49..d0145f5643 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -15,5 +15,5 @@ open Univ
 val universes_of_constr : constr -> LSet.t
 [@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
 
-val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:UGraph.Bound.t -> ContextSet.t -> LSet.t -> ContextSet.t
 [@@ocaml.deprecated "Use [UState.restrict_universe_context]"]
diff --git a/kernel/environ.ml b/kernel/environ.ml
index d6d52dbc2b..182ed55d0e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -67,7 +67,7 @@ end
 type stratification = {
   env_universes : UGraph.t;
   env_sprop_allowed : bool;
-  env_universes_lbound : Univ.Level.t;
+  env_universes_lbound : UGraph.Bound.t;
   env_engagement : engagement
 }
 
@@ -129,7 +129,7 @@ let empty_env = {
   env_stratification = {
     env_universes = UGraph.initial_universes;
     env_sprop_allowed = true;
-    env_universes_lbound = Univ.Level.set;
+    env_universes_lbound = UGraph.Bound.Set;
     env_engagement = PredicativeSet };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 7a46538772..79e632daa0 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -62,7 +62,7 @@ end
 type stratification = {
   env_universes : UGraph.t;
   env_sprop_allowed : bool;
-  env_universes_lbound : Univ.Level.t;
+  env_universes_lbound : UGraph.Bound.t;
   env_engagement : engagement
 }
 
@@ -96,8 +96,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
 val empty_env : env
 
 val universes     : env -> UGraph.t
-val universes_lbound : env -> Univ.Level.t
-val set_universes_lbound : env -> Univ.Level.t -> env
+val universes_lbound : env -> UGraph.Bound.t
+val set_universes_lbound : env -> UGraph.Bound.t -> env
 val rel_context   : env -> Constr.rel_context
 val named_context : env -> Constr.named_context
 val named_context_val : env -> named_context_val
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 8ac96a6481..e9687991c0 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -321,7 +321,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
       if has_template_poly then
         (* For that particular case, we typecheck the inductive in an environment
            where the universes introduced by the definition are only [>= Prop] *)
-        let env = set_universes_lbound env Univ.Level.prop in
+        let env = set_universes_lbound env UGraph.Bound.Prop in
         push_context_set ~strict:false ctx env
       else
         (* In the regular case, all universes are [> Set] *)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5f5f0ef8cd..927db9e9e6 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -148,8 +148,14 @@ let enforce_leq_alg u v g =
   assert (check_leq g u v);
   cg
 
+module Bound =
+struct
+  type t = Prop | Set
+end
+
 exception AlreadyDeclared = G.AlreadyDeclared
 let add_universe u ~lbound ~strict g =
+  let lbound = match lbound with Bound.Prop -> Level.prop | Bound.Set -> Level.set in
   let graph = G.add u g.graph in
   let d = if strict then Lt else Le in
   enforce_constraint (lbound,d,u) {g with graph}
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 8d9afb0990..c9fbd7f694 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -48,7 +48,13 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
 
 exception AlreadyDeclared
 
-val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t
+module Bound :
+sig
+  type t = Prop | Set
+  (** The [Prop] bound is only used for template polymorphic inductive types. *)
+end
+
+val add_universe : Level.t -> lbound:Bound.t -> strict:bool -> t -> t
 
 (** Add a universe without (Prop,Set) <= u *)
 val add_universe_unconstrained : Level.t -> t -> t
@@ -86,7 +92,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t
 val domain : t -> LSet.t
 (** Known universes *)
 
-val check_subtype : lbound:Level.t -> AUContext.t check_function
+val check_subtype : lbound:Bound.t -> AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)
 
diff --git a/library/global.mli b/library/global.mli
index 2acd7e2a67..2767594171 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -22,7 +22,7 @@ val env : unit -> Environ.env
 val env_is_initial : unit -> bool
 
 val universes : unit -> UGraph.t
-val universes_lbound : unit -> Univ.Level.t
+val universes_lbound : unit -> UGraph.Bound.t
 val named_context_val : unit -> Environ.named_context_val
 val named_context : unit -> Constr.named_context
 
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index cc9b840bed..4242f06844 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -475,7 +475,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
   (* In case of template polymorphism, we need to compute more constraints *)
-  let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in
+  let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
 
   let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) =
     interp_params env0 udecl uparamsl paramsl
diff --git a/vernac/record.ml b/vernac/record.ml
index 9fda98d08e..36254780cd 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -121,7 +121,7 @@ let typecheck_params_and_fields def poly pl ps records =
      any Set <= i constraint for universes that might actually be instantiated with Prop. *)
   let is_template =
     List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
-  let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in
+  let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
   let () =
     let error bk {CAst.loc; v=name} =
-- 
cgit v1.2.3