Generate names for anonymous polymorphic universes

This should make the univbinders output test less fragile as it
depends less on the global counter (still used for universes from
section variables).

3 files changed, 47 insertions, 3 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 2ad9e268c2..b0a4c8b738 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -173,6 +173,38 @@ let safe_gen f env sigma c =
 let safe_pr_lconstr_env = safe_gen pr_lconstr_env
 let safe_pr_constr_env = safe_gen pr_constr_env
 
+let u_ident = Id.of_string "u"
+
+let universe_binders_with_opt_names orig names =
+  let orig = Univ.AUContext.names orig in
+  let orig = Array.to_list orig in
+  let udecl = match names with
+  | None -> orig
+  | Some udecl ->
+    try
+      List.map2 (fun orig {CAst.v = na} ->
+          match na with
+          | Anonymous -> orig
+          | 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_named i ubind = function
+    | Name id -> Id.Map.add id (Univ.Level.var i) ubind
+    | Anonymous -> ubind
+  in
+  let ubind = List.fold_left_i fold_named 0 UnivNames.empty_binders udecl in
+  let fold_anons i (u_ident, ubind) = function
+    | Name _ -> u_ident, ubind
+    | Anonymous ->
+      let id = Namegen.next_ident_away_from u_ident (fun id -> Id.Map.mem id ubind) in
+      (id, Id.Map.add id (Univ.Level.var i) ubind)
+  in
+  let (_, ubind) = List.fold_left_i fold_anons 0 (u_ident, ubind) udecl in
+  ubind
+
 let pr_universe_ctx_set sigma c =
   if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
     fnl()++pr_in_comment (v 0 (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c))
diff --git a/printing/printer.mli b/printing/printer.mli
index 8c633b5e79..8805819890 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -132,6 +132,18 @@ val pr_universes  : evar_map ->
   ?variance:Univ.Variance.t array -> ?priv:Univ.ContextSet.t ->
   Declarations.universes -> Pp.t
 
+(** [universe_binders_with_opt_names ref l]
+
+    If [l] is [Some univs] return the universe binders naming the
+   bound levels of [ref] by [univs] (generating names for Anonymous).
+   May error if the lengths mismatch.
+
+    Otherwise return the bound universe names registered for [ref].
+
+    Inefficient on large contexts due to name generation. *)
+val universe_binders_with_opt_names : Univ.AUContext.t ->
+  UnivNames.univ_name_list option -> UnivNames.universe_binders
+
 (** Printing global references using names as short as possible *)
 
 val pr_global_env          : Id.Set.t -> GlobRef.t -> Pp.t
diff --git a/printing/printmod.ml b/printing/printmod.ml
index eec2fe86ac..9beac17546 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -118,7 +118,7 @@ let print_mutual_inductive env mind mib udecl =
     | BiFinite -> "Variant"
     | CoFinite -> "CoInductive"
   in
-  let bl = UnivNames.universe_binders_with_opt_names
+  let bl = Printer.universe_binders_with_opt_names
       (Declareops.inductive_polymorphic_context mib) udecl
   in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
@@ -151,7 +151,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 (Declareops.inductive_polymorphic_context mib)
+  let bl = Printer.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib)
       udecl
   in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
@@ -290,7 +290,7 @@ let print_body is_impl extent env mp (l,body) =
       (match extent with
          | OnlyNames -> mt ()
          | WithContents ->
-            let bl = UnivNames.universe_binders_with_opt_names ctx None in
+            let bl = Printer.universe_binders_with_opt_names ctx 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) ++