Merge PR #8585: Simplify declaration of universe names

3 files changed, 46 insertions, 51 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index f4e57073cc..07a0066ea8 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -477,20 +477,7 @@ type universe_source =
   | QualifiedUniv of Id.t (* global universe introduced by some global value *)
   | UnqualifiedUniv (* other global universe *)
 
-type universe_decl = universe_source * Nametab.universe_id
-
-let add_universe src (dp, i) =
-  let level = Univ.Level.make dp i in
-  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;
-      if poly then Lib.add_section_context ctx)
-    optpoly
+type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list
 
 let check_exists sp =
   let depth = sections_depth () in
@@ -499,41 +486,42 @@ let check_exists sp =
     alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
   else ()
 
-let qualify_univ src (sp,i as orig) =
+let qualify_univ i sp src id =
+  let open Libnames in
   match src with
-  | BoundUniv | UnqualifiedUniv -> orig
+  | BoundUniv | UnqualifiedUniv ->
+    let sp = dirpath sp in
+    i, make_path sp id
   | 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 i) sp id in
-    add_universe src 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 src 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
-  ()
-
-let discharge_universe = function
+    let sp = dirpath sp in
+    let sp = DirPath.repr sp in
+    Nametab.map_visibility succ i, make_path (DirPath.make (l::sp)) id
+
+let do_univ_name ~check i sp src (id,univ) =
+  let i, sp = qualify_univ i sp src id in
+  if check then check_exists sp;
+  Nametab.push_universe i sp univ
+
+let cache_univ_names ((sp, _), (src, univs)) =
+  List.iter (do_univ_name ~check:true (Nametab.Until 1) sp src) univs
+
+let load_univ_names i ((sp, _), (src, univs)) =
+  List.iter (do_univ_name ~check:false (Nametab.Until i) sp src) univs
+
+let open_univ_names i ((sp, _), (src, univs)) =
+  List.iter (do_univ_name ~check:false (Nametab.Exactly i) sp src) univs
+
+let discharge_univ_names = function
   | _, (BoundUniv, _) -> None
   | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
 
-let input_universe : universe_decl -> Libobject.obj =
+let input_univ_names : universe_name_decl -> Libobject.obj =
   declare_object
     { (default_object "Global universe name state") with
-      cache_function = cache_universe;
-      load_function = load_universe;
-      open_function = open_universe;
-      discharge_function = discharge_universe;
+      cache_function = cache_univ_names;
+      load_function = load_univ_names;
+      open_function = open_univ_names;
+      discharge_function = discharge_univ_names;
       subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
       classify_function = (fun a -> Substitute a) }
 
@@ -549,12 +537,12 @@ let declare_univ_binders gr pl =
         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 univs = Id.Map.fold (fun id univ univs ->
+        match Univ.Level.name univ with
+        | None -> assert false (* having Prop/Set/Var as binders is nonsense *)
+        | Some univ -> (id,univ)::univs) pl []
+    in
+    Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
 
 let do_universe poly l =
   let in_section = Lib.sections_are_opened () in
@@ -568,10 +556,12 @@ let do_universe poly l =
       let lev = UnivGen.new_univ_id () in
       (id, lev)) l
   in
+  let ctx = List.fold_left (fun ctx (_,(dp,i)) -> Univ.LSet.add (Univ.Level.make dp i) ctx)
+      Univ.LSet.empty l, Univ.Constraint.empty
+  in
+  let () = declare_universe_context poly ctx in
   let src = if poly then BoundUniv else UnqualifiedUniv in
-  List.iter (fun (id,lev) ->
-      ignore(Lib.add_leaf id (input_universe (src, lev))))
-    l
+  Lib.add_anonymous_leaf (input_univ_names (src, l))
 
 let do_constraint poly l =
   let open Univ in
diff --git a/library/nametab.ml b/library/nametab.ml
index 840cf8e380..06ace373c3 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -30,6 +30,9 @@ let error_global_not_found qid =
 *)
 type visibility = Until of int | Exactly of int
 
+let map_visibility f = function
+  | Until i -> Until (f i)
+  | Exactly i -> Exactly (f i)
 
 (* Data structure for nametabs *******************************************)
 
diff --git a/library/nametab.mli b/library/nametab.mli
index 57e9141db9..1c3322bfb1 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -75,6 +75,8 @@ val error_global_not_found : qualid -> 'a
 
 type visibility = Until of int | Exactly of int
 
+val map_visibility : (int -> int) -> visibility -> visibility
+
 val push : visibility -> full_path -> GlobRef.t -> unit
 val push_modtype : visibility -> full_path -> ModPath.t -> unit
 val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit