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, 30 insertions, 28 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 8942bc7805..4c410c3170 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -152,14 +152,15 @@ let tag_var = tag Tag.variable
 
   let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c)
 
-  let pr_glob_sort_name = function
-    | GSProp -> str "SProp"
-    | GProp -> str "Prop"
-    | GSet -> str "Set"
-    | GType qid -> pr_qualid qid
+  let pr_sort_name_expr = function
+    | CSProp -> str "SProp"
+    | CProp -> str "Prop"
+    | CSet -> str "Set"
+    | CType qid -> pr_qualid qid
+    | CRawType s -> Univ.Level.pr s
 
   let pr_univ_expr (u,n) =
-    pr_glob_sort_name u ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
+    pr_sort_name_expr u ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
 
   let pr_univ l =
     match l with
@@ -168,21 +169,22 @@ let tag_var = tag Tag.variable
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
-  let pr_glob_sort = let open Glob_term in function
-    | UNamed [GSProp,0] -> tag_type (str "SProp")
-    | UNamed [GProp,0] -> tag_type (str "Prop")
-    | UNamed [GSet,0] -> tag_type (str "Set")
+  let pr_sort_expr = function
+    | UNamed [CSProp,0] -> tag_type (str "SProp")
+    | UNamed [CProp,0] -> tag_type (str "Prop")
+    | UNamed [CSet,0] -> tag_type (str "Set")
     | UAnonymous {rigid=true} -> tag_type (str "Type")
     | UAnonymous {rigid=false} -> tag_type (str "Type") ++ pr_univ_annot (fun _ -> str "_") ()
     | UNamed u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
 
-  let pr_glob_level = let open Glob_term in function
-    | UNamed GSProp -> tag_type (str "SProp")
-    | UNamed GProp -> tag_type (str "Prop")
-    | UNamed GSet -> tag_type (str "Set")
+  let pr_univ_level_expr = function
+    | UNamed CSProp -> tag_type (str "SProp")
+    | UNamed CProp -> tag_type (str "Prop")
+    | UNamed CSet -> tag_type (str "Set")
     | UAnonymous {rigid=true} -> tag_type (str "Type")
     | UAnonymous {rigid=false} -> tag_type (str "_")
-    | UNamed (GType u) -> tag_type (pr_qualid u)
+    | UNamed (CType u) -> tag_type (pr_qualid u)
+    | UNamed (CRawType s) -> tag_type (Univ.Level.pr s)
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
@@ -200,7 +202,7 @@ let tag_var = tag Tag.variable
   let pr_patvar = pr_id
 
   let pr_universe_instance l =
-    pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_level)) l
+    pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_univ_level_expr)) l
 
   let pr_reference qid =
     if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid)
@@ -664,7 +666,7 @@ let tag_var = tag Tag.variable
       | CPatVar p ->
         return (str "@?" ++ pr_patvar p, latom)
       | CSort s ->
-        return (pr_glob_sort s, latom)
+        return (pr_sort_expr s, latom)
       | CCast (a,b) ->
         return (
           hv 0 (pr mt (LevelLt lcast) a ++ spc () ++
@@ -717,7 +719,7 @@ let tag_var = tag Tag.variable
   let transf env sigma c =
     if !Flags.beautify_file then
       let r = Constrintern.for_grammar (Constrintern.intern_constr env sigma) c in
-      Constrextern.extern_glob_constr (Termops.vars_of_env env) r
+      Constrextern.(extern_glob_constr (extern_env env sigma)) r
     else c
 
   let pr_expr env sigma prec c =
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 02e04573f8..d66b77efb2 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -32,9 +32,9 @@ val pr_id : Id.t -> Pp.t
 val pr_qualid : qualid -> Pp.t
 val pr_patvar : Pattern.patvar -> Pp.t
 
-val pr_glob_sort_name : Glob_term.glob_sort_name -> Pp.t
-val pr_glob_level : Glob_term.glob_level -> Pp.t
-val pr_glob_sort : Glob_term.glob_sort -> Pp.t
+val pr_sort_name_expr : sort_name_expr -> Pp.t
+val pr_univ_level_expr : univ_level_expr -> Pp.t
+val pr_sort_expr : sort_expr -> Pp.t
 val pr_guard_annot
   :  (constr_expr -> Pp.t)
   -> local_binder_expr list
diff --git a/printing/printer.ml b/printing/printer.ml
index ea718526de..1425cebafc 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -97,10 +97,10 @@ let pr_ltype_env ?lax ?goal_concl_style env sigma ?impargs c =
 let pr_ljudge_env env sigma j =
   (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
 
-let pr_lglob_constr_env env c =
-  pr_lconstr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c)
-let pr_glob_constr_env env c =
-  pr_constr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c)
+let pr_lglob_constr_env env sigma c =
+  pr_lconstr_expr env sigma (extern_glob_constr (extern_env env sigma) c)
+let pr_glob_constr_env env sigma c =
+  pr_constr_expr env sigma (extern_glob_constr (extern_env env sigma) c)
 
 let pr_closed_glob_n_env ?lax ?goal_concl_style ?inctx ?scope env sigma n c =
   pr_constr_expr_n env sigma n (extern_closed_glob ?lax ?goal_concl_style ?inctx ?scope env sigma c)
@@ -115,7 +115,7 @@ let pr_constr_pattern_env env sigma c =
 let pr_cases_pattern t =
   pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t)
 
-let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
+let pr_sort sigma s = pr_sort_expr (extern_sort sigma s)
 
 let () = Termops.Internal.set_print_constr
   (fun env sigma t -> pr_lconstr_expr env sigma (extern_constr ~lax:true env sigma t))
diff --git a/printing/printer.mli b/printing/printer.mli
index ea388ae57e..732af5570d 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -107,9 +107,9 @@ val pr_closed_glob_env     : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool
 
 val pr_ljudge_env          : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t
 
-val pr_lglob_constr_env      : env -> 'a glob_constr_g -> Pp.t
+val pr_lglob_constr_env    : env -> evar_map -> 'a glob_constr_g -> Pp.t
 
-val pr_glob_constr_env       : env -> 'a glob_constr_g -> Pp.t
+val pr_glob_constr_env     : env -> evar_map -> 'a glob_constr_g -> Pp.t
 
 val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t