Merge PR #13415: Separate interning and pretyping of universes

Reviewed-by: mattam82

6 files changed, 70 insertions, 78 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 f42c754ef5..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,19 +62,23 @@ let glob_sort_family = let open Sorts in function
   | UNamed [GSet,0] -> InSet
   | _ -> raise ComplexSort
 
-let glob_sort_expr_eq f u1 u2 =
+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
   | UNamed l1, UNamed l2 -> f l1 l2
   | (UNamed _ | UAnonymous _), _ -> false
 
 let glob_sort_eq u1 u2 =
-  glob_sort_expr_eq
+  glob_sort_gen_eq
     (List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n))
     u1 u2
 
 let glob_level_eq u1 u2 =
-  glob_sort_expr_eq glob_sort_name_eq u1 u2
+  glob_sort_gen_eq glob_sort_name_eq u1 u2
 
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Explicit, Explicit -> true
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 a49c8abe26..a957bc0fcd 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -26,17 +26,23 @@ 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
 
-type 'a glob_sort_expr =
+      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 *)
   | UNamed of 'a
 
 (** levels, occurring in universe instances *)
-type glob_level = glob_sort_name glob_sort_expr
+type glob_level = glob_sort_name glob_sort_gen
 
 (** sort expressions *)
-type glob_sort = (glob_sort_name * int) list glob_sort_expr
+type glob_sort = (glob_sort_name * int) list glob_sort_gen
 
 type glob_constraint = glob_sort_name * Univ.constraint_type * glob_sort_name
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f52dfc51ac..9dbded75ba 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_typed_evar env sigma ?naming ~src tycon =
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 *)