Merge PR #13552: Delay inventing names for monomorphic universes

Reviewed-by: ppedrot

6 files changed, 73 insertions, 41 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index 0c994dfea0..20ea24dd87 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -113,19 +113,18 @@ let constraints uctx = snd uctx.local
 let context uctx = ContextSet.to_context uctx.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
+    try Name (Option.get (LMap.find lvl ubinders).uname)
+    with Option.IsNone | 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 (_, rbinders) = uctx.names in
     let uctx = context uctx in
-    let nas = compute_instance_binders (UContext.instance uctx) binders in
+    let nas = compute_instance_binders (UContext.instance uctx) rbinders in
     Polymorphic_entry (nas, uctx)
   else Monomorphic_entry (context_set uctx)
 
@@ -158,23 +157,8 @@ let of_binders names =
   in
   { empty with names = (names, rev_map) }
 
-let invent_name (named,cnt) u =
-  let rec aux i =
-    let na = Id.of_string ("u"^(string_of_int i)) in
-    if Id.Map.mem na named then aux (i+1)
-    else Id.Map.add na u named, i+1
-  in
-  aux cnt
-
 let universe_binders uctx =
-  let named, rev = uctx.names in
-  let named, _ = LSet.fold (fun u named ->
-      match LMap.find u rev with
-      | exception Not_found -> (* not sure if possible *) invent_name named u
-      | { uname = None } -> invent_name named u
-      | { uname = Some _ } -> named)
-      (ContextSet.levels uctx.local) (named, 0)
-  in
+  let named, _ = uctx.names in
   named
 
 let instantiate_variable l b v =
@@ -447,9 +431,9 @@ let check_univ_decl ~poly uctx decl =
   let names = decl.univdecl_instance in
   let extensible = decl.univdecl_extensible_instance in
   if poly then
-    let (binders, _) = uctx.names in
+    let (_, rbinders) = uctx.names in
     let uctx = universe_context ~names ~extensible uctx in
-    let nas = compute_instance_binders (UContext.instance uctx) binders in
+    let nas = compute_instance_binders (UContext.instance uctx) rbinders in
     Entries.Polymorphic_entry (nas, uctx)
   else
     let () = check_universe_context_set ~names ~extensible uctx in
diff --git a/engine/uState.mli b/engine/uState.mli
index 442c29180c..9cff988c99 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -79,7 +79,7 @@ val univ_entry : poly:bool -> t -> Entries.universes_entry
 (** Pick from {!context} or {!context_set} based on [poly]. *)
 
 val universe_binders : t -> UnivNames.universe_binders
-(** Return names of universes, inventing names if needed *)
+(** Return local names of universes. *)
 
 (** {5 Constraints handling} *)
 
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 0fbb4f4c11..95b6c6ee95 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -162,6 +162,9 @@ When declaring multiple axioms in one command, only the first is allowed a unive
 foo@{i} = Type@{M.i} -> Type@{i}
      : Type@{max(M.i+1,i+1)}
 (* i |=  *)
+Type@{u0} -> Type@{UnivBinders.64}
+     : Type@{max(u0+1,UnivBinders.64+1)}
+(* {UnivBinders.64} |=  *)
 bind_univs.mono = 
 Type@{bind_univs.mono.u}
      : Type@{bind_univs.mono.u+1}
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index ed6e90b2a6..9539e34cfe 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -161,6 +161,16 @@ Module Notas.
 
 End Notas.
 
+Module NoAutoNames.
+  Monomorphic Universe u0.
+
+  (* The anonymous universe doesn't get a name (names are only
+     invented at the end of a definition/inductive) so no need to
+     qualify u0. *)
+  Check (Type@{u0} -> Type).
+
+End NoAutoNames.
+
 (* Universe binders survive through compilation, sections and modules. *)
 Require TestSuite.bind_univs.
 Print bind_univs.mono.
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 1987d48e0f..834ef0d29a 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -9,6 +9,8 @@
 (************************************************************************)
 
 open Names
+open Declarations
+open Univ
 
 (* object_kind , id *)
 exception AlreadyDeclared of (string option * Id.t)
@@ -72,23 +74,51 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
       subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
       classify_function = (fun a -> Substitute a) }
 
+let invent_name (named,cnt) u =
+  let rec aux i =
+    let na = Id.of_string ("u"^(string_of_int i)) in
+    if Id.Map.mem na named then aux (i+1)
+    else na, (Id.Map.add na u named, i+1)
+  in
+  aux cnt
+
+let label_and_univs_of = let open GlobRef in function
+    | ConstRef c ->
+      let l = Label.to_id @@ Constant.label c in
+      let univs = (Global.lookup_constant c).const_universes in
+      l, univs
+    | IndRef (c,_) ->
+      let l = Label.to_id @@ MutInd.label c in
+      let univs = (Global.lookup_mind c).mind_universes in
+      l, univs
+    | VarRef id ->
+      CErrors.anomaly ~label:"declare_univ_binders"
+        Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
+    | ConstructRef _ ->
+      CErrors.anomaly ~label:"declare_univ_binders"
+        Pp.(str "declare_univ_binders on a constructor reference")
+
 let declare_univ_binders gr pl =
-  if Global.is_polymorphic gr then
-    ()
-  else
-    let l = let open GlobRef in match gr with
-      | ConstRef c -> Label.to_id @@ Constant.label c
-      | IndRef (c, _) -> Label.to_id @@ MutInd.label c
-      | VarRef id ->
-        CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
-      | ConstructRef _ ->
-        CErrors.anomaly ~label:"declare_univ_binders"
-          Pp.(str "declare_univ_binders on a constructor reference")
+  let l, univs = label_and_univs_of gr in
+  match univs with
+  | Polymorphic _ -> ()
+  | Monomorphic (levels,_) ->
+    (* First the explicitly named universes *)
+    let named, univs = Id.Map.fold (fun id univ (named,univs) ->
+        let univs = match Univ.Level.name univ with
+          | None -> assert false (* having Prop/Set/Var as binders is nonsense *)
+          | Some univ -> (id,univ)::univs
+        in
+        let named = LSet.add univ named in
+        named, univs)
+        pl (LSet.empty,[])
     in
-    let univs = Id.Map.fold (fun id univ univs ->
-        match Univ.Level.name univ with
-        | None -> assert false (* having Prop/Set/Var as binders is nonsense *)
-        | Some univ -> (id,univ)::univs) pl []
+    (* then invent names for the rest *)
+    let _, univs = LSet.fold (fun univ (aux,univs) ->
+        let id, aux = invent_name aux univ in
+        let univ = Option.get (Level.name univ) in
+        aux, (id,univ) :: univs)
+        (LSet.diff levels named) ((pl,0),univs)
     in
     Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
 
diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli
index ca990a58eb..a7e942be5a 100644
--- a/vernac/declareUniv.mli
+++ b/vernac/declareUniv.mli
@@ -10,11 +10,16 @@
 
 open Names
 
-(* object_kind , id *)
+(** Also used by [Declare] for constants, [DeclareInd] for inductives, etc.
+    Containts [object_kind , id]. *)
 exception AlreadyDeclared of (string option * Id.t)
 
-(** Global universe contexts, names and constraints *)
+(** Internally used to declare names of universes from monomorphic
+   constants/inductives. Noop on polymorphic references. *)
 val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
 
+(** Command [Universes]. *)
 val do_universe : poly:bool -> lident list -> unit
+
+(** Command [Constraint]. *)
 val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit