Cleanup API for registering universe binders.

- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.

  E.g mono@{i} := Type@{i} is printed as
  mono@{mono.i} := Type@{mono.i}.

  There can be a name clash if there's a module and a constant of the
  same name. It is detected and is an error if the constant is first
  but is not detected and the name for the constant not
  registered (??) if the constant comes second.

Accept VarRef when registering universe binders

Fix two problems found by Gaëtan where binders were not registered properly

Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs

Fix an issue of the stronger restrict universe context + no evd leak

This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.

1 files changed, 65 insertions, 18 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 8fc959b0f..1aeb67afb 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -458,33 +458,61 @@ let declare_universe_context poly ctx =
    used to distinguish universes declared in polymorphic sections, which
    are discharged and do not remain in scope. *)
 
-type universe_decl = polymorphic * Nametab.universe_id
+type universe_source =
+  | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *)
+  | QualifiedUniv of Id.t (* global universe introduced by some global value *)
+  | UnqualifiedUniv (* other global universe *)
 
-let add_universe p (dp, i) =
+type universe_decl = universe_source * Nametab.universe_id
+
+let add_universe src (dp, i) =
   let level = Univ.Level.make dp i in
-  let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
-  Global.push_context_set p ctx;
-  Universes.add_global_universe level p;
-  if p then Lib.add_section_context ctx
+  let optpoly = match src with
+    | BoundUniv -> Some true
+    | UnqualifiedUniv -> Some false
+    | QualifiedUniv _ -> None
+  in
+  Option.iter (fun poly ->
+      let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
+      Global.push_context_set poly ctx;
+      Universes.add_global_universe level poly;
+      if poly then Lib.add_section_context ctx)
+    optpoly
 
 let check_exists sp =
   let depth = sections_depth () in
   let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in
-  if Nametab.exists_universe sp then alreadydeclared (Id.print (basename sp) ++ str " already exists")
+  if Nametab.exists_universe sp then
+    alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
   else ()
 
-let cache_universe ((sp, _), (poly, id)) =
+let qualify_univ src (sp,i as orig) =
+  match src with
+  | BoundUniv | UnqualifiedUniv -> orig
+  | QualifiedUniv l ->
+    let sp0, id = Libnames.repr_path sp in
+    let sp0 = DirPath.repr sp0 in
+    Libnames.make_path (DirPath.make (l::sp0)) id, i+1
+
+let cache_universe ((sp, _), (src, id)) =
+  let sp, i = qualify_univ src (sp,1) in
   let () = check_exists sp in
-  let () = Nametab.push_universe (Nametab.Until 1) sp id in
-    add_universe poly id
+  let () = Nametab.push_universe (Nametab.Until i) sp id in
+    add_universe src id
 
-let load_universe i ((sp, _), (poly, id)) =
+let load_universe i ((sp, _), (src, id)) =
+  let sp, i = qualify_univ src (sp,i) in
   let () = Nametab.push_universe (Nametab.Until i) sp id in
-  add_universe poly id
+  add_universe src id
 
-let open_universe i ((sp, _), (poly, id)) =
+let open_universe i ((sp, _), (src, id)) =
+  let sp, i = qualify_univ src (sp,i) in
   let () = Nametab.push_universe (Nametab.Exactly i) sp id in
-  ()(** add_universe p id Necessary ? *)
+  ()
+
+let discharge_universe = function
+  | _, (BoundUniv, _) -> None
+  | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
 
 let input_universe : universe_decl -> Libobject.obj =
   declare_object
@@ -492,12 +520,28 @@ let input_universe : universe_decl -> Libobject.obj =
       cache_function = cache_universe;
       load_function = load_universe;
       open_function = open_universe;
-      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
+      discharge_function = discharge_universe;
       subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
       classify_function = (fun a -> Substitute a) }
 
-let add_universe poly (id, lev) =
-  ignore(Lib.add_leaf id (input_universe (poly, lev)))
+let declare_univ_binders gr pl =
+  if Global.is_polymorphic gr then
+    Universes.register_universe_binders gr pl
+  else
+    let l = match gr with
+      | ConstRef c -> Label.to_id @@ Constant.label c
+      | IndRef (c, _) -> Label.to_id @@ MutInd.label c
+      | VarRef id -> id
+      | ConstructRef _ ->
+        anomaly ~label:"declare_univ_binders"
+          Pp.(str "declare_univ_binders on an constructor reference")
+    in
+    Id.Map.iter (fun id lvl ->
+        match Univ.Level.name lvl with
+        | None -> ()
+        | Some na ->
+          ignore (Lib.add_leaf id (input_universe (QualifiedUniv l, na))))
+      pl
 
 let do_universe poly l =
   let in_section = Lib.sections_are_opened () in
@@ -511,7 +555,10 @@ let do_universe poly l =
       let lev = Universes.new_univ_id () in
       (id, lev)) l
   in
-  List.iter (add_universe poly) l
+  let src = if poly then BoundUniv else UnqualifiedUniv in
+  List.iter (fun (id,lev) ->
+      ignore(Lib.add_leaf id (input_universe (src, lev))))
+    l
 
 type constraint_decl = polymorphic * Univ.constraints