Merge PR #8475: Centralize the reliance on abstract universe context internals

4 files changed, 54 insertions, 32 deletions

diff --git a/engine/univNames.ml b/engine/univNames.ml
index e861913de2..9e4c6e47fc 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Util
 open Names
 open Univ
 open Nametab
@@ -52,10 +53,10 @@ let empty_binders = Id.Map.empty
 
 let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders"
 
-let universe_binders_of_global ref : universe_binders =
+let universe_binders_of_global ref : Id.t list =
   try
     let l = GlobRef.Map.find ref !universe_binders_table in l
-  with Not_found -> Names.Id.Map.empty
+  with Not_found -> []
 
 let cache_ubinder (_,(ref,l)) =
   universe_binders_table := GlobRef.Map.add ref l !universe_binders_table
@@ -64,10 +65,28 @@ let subst_ubinder (subst,(ref,l as orig)) =
   let ref' = fst (Globnames.subst_global subst ref) in
   if ref == ref' then orig else ref', l
 
+let name_universe lvl =
+  (** Best-effort naming from the string representation of the level. This is
+      completely hackish and should be solved in upper layers instead. *)
+  Id.of_string_soft (Level.to_string lvl)
+
 let discharge_ubinder (_,(ref,l)) =
+  (** Expand polymorphic binders with the section context *)
+  let info = Lib.section_segment_of_reference ref in
+  let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in
+  let map lvl = match Level.name lvl with
+    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+      assert false
+    | Some na ->
+      try
+        let qid = Nametab.shortest_qualid_of_universe na in
+        snd (Libnames.repr_qualid qid)
+      with Not_found -> name_universe lvl
+  in
+  let l = List.map map sec_inst @ l in
   Some (Lib.discharge_global ref, l)
 
-let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
+let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj =
   let open Libobject in
   declare_object { (default_object "universe binder") with
     cache_function = cache_ubinder;
@@ -78,28 +97,35 @@ let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
     rebuild_function = (fun x -> x); }
 
 let register_universe_binders ref ubinders =
-  (* Add the polymorphic (section) universes *)
-  let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
-    let qid = Nametab.shortest_qualid_of_universe lvl in
-    let level = Level.make (fst lvl) (snd lvl) in
-    if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
-    else ubinders)
-    !universe_map ubinders
+  (** TODO: change the API to register a [Name.t list] instead. This is the last
+      part of the code that depends on the internal representation of names in
+      abstract contexts, but removing it requires quite a rework of the
+      callers. *)
+  let univs = AUContext.instance (Global.universes_of_global ref) in
+  let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
+  let map lvl =
+    try LMap.find lvl revmap
+    with Not_found -> name_universe lvl
   in
-  if not (Id.Map.is_empty ubinders)
-  then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
+  let ubinders = Array.map_to_list map (Instance.to_array univs) in
+  if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders))
 
 type univ_name_list = Names.lname list
 
-let universe_binders_with_opt_names ref levels = function
-  | None -> universe_binders_of_global ref
+let universe_binders_with_opt_names ref names =
+  let orig = universe_binders_of_global ref in
+  let udecl = match names with
+  | None -> orig
   | Some udecl ->
-    if Int.equal(List.length levels) (List.length udecl)
-    then
-      List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
-          | Anonymous -> acc
-          | Name na -> Names.Id.Map.add na lvl acc)
-        empty_binders udecl levels
-    else
+    try
+      List.map2 (fun orig {CAst.v = na} ->
+          match na with
+          | Anonymous -> orig
+          | Name id -> id) orig udecl
+    with Invalid_argument _ ->
+      let len = List.length orig in
       CErrors.user_err ~hdr:"universe_binders_with_opt_names"
-        Pp.(str "Universe instance should have length " ++ int (List.length levels))
+        Pp.(str "Universe instance should have length " ++ int len)
+  in
+  let fold i acc na = Names.Id.Map.add na (Level.var i) acc in
+  List.fold_left_i fold 0 empty_binders udecl
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 837beac267..d794d7b744 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -27,15 +27,14 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 val empty_binders : universe_binders
 
 val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
-val universe_binders_of_global : Names.GlobRef.t -> universe_binders
 
 type univ_name_list = Names.lname list
 
-(** [universe_binders_with_opt_names ref u l]
+(** [universe_binders_with_opt_names ref l]
 
-    If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
-    May error if the lengths mismatch.
+    If [l] is [Some univs] return the universe binders naming the bound levels
+    of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch.
 
-    Otherwise return [universe_binders_of_global ref]. *)
+    Otherwise return the bound universe names registered for [ref]. *)
 val universe_binders_with_opt_names : Names.GlobRef.t ->
-  Univ.Level.t list -> univ_name_list option -> universe_binders
+  univ_name_list option -> universe_binders
diff --git a/engine/universes.ml b/engine/universes.ml
index ee9668433c..c7e5f654a1 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -26,7 +26,6 @@ let is_polymorphic = UnivNames.is_polymorphic
 let empty_binders = UnivNames.empty_binders
 
 let register_universe_binders = UnivNames.register_universe_binders
-let universe_binders_of_global = UnivNames.universe_binders_of_global
 
 let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names
 
diff --git a/engine/universes.mli b/engine/universes.mli
index ad937471e9..7ca33f47a1 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -39,14 +39,12 @@ val empty_binders : universe_binders
 
 val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
 [@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"]
-val universe_binders_of_global : Globnames.global_reference -> universe_binders
-[@@ocaml.deprecated "Use [UnivNames.universe_binders_of_global]"]
 
 type univ_name_list = UnivNames.univ_name_list
 [@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
 
 val universe_binders_with_opt_names : Globnames.global_reference ->
-  Univ.Level.t list -> univ_name_list option -> universe_binders
+  univ_name_list option -> universe_binders
 [@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"]
 
 (** ****** Deprecated: moved to [UnivGen] *)