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.

6 files changed, 53 insertions, 88 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] *)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 605c1ae957..66f748454d 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -73,8 +73,7 @@ let print_basename sp = pr_global (ConstRef sp)
 let print_ref reduce ref udecl =
   let typ, univs = Global.type_of_global_in_context (Global.env ()) ref in
   let inst = Univ.make_abstract_instance univs in
-  let bl = UnivNames.universe_binders_with_opt_names ref
-      (Array.to_list (Univ.Instance.to_array inst)) udecl in
+  let bl = UnivNames.universe_binders_with_opt_names ref udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let typ = EConstr.of_constr typ in
   let typ =
@@ -556,33 +555,23 @@ let print_constant with_values sep sp udecl =
   let cb = Global.lookup_constant sp in
   let val_0 = Global.body_of_constant_body cb in
   let typ = cb.const_type in
-  let univs, ulist =
+  let univs =
     let open Univ in
     let otab = Global.opaque_tables () in
     match cb.const_body with
-    | Undef _ | Def _ ->
-      begin
-        match cb.const_universes with
-        | Monomorphic_const ctx -> Monomorphic_const ctx, []
-        | Polymorphic_const ctx ->
-          let inst = make_abstract_instance ctx in
-          Polymorphic_const ctx,
-          Array.to_list (Instance.to_array inst)
-      end
+    | Undef _ | Def _ -> cb.const_universes
     | OpaqueDef o ->
       let body_uctxs = Opaqueproof.force_constraints otab o in
       match cb.const_universes with
       | Monomorphic_const ctx ->
-        Monomorphic_const (ContextSet.union body_uctxs ctx), []
+        Monomorphic_const (ContextSet.union body_uctxs ctx)
       | Polymorphic_const ctx ->
         assert(ContextSet.is_empty body_uctxs);
-        let inst = make_abstract_instance ctx in
-        Polymorphic_const ctx,
-        Array.to_list (Instance.to_array inst)
+        Polymorphic_const ctx
   in
   let ctx =
     UState.of_binders
-      (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
+      (UnivNames.universe_binders_with_opt_names (ConstRef sp) udecl)
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
diff --git a/printing/printmod.ml b/printing/printmod.ml
index f8d88aea07..1fc308ac99 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -119,14 +119,7 @@ let print_mutual_inductive env mind mib udecl =
     | BiFinite -> "Variant"
     | CoFinite -> "CoInductive"
   in
-  let univs =
-    let open Univ in
-    if Declareops.inductive_is_polymorphic mib then
-      Array.to_list (Instance.to_array
-                       (make_abstract_instance (Declareops.inductive_polymorphic_context mib)))
-    else []
-  in
-  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
+  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
          Printer.pr_cumulative
@@ -164,8 +157,7 @@ let print_record env mind mib udecl =
   let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
-  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0))
-      (Array.to_list (Univ.Instance.to_array u)) udecl in
+  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let keyword =
     let open Declarations in
@@ -304,8 +296,7 @@ let print_body is_impl env mp (l,body) =
       (match env with
 	  | None -> mt ()
 	  | Some env ->
-            let univs = Array.to_list (Univ.Instance.to_array (Univ.make_abstract_instance ctx)) in
-            let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) univs None in
+            let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) None in
             let sigma = Evd.from_ctx (UState.of_binders bl) in
 	    str " :" ++ spc () ++
             hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++