Store universe binder names as a mere list of names.

This is the only information we care about. The printing mechanism is only
called on polymorphic constants, as the naming of global monomorphic levels
is performed in another module.

4 files changed, 44 insertions, 59 deletions

diff --git a/engine/univNames.ml b/engine/univNames.ml
index 29d92c46ea..a4a08ff18e 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -53,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 : Name.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
@@ -68,25 +68,19 @@ let subst_ubinder (subst,(ref,l as orig)) =
 let discharge_ubinder (_,(ref,l)) =
   (** Expand polymorphic binders with the section context *)
   let info = Lib.section_segment_of_reference ref in
-  let sec_inst = info.Lib.abstr_subst in
-  let shift = Instance.length sec_inst in
-  let map lvl = match Level.var_index lvl with
-  | None -> lvl
-  | Some n -> Level.var (n + shift)
-  in
-  let l = Id.Map.map map l in
-  let fold i accu lvl = match Level.name lvl with
-  | None -> accu
+  let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in
+  let map i lvl = match Level.name lvl with
+  | None -> Anonymous
   | Some na ->
     try
       let qid = Nametab.shortest_qualid_of_universe na in
-      Id.Map.add (snd (Libnames.repr_qualid qid)) (Level.var i) accu
-    with Not_found -> accu
+      Name (snd (Libnames.repr_qualid qid))
+    with Not_found -> Anonymous
   in
-  let l = Array.fold_left_i fold l (Instance.to_array sec_inst) in
+  let l = List.mapi 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 * Name.t list -> Libobject.obj =
   let open Libobject in
   declare_object { (default_object "universe binder") with
     cache_function = cache_ubinder;
@@ -97,42 +91,37 @@ 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
-  in
-  let ubinders =
-    if Global.is_polymorphic ref then
-      (** FIXME: little dance to make the named universes refer to bound
-          universe variables *)
-      let univs = AUContext.instance (Global.universes_of_global ref) in
-      let fold i accu l = LMap.add l i accu in
-      let univs = Array.fold_left_i fold LMap.empty (Instance.to_array univs) in
-      let fold id lvl accu =
-        try Id.Map.add id (Level.var (LMap.find lvl univs)) accu
-        with Not_found -> accu
-      in
-      Id.Map.fold fold ubinders Id.Map.empty
-    else 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 Name (LMap.find lvl revmap)
+    with Not_found -> Anonymous
   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
+let universe_binders_with_opt_names ref names =
+  let udecl = match names with
   | None -> universe_binders_of_global ref
-  | 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
-      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
-        Pp.(str "Universe instance should have length " ++ int (List.length levels))
+  | Some udecl -> List.map (fun na -> na.CAst.v) udecl
+  in
+  let () =
+    try
+      let ctx = Global.universes_of_global ref in
+      let len = AUContext.size ctx in
+      if not (Option.is_empty names || Int.equal len (List.length udecl)) then
+        CErrors.user_err ~hdr:"universe_binders_with_opt_names"
+          Pp.(str "Universe instance should have length " ++ int len)
+    with Not_found -> ()
+  in
+  let fold i acc = function
+  | Anonymous -> acc
+  | Name 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] *)