Merge PR #11977: Generate default names for bound universes of polymorphic definitions

Reviewed-by: ejgallego
Reviewed-by: herbelin

9 files changed, 73 insertions, 70 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index 25d7638686..d4cb59da26 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -114,12 +114,20 @@ let constraints ctx = snd ctx.local
 
 let context ctx = ContextSet.to_context ctx.local
 
+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 Name (LMap.find lvl revmap)
+    with Not_found -> Anonymous
+  in
+  Array.map map (Instance.to_array inst)
+
 let univ_entry ~poly uctx =
   let open Entries in
   if poly then
     let (binders, _) = uctx.names in
     let uctx = context uctx in
-    let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
+    let nas = compute_instance_binders (UContext.instance uctx) binders in
     Polymorphic_entry (nas, uctx)
   else Monomorphic_entry (context_set uctx)
 
@@ -433,7 +441,7 @@ let check_univ_decl ~poly uctx decl =
     if poly then
       let (binders, _) = uctx.names in
       let uctx = universe_context ~names ~extensible uctx in
-      let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
+      let nas = compute_instance_binders (UContext.instance uctx) binders in
       Entries.Polymorphic_entry (nas, uctx)
     else
       let () = check_universe_context_set ~names ~extensible uctx in
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6d9095680c..2e15558db2 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Names
 open Univ
 
@@ -30,43 +29,8 @@ let pr_with_global_universes l =
 
 (** Local universe names of polymorphic references *)
 
-type universe_binders = Univ.Level.t Names.Id.Map.t
+type universe_binders = Level.t Names.Id.Map.t
 
 let empty_binders = Id.Map.empty
 
-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 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 Name (LMap.find lvl revmap)
-    with Not_found -> Name (name_universe lvl)
-  in
-  Array.map map (Instance.to_array inst)
-
 type univ_name_list = Names.lname list
-
-let universe_binders_with_opt_names orig names =
-  let orig = 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 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 34a18d6b6e..5f69d199b3 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -19,15 +19,4 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 val empty_binders : universe_binders
 
-val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array
-
 type univ_name_list = Names.lname list
-
-(** [universe_binders_with_opt_names ref l]
-
-    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 the bound universe names registered for [ref]. *)
-val universe_binders_with_opt_names : AUContext.t ->
-  univ_name_list option -> universe_binders
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) ++
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 04514c15cb..edd2c9674f 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -37,10 +37,10 @@ Arguments wrap {A}%type_scope {Wrap}
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u *)
-foo@{u UnivBinders.18 v} = 
-Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,UnivBinders.18+1,v+1)}
-(* u UnivBinders.18 v |=  *)
+foo@{u u0 v} = 
+Type@{u0} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,u0+1,v+1)}
+(* u u0 v |=  *)
 Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
 (* {j i} |=  *)
@@ -76,10 +76,10 @@ foo@{E M N} =
 Type@{M} -> Type@{N} -> Type@{E}
      : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
-foo@{u UnivBinders.18 v} = 
-Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,UnivBinders.18+1,v+1)}
-(* u UnivBinders.18 v |=  *)
+foo@{u u0 v} = 
+Type@{u0} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,u0+1,v+1)}
+(* u u0 v |=  *)
 Inductive Empty@{E} : Type@{E} :=  
 (* E |=  *)
 Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
@@ -142,16 +142,14 @@ Applied.infunct@{u v} =
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
-axfoo@{i UnivBinders.58 UnivBinders.59} :
-Type@{UnivBinders.58} -> Type@{i}
-(* i UnivBinders.58 UnivBinders.59 |=  *)
+axfoo@{i u u0} : Type@{u} -> Type@{i}
+(* i u u0 |=  *)
 
 axfoo is universe polymorphic
 Arguments axfoo _%type_scope
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.58 UnivBinders.59} :
-Type@{UnivBinders.59} -> Type@{i}
-(* i UnivBinders.58 UnivBinders.59 |=  *)
+axbar@{i u u0} : Type@{u0} -> Type@{i}
+(* i u u0 |=  *)
 
 axbar is universe polymorphic
 Arguments axbar _%type_scope
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9d67ce3757..540d470fdc 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -957,7 +957,7 @@ let explain_not_match_error = function
     let pr_auctx auctx =
       let sigma = Evd.from_ctx
           (UState.of_binders
-             (UnivNames.universe_binders_with_opt_names auctx None))
+             (Printer.universe_binders_with_opt_names auctx None))
       in
       let uctx = AUContext.repr auctx in
       Printer.pr_universe_instance_constraints sigma
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index faf53d3fad..80e0b9987f 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -75,7 +75,7 @@ let print_ref reduce ref udecl =
   let env = Global.env () in
   let typ, univs = Typeops.type_of_global_in_context env ref in
   let inst = Univ.make_abstract_instance univs in
-  let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in
+  let bl = Printer.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let typ = EConstr.of_constr typ in
   let typ =
@@ -633,7 +633,7 @@ let print_constant with_values sep sp udecl =
   in
   let ctx =
     UState.of_binders
-      (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl)
+      (Printer.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl)
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in