Separate interning and pretyping of universes

This allows proper treatment in notations, ie fixes #13303

The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).

This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:

~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~

When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.

Extern has a symmetrical problem:

~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)

Therefore extern also takes a universe binders argument.

Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)

As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.

Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.

4 files changed, 19 insertions, 12 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index 103b552d86..0c994dfea0 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -341,12 +341,16 @@ let constrain_variables diff uctx =
   in
   { uctx with local = (univs, local); univ_variables = vars }
 
-let qualid_of_level uctx =
+let id_of_level uctx l =
+  try Some (Option.get (LMap.find l (snd uctx.names)).uname)
+  with Not_found | Option.IsNone ->
+    None
+
+let qualid_of_level uctx l =
   let map, map_rev = uctx.names in
-    fun l ->
-      try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
-      with Not_found | Option.IsNone ->
-        UnivNames.qualid_of_level l
+  try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
+  with Not_found | Option.IsNone ->
+    UnivNames.qualid_of_level map l
 
 let pr_uctx_level uctx l =
   match qualid_of_level uctx l with
diff --git a/engine/uState.mli b/engine/uState.mli
index bd3aac0d8b..442c29180c 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -209,4 +209,7 @@ val update_sigma_univs : t -> UGraph.t -> t
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
 val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
 
+(** Only looks in the local names, not in the nametab. *)
+val id_of_level : t -> Univ.Level.t -> Id.t option
+
 val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 2e15558db2..f5542cc0f7 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -12,15 +12,15 @@ open Names
 open Univ
 
 
-let qualid_of_level l =
+let qualid_of_level ctx l =
   match Level.name l with
   | Some qid  ->
-    (try Some (Nametab.shortest_qualid_of_universe qid)
+    (try Some (Nametab.shortest_qualid_of_universe (Id.Map.domain ctx) qid)
      with Not_found -> None)
   | None -> None
 
-let pr_with_global_universes l =
-  match qualid_of_level l with
+let pr_with_global_universes ctx l =
+  match qualid_of_level ctx l with
   | Some qid  -> Libnames.pr_qualid qid
   | None -> Level.pr l
 
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 5f69d199b3..875c043032 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -10,9 +10,6 @@
 
 open Univ
 
-val pr_with_global_universes : Level.t -> Pp.t
-val qualid_of_level : Level.t -> Libnames.qualid option
-
 (** Local universe name <-> level mapping *)
 
 type universe_binders = Univ.Level.t Names.Id.Map.t
@@ -20,3 +17,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 val empty_binders : universe_binders
 
 type univ_name_list = Names.lname list
+
+val pr_with_global_universes : universe_binders -> Level.t -> Pp.t
+val qualid_of_level : universe_binders -> Level.t -> Libnames.qualid option