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.

6 files changed, 64 insertions, 72 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a12a832f76..402a6f6ed3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -648,26 +648,16 @@ let detype_cofix detype flags avoid env sigma n (names,tys,bodies) =
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
-(* TODO use some algebraic type with a case for unnamed univs so we
-   can cleanly detype them. NB: this corresponds to a hack in
-   Pretyping.interp_universe_level_name to convert Foo.xx strings into
-   universes. *)
-let hack_qualid_of_univ_level sigma l =
-  match Termops.reference_of_level sigma l with
-  | Some qid -> qid
-  | None ->
-    let path = String.split_on_char '.' (Univ.Level.to_string l) in
-    let path = List.rev_map Id.of_string_soft path in
-    Libnames.qualid_of_dirpath (DirPath.make path)
+let detype_level_name sigma l =
+  if Univ.Level.is_sprop l then GSProp else
+  if Univ.Level.is_prop l then GProp else
+  if Univ.Level.is_set l then GSet else
+    match UState.id_of_level (Evd.evar_universe_context sigma) l with
+    | Some id -> GLocalUniv (CAst.make id)
+    | None -> GUniv l
 
 let detype_universe sigma u =
-  let fn (l, n) =
-    let s =
-      if Univ.Level.is_prop l then GProp else
-      if Univ.Level.is_set l then GSet else
-      GType (hack_qualid_of_univ_level sigma l) in
-    (s, n) in
-  List.map fn (Univ.Universe.repr u)
+  List.map (on_fst (detype_level_name sigma)) (Univ.Universe.repr u)
 
 let detype_sort sigma = function
   | SProp -> UNamed [GSProp,0]
@@ -684,8 +674,7 @@ type binder_kind = BProd | BLambda | BLetIn
 (* Main detyping function                                             *)
 
 let detype_level sigma l =
-  let l = hack_qualid_of_univ_level sigma l in
-  UNamed (GType l)
+  UNamed (detype_level_name sigma l)
 
 let detype_instance sigma l =
   let l = EInstance.kind sigma l in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index d631be18b8..86d2cc78e0 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -48,8 +48,10 @@ let glob_sort_name_eq g1 g2 = match g1, g2 with
   | GSProp, GSProp
   | GProp, GProp
   | GSet, GSet -> true
-  | GType u1, GType u2 -> Libnames.qualid_eq u1 u2
-  | (GSProp|GProp|GSet|GType _), _ -> false
+  | GUniv u1, GUniv u2 -> Univ.Level.equal u1 u2
+  | GLocalUniv u1, GLocalUniv u2 -> lident_eq u1 u2
+  | GRawUniv u1, GRawUniv u2 -> Univ.Level.equal u1 u2
+  | (GSProp|GProp|GSet|GUniv _|GLocalUniv _|GRawUniv _), _ -> false
 
 exception ComplexSort
 
@@ -60,6 +62,10 @@ let glob_sort_family = let open Sorts in function
   | UNamed [GSet,0] -> InSet
   | _ -> raise ComplexSort
 
+let map_glob_sort_gen f = function
+  | UNamed l -> UNamed (f l)
+  | UAnonymous _ as x -> x
+
 let glob_sort_gen_eq f u1 u2 =
  match u1, u2 with
   | UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 6da8173dce..5ad1a207f3 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -11,8 +11,12 @@
 open Names
 open Glob_term
 
+val map_glob_sort_gen : ('a -> 'b) -> 'a glob_sort_gen -> 'b glob_sort_gen
+
 (** Equalities *)
 
+val glob_sort_gen_eq : ('a -> 'a -> bool) -> 'a glob_sort_gen -> 'a glob_sort_gen -> bool
+
 val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
 
 val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 0b4eab1475..a957bc0fcd 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -26,7 +26,13 @@ type glob_sort_name =
   | GSProp (** representation of [SProp] literal *)
   | GProp (** representation of [Prop] level *)
   | GSet  (** representation of [Set] level *)
