Merge PR #8601: Move bound universe names to abstract contexts

3 files changed, 29 insertions, 56 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index aa7ec63a6f..41905feab7 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -101,13 +101,21 @@ let context ctx = Univ.ContextSet.to_context ctx.uctx_local
 
 let const_univ_entry ~poly uctx =
   let open Entries in
-  if poly then Polymorphic_const_entry (context uctx)
+  if poly then
+    let (binders, _) = uctx.uctx_names in
+    let uctx = context uctx in
+    let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+    Polymorphic_const_entry (nas, uctx)
   else Monomorphic_const_entry (context_set uctx)
 
 (* does not support cumulativity since you need more info *)
 let ind_univ_entry ~poly uctx =
   let open Entries in
-  if poly then Polymorphic_ind_entry (context uctx)
+  if poly then
+    let (binders, _) = uctx.uctx_names in
+    let uctx = context uctx in
+    let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+    Polymorphic_ind_entry (nas, uctx)
   else Monomorphic_ind_entry (context_set uctx)
 
 let of_context_set ctx = { empty with uctx_local = ctx }
@@ -394,8 +402,11 @@ let check_univ_decl ~poly uctx decl =
   let ctx =
     let names = decl.univdecl_instance in
     let extensible = decl.univdecl_extensible_instance in
-    if poly
-    then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx)
+    if poly then
+      let (binders, _) = uctx.uctx_names in
+      let uctx = universe_context ~names ~extensible uctx in
+      let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+      Entries.Polymorphic_const_entry (nas, uctx)
     else
       let () = check_universe_context_set ~names ~extensible uctx in
       Entries.Monomorphic_const_entry uctx.uctx_local
diff --git a/engine/univNames.ml b/engine/univNames.ml
index a71f9c5736..ad91d31f87 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -36,69 +36,28 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 let empty_binders = Id.Map.empty
 
-let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"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 -> []
-
-let cache_ubinder (_,(ref,l)) =
-  universe_binders_table := GlobRef.Map.add ref l !universe_binders_table
-
-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 universe_binders_of_global ref : Name.t array =
+  try AUContext.names (Environ.universes_of_global (Global.env ()) ref)
+  with Not_found -> [||]
 
 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 (ref, l)
-
-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;
-    load_function = (fun _ x -> cache_ubinder x);
-    classify_function = (fun x -> Substitute x);
-    subst_function = subst_ubinder;
-    discharge_function = discharge_ubinder;
-    rebuild_function = (fun x -> x); }
-
-let register_universe_binders ref 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 (Environ.universes_of_global (Global.env()) ref) in
+let compute_instance_binders inst ubinders =
   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
+    try Name (LMap.find lvl revmap)
+    with Not_found -> Name (name_universe lvl)
   in
-  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))
+  Array.map map (Instance.to_array inst)
 
 type univ_name_list = Names.lname list
 
 let universe_binders_with_opt_names ref names =
   let orig = universe_binders_of_global ref in
+  let orig = Array.to_list orig in
   let udecl = match names with
   | None -> orig
   | Some udecl ->
@@ -106,11 +65,14 @@ let universe_binders_with_opt_names ref names =
       List.map2 (fun orig {CAst.v = na} ->
           match na with
           | Anonymous -> orig
-          | Name id -> id) orig udecl
+          | Name id -> Name 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 len)
   in
-  let fold i acc na = Names.Id.Map.add na (Level.var i) acc in
+  let fold i acc na = match na with
+  | Name id -> Names.Id.Map.add id (Level.var i) acc
+  | Anonymous -> acc
+  in
   List.fold_left_i fold 0 empty_binders udecl
diff --git a/engine/univNames.mli b/engine/univNames.mli
index bd4062ade4..dc669f45d6 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -19,7 +19,7 @@ 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 compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array
 
 type univ_name_list = Names.lname list