-  | GType of Libnames.qualid (** representation of a [Type] level *)
+  | GUniv of Univ.Level.t
+  | GLocalUniv of lident (** Locally bound universes (may also be nonstrict declaration) *)
+  | GRawUniv of Univ.Level.t
+  (** Hack for funind, DO NOT USE
+
+      Note that producing the similar Constrexpr.CRawType for printing
+      is OK, just don't try to reinterp it. *)
 
 type 'a glob_sort_gen =
   | UAnonymous of { rigid : bool } (** not rigid = unifiable by minimization *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b70ff20e32..65950edb81 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -130,53 +130,32 @@ let is_strict_universe_declarations =
 
 (** Miscellaneous interpretation functions *)
 
-let interp_known_universe_level_name evd qid =
-  try
-    let open Libnames in
-    if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
-    else raise Not_found
+let universe_level_name evd ({CAst.v=id} as lid) =
+  try evd, Evd.universe_of_name evd id
   with Not_found ->
-    let qid = Nametab.locate_universe qid in
-    Univ.Level.make qid
+    if not (is_strict_universe_declarations ()) then
+      new_univ_level_variable ?loc:lid.CAst.loc ~name:id univ_rigid evd
+    else user_err ?loc:lid.CAst.loc ~hdr:"universe_level_name"
+        (Pp.(str "Undeclared universe: " ++ Id.print id))
 
-let interp_universe_level_name evd qid =
-  try evd, interp_known_universe_level_name evd qid
-  with Not_found ->
-    if Libnames.qualid_is_ident qid then (* Undeclared *)
-      let id = Libnames.qualid_basename qid in
-      if not (is_strict_universe_declarations ()) then
-        new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd
-      else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
-          (Pp.(str "Undeclared universe: " ++ Id.print id))
-    else
-      let dp, i = Libnames.repr_qualid qid in
-      let num =
-        try int_of_string (Id.to_string i)
-        with Failure _ ->
-          user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
-            (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
-      in
-      let level = Univ.Level.(make (UGlobal.make dp num)) in
-      let evd =
-        try Evd.add_global_univ evd level
-        with UGraph.AlreadyDeclared -> evd
-      in evd, level
-
-let interp_sort_name sigma = function
+let sort_name sigma = function
   | GSProp -> sigma, Univ.Level.sprop
   | GProp -> sigma, Univ.Level.prop
   | GSet -> sigma, Univ.Level.set
-  | GType l -> interp_universe_level_name sigma l
+  | GUniv u -> sigma, u
+  | GRawUniv u ->
+    (try Evd.add_global_univ sigma u with UGraph.AlreadyDeclared -> sigma), u
+  | GLocalUniv l -> universe_level_name sigma l
 
-let interp_sort_info ?loc evd l =
+let sort_info ?loc evd l =
     List.fold_left (fun (evd, u) (l,n) ->
-      let evd', u' = interp_sort_name evd l in
+      let evd', u' = sort_name evd l in
       let u' = Univ.Universe.make u' in
       let u' = match n with
       | 0 -> u'
       | 1 -> Univ.Universe.super u'
       | n ->
-        user_err ?loc ~hdr:"interp_universe"
+        user_err ?loc ~hdr:"sort_info"
           (Pp.(str "Cannot interpret universe increment +" ++ int n))
       in (evd', Univ.sup u u'))
     (evd, Univ.Universe.type0m) l
@@ -393,24 +372,33 @@ let pretype_id pretype loc env sigma id =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let interp_known_glob_level ?loc evd = function
+let known_universe_level_name evd lid =
+  try Evd.universe_of_name evd lid.CAst.v
+  with Not_found ->
+    let u = Nametab.locate_universe (Libnames.qualid_of_lident lid) in
+    Univ.Level.make u
+
+let known_glob_level evd = function
   | GSProp -> Univ.Level.sprop
   | GProp -> Univ.Level.prop
   | GSet -> Univ.Level.set
-  | GType qid ->
-    try interp_known_universe_level_name evd qid
+  | GUniv u -> u
+  | GRawUniv u -> anomaly Pp.(str "Raw universe in known_glob_level.")
+  | GLocalUniv lid ->
+    try known_universe_level_name evd lid
     with Not_found ->
-      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
+      user_err ?loc:lid.CAst.loc ~hdr:"known_level_info"
+        (str "Undeclared universe " ++ Id.print lid.CAst.v)
 
-let interp_glob_level ?loc evd : glob_level -> _ = function
+let glob_level ?loc evd : glob_level -> _ = function
   | UAnonymous {rigid} -> new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd
-  | UNamed s -> interp_sort_name evd s
+  | UNamed s -> sort_name evd s
 
-let interp_instance ?loc evd l =
+let instance ?loc evd l =
   let evd, l' =
     List.fold_left
       (fun (evd, univs) l ->
-         let evd, l = interp_glob_level ?loc evd l in
+         let evd, l = glob_level ?loc evd l in
          (evd, l :: univs)) (evd, [])
       l
   in
@@ -424,7 +412,7 @@ let pretype_global ?loc rigid env evd gr us =
   let evd, instance =
     match us with
     | None -> evd, None
-    | Some l -> interp_instance ?loc evd l
+    | Some l -> instance ?loc evd l
   in
   Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr
 
@@ -451,11 +439,11 @@ let pretype_ref ?loc sigma env ref us =
     let sigma, ty = type_of !!env sigma c in
     sigma, make_judge c ty
 
-let interp_sort ?loc evd : glob_sort -> _ = function
+let sort ?loc evd : glob_sort -> _ = function
   | UAnonymous {rigid} ->
     let evd, l = new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd in
     evd, Univ.Universe.make l
-  | UNamed l -> interp_sort_info ?loc evd l
+  | UNamed l -> sort_info ?loc evd l
 
 let judge_of_sort ?loc evd s =
   let judge =
@@ -469,7 +457,7 @@ let pretype_sort ?loc sigma s =
   | UNamed [GProp,0] -> sigma, judge_of_prop
   | UNamed [GSet,0] -> sigma, judge_of_set
   | _ ->
-  let sigma, s = interp_sort ?loc sigma s in
+  let sigma, s = sort ?loc sigma s in
   judge_of_sort ?loc sigma s
 
 let new_type_evar env sigma loc =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7bb4a6e273..5668098fe6 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -30,8 +30,7 @@ val get_bidirectionality_hint : GlobRef.t -> int option
 
 val clear_bidirectionality_hint : GlobRef.t -> unit
 
-val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
-  glob_sort_name -> Univ.Level.t
+val known_glob_level : Evd.evar_map -> glob_sort_name -> Univ.Level.t
 
 (** An auxiliary function for searching for fixpoint guard indexes *)