Preserve the ESorts abstraction in the upper layers.

We should never go back and forth between the low-level representation and the
high level one that keeps a quotient relative to a universe state.

engine/eConstr.ml

@@ -21,6 +21,24 @@ module ESorts = struct
 
   let equal sigma s1 s2 =
     Sorts.equal (kind sigma s1) (kind sigma s2)
+
+  let is_small sigma s = Sorts.is_small (kind sigma s)
+  let is_prop sigma s = Sorts.is_prop (kind sigma s)
+  let is_sprop sigma s = Sorts.is_sprop (kind sigma s)
+  let is_set sigma s = Sorts.is_set (kind sigma s)
+
+  let prop = make Sorts.prop
+  let sprop = make Sorts.sprop
+  let set = make Sorts.set
+  let type1 = make Sorts.type1
+
+  let super sigma s =
+    make (Sorts.super (kind sigma s))
+
+  let relevance_of_sort sigma s = Sorts.relevance_of_sort (kind sigma s)
+
+  let family sigma s = Sorts.family (kind sigma s)
+
 end
 
 module EInstance = struct
@@ -44,7 +62,7 @@ type case = (t, t, EInstance.t) pcase
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
-type unsafe_type_judgment = types Environ.punsafe_type_judgment
+type unsafe_type_judgment = (types, ESorts.t) Environ.punsafe_type_judgment
 type named_declaration = (constr, types) Context.Named.Declaration.pt
 type rel_declaration = (constr, types) Context.Rel.Declaration.pt
 type named_context = (constr, types) Context.Named.pt
@@ -62,7 +80,7 @@ let mkRel n = of_kind (Rel n)
 let mkVar id = of_kind (Var id)
 let mkMeta n = of_kind (Meta n)
 let mkEvar e = of_kind (Evar e)
-let mkSort s = of_kind (Sort (ESorts.make s))
+let mkSort s = of_kind (Sort s)
 let mkCast (b, k, t) = of_kind (Cast (b, k, t))
 let mkProd (na, t, u) = of_kind (Prod (na, t, u))
 let mkLambda (na, t, c) = of_kind (Lambda (na, t, c))
@@ -93,7 +111,7 @@ let mkRef (gr,u) = let open GlobRef in match gr with
 
 let mkLEvar = Evd.MiniEConstr.mkLEvar
 
-let type1 = mkSort Sorts.type1
+let type1 = mkSort ESorts.type1
 
 let applist (f, arg) = mkApp (f, Array.of_list arg)
 let applistc f arg = mkApp (f, Array.of_list arg)

engine/eConstr.mli

@@ -25,7 +25,7 @@ type case_branch = t pcase_branch
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
-type unsafe_type_judgment = types Environ.punsafe_type_judgment
+type unsafe_type_judgment = (types, Evd.esorts) Environ.punsafe_type_judgment
 type named_declaration = (constr, types) Context.Named.Declaration.pt
 type rel_declaration = (constr, types) Context.Rel.Declaration.pt
 type named_context = (constr, types) Context.Named.pt
@@ -35,7 +35,7 @@ type rel_context = (constr, types) Context.Rel.pt
 
 module ESorts :
 sig
-  type t
+  type t = Evd.esorts
   (** Type of sorts up-to universe unification. Essentially a wrapper around
       Sorts.t so that normalization is ensured statically. *)
 
@@ -46,6 +46,24 @@ sig
   (** Returns the view into the current sort. Note that the kind of a variable
       may change if the unification state of the evar map changes. *)
 
+  val equal : Evd.evar_map -> t -> t -> bool
+
+  val is_small : Evd.evar_map -> t -> bool
+  val is_prop : Evd.evar_map -> t -> bool
+  val is_sprop : Evd.evar_map -> t -> bool
+  val is_set : Evd.evar_map -> t -> bool
+
+  val prop : t
+  val sprop : t
+  val set : t
+  val type1 : t
+
+  val super : Evd.evar_map -> t -> t
+
+  val relevance_of_sort : Evd.evar_map -> t -> Sorts.relevance
+
+  val family : Evd.evar_map -> t -> Sorts.family
+
 end
 
 module EInstance :
@@ -115,7 +133,7 @@ val mkRel : int -> t
 val mkVar : Id.t -> t
 val mkMeta : metavariable -> t
 val mkEvar : t pexistential -> t
-val mkSort : Sorts.t -> t
+val mkSort : ESorts.t -> t
 val mkSProp : t
 val mkProp : t
 val mkSet  : t

engine/evarutil.ml

@@ -757,7 +757,7 @@ let occur_evar_upto sigma n c =
 let judge_of_new_Type evd =
   let open EConstr in
   let (evd', s) = new_sort_variable univ_rigid evd in
-  (evd', { uj_val = mkSort s; uj_type = mkSort (Sorts.super s) })
+  (evd', { uj_val = mkSort s; uj_type = mkSort (ESorts.super evd s) })
 
 let subterm_source evk ?where (loc,k) =
   let evk = match k with

engine/evarutil.mli

@@ -64,7 +64,7 @@ val new_type_evar :
   ?naming:intro_pattern_naming_expr ->
   ?principal:bool -> ?hypnaming:naming_mode ->
   env -> evar_map -> rigid ->
-  evar_map * (constr * Sorts.t)
+  evar_map * (constr * ESorts.t)
 
 val new_Type : ?rigid:rigid -> evar_map -> evar_map * constr
 

engine/evd.ml

@@ -23,6 +23,7 @@ module NamedDecl = Context.Named.Declaration
 
 type econstr = constr
 type etypes = types
+type esorts = Sorts.t
 
 (** Generic filters *)
 module Filter :

engine/evd.mli

@@ -30,6 +30,7 @@ open Environ
 
 type econstr
 type etypes = econstr
+type esorts
 
 (** {5 Existential variables and unification states} *)
 
@@ -625,7 +626,7 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 val universe_binders : evar_map -> UnivNames.universe_binders
 
 val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
-val new_sort_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Sorts.t
+val new_sort_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * esorts
 
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
 
@@ -636,23 +637,23 @@ val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_
 val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map
 (** See [UState.make_nonalgebraic_variable]. *)
 
-val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option
+val is_sort_variable : evar_map -> esorts -> Univ.Level.t option
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is
     not a local sort variable declared in [evm] *)
 
 val is_flexible_level : evar_map -> Univ.Level.t -> bool
 
 val normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t
 
-val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
-val set_eq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
+val set_leq_sort : env -> evar_map -> esorts -> esorts -> evar_map
+val set_eq_sort : env -> evar_map -> esorts -> esorts -> evar_map
 val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
 val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
 val set_eq_instances : ?flex:bool ->
   evar_map -> Univ.Instance.t -> Univ.Instance.t -> evar_map
 
-val check_eq : evar_map -> Sorts.t -> Sorts.t -> bool
-val check_leq : evar_map -> Sorts.t -> Sorts.t -> bool
+val check_eq : evar_map -> esorts -> esorts -> bool
+val check_leq : evar_map -> esorts -> esorts -> bool
 
 val check_constraints : evar_map -> Univ.Constraints.t -> bool
 
@@ -690,7 +691,7 @@ val update_sigma_univs : UGraph.t -> evar_map -> evar_map
 (** Polymorphic universes *)
 
 val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid
-  -> evar_map -> Sorts.family -> evar_map * Sorts.t
+  -> evar_map -> Sorts.family -> evar_map * esorts
 val fresh_constant_instance : ?loc:Loc.t -> ?rigid:rigid
   -> env -> evar_map -> Constant.t -> evar_map * pconstant
 val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid
@@ -730,7 +731,7 @@ val create_evar_defs : evar_map -> evar_map
 (** Use this module only to bootstrap EConstr *)
 module MiniEConstr : sig
   module ESorts : sig
-    type t
+    type t = esorts
     val make : Sorts.t -> t
     val kind : evar_map -> t -> Sorts.t
     val unsafe_to_sorts : t -> Sorts.t

interp/notation.ml

@@ -517,6 +517,7 @@ let rec check_glob env sigma g c = match DAst.get g, Constr.kind c with
      sigma, mkArray (u,t,def,ty)
   | Glob_term.GSort s, Constr.Sort s' ->
      let sigma,s = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family s) in
+     let s = EConstr.ESorts.kind sigma s in
      if not (Sorts.equal s s') then raise NotAValidPrimToken;
      sigma,mkSort s
   | _ -> raise NotAValidPrimToken
@@ -574,6 +575,7 @@ let rec constr_of_glob to_post post env sigma g = match DAst.get g with
        sigma, mkArray (u',t',def',ty')
   | Glob_term.GSort gs ->
       let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in
+      let c = EConstr.ESorts.kind sigma c in
       sigma,mkSort c
   | _ ->
       raise NotAValidPrimToken

kernel/environ.ml

@@ -783,11 +783,11 @@ let make_judge v tj =
 let j_val j = j.uj_val
 let j_type j = j.uj_type
 
-type 'types punsafe_type_judgment = {
+type ('types, 'sorts) punsafe_type_judgment = {
   utj_val : 'types;
-  utj_type : Sorts.t }
+  utj_type : 'sorts }
 
-type unsafe_type_judgment = types punsafe_type_judgment
+type unsafe_type_judgment = (types, Sorts.t) punsafe_type_judgment
 
 exception Hyp_not_found
 

kernel/environ.mli

@@ -391,11 +391,11 @@ val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment
 val j_val  : ('constr, 'types) punsafe_judgment -> 'constr
 val j_type : ('constr, 'types) punsafe_judgment -> 'types
 
-type 'types punsafe_type_judgment = {
+type ('types, 'sorts) punsafe_type_judgment = {
   utj_val : 'types;
-  utj_type : Sorts.t }
+  utj_type : 'sorts }
 
-type unsafe_type_judgment = types punsafe_type_judgment
+type unsafe_type_judgment = (types, Sorts.t) punsafe_type_judgment
 
 exception Hyp_not_found
 

plugins/cc/cctac.ml

@@ -49,7 +49,7 @@ let whd_in_concl =
 (* decompose member of equality in an applicative format *)
 
 (** FIXME: evar leak *)
-let sf_of env sigma c = snd (sort_of env sigma c)
+let sf_of env sigma c = ESorts.kind sigma (snd (sort_of env sigma c))
 
 let rec decompose_term env sigma t =
     match EConstr.kind sigma (whd env sigma t) with

plugins/funind/gen_principle.ml

@@ -204,7 +204,7 @@ let build_functional_principle env (sigma : Evd.evar_map) old_princ_type sorts f
   let new_principle_type =
     Functional_principles_types.compute_new_princ_type_from_rel (Global.env ())
       (Array.map Constr.mkConstU funs)
-      sorts old_princ_type
+      (Array.map (fun s -> EConstr.ESorts.kind sigma s) sorts) old_princ_type
   in
   let sigma, _ =
     Typing.type_of ~refresh:true env sigma
@@ -223,6 +223,7 @@ let build_functional_principle env (sigma : Evd.evar_map) old_princ_type sorts f
 
 let change_property_sort evd toSort princ princName =
   let open Context.Rel.Declaration in
+  let toSort = EConstr.ESorts.kind evd toSort in
   let princ = EConstr.of_constr princ in
   let princ_info = Tactics.compute_elim_sig evd princ in
   let change_sort_in_predicate decl =
@@ -273,7 +274,7 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
       | Some id -> (id, id)
       | None ->
         let id_of_f = Label.to_id (Constant.label (fst f)) in
-        (id_of_f, Indrec.make_elimination_ident id_of_f (Sorts.family type_sort))
+        (id_of_f, Indrec.make_elimination_ident id_of_f (EConstr.ESorts.family !evd type_sort))
     in
     let names = ref [new_princ_name] in
     let hook new_principle_type _ =
@@ -1368,6 +1369,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list =
     let other_fun_princ_types =
       let funs = Array.map Constr.mkConstU this_block_funs in
       let sorts = Array.of_list sorts in
+      let sorts = Array.map (fun s -> EConstr.ESorts.kind sigma s) sorts in
       List.map
         (Functional_principles_types.compute_new_princ_type_from_rel (Global.env ()) funs sorts)
         other_princ_types
@@ -2226,7 +2228,7 @@ let build_case_scheme fa =
   let sigma, scheme, scheme_type =
     Indrec.build_case_analysis_scheme_default env sigma ind sf
   in
-  let sorts = (fun (_, _, x) -> fst @@ UnivGen.fresh_sort_in_family x) fa in
+  let sorts = (fun (_, _, x) -> EConstr.ESorts.make @@ fst @@ UnivGen.fresh_sort_in_family x) fa in
   let princ_name = (fun (x, _, _) -> x) fa in
   let (_ : unit) =
     (* Pp.msgnl (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++

plugins/ltac2/tac2core.ml

@@ -651,7 +651,7 @@ let () = define1 "constr_make" valexpr begin fun knd ->
     EConstr.mkLEvar sigma (evk, Array.to_list args)
   | (4, [|s|]) ->
     let s = Value.to_ext Value.val_sort s in
-    EConstr.mkSort (EConstr.Unsafe.to_sorts s)
+    EConstr.mkSort s
   | (5, [|c; k; t|]) ->
     let c = Value.to_constr c in
     let k = Value.to_ext Value.val_cast k in
@@ -803,7 +803,7 @@ let () = define3 "constr_in_context" ident constr closure begin fun id t c ->
         let t_ty = Retyping.get_type_of env sigma t in
         (* If the user passed eg ['_] for the type we force it to indeed be a type *)
         let sigma, j = Typing.type_judgment env sigma {uj_val=t; uj_type=t_ty} in
-        sigma, Sorts.relevance_of_sort j.utj_type
+        sigma, EConstr.ESorts.relevance_of_sort sigma j.utj_type
       in
       let nenv = EConstr.push_named (LocalAssum (Context.make_annot id t_rel, t)) env in
       let (sigma, (evt, _)) = Evarutil.new_type_evar nenv sigma Evd.univ_flexible in

plugins/micromega/coq_micromega.ml

@@ -938,7 +938,7 @@ let mkformula_binary b g term f1 f2 =
 
 let is_prop env sigma term =
   let sort = Retyping.get_sort_of env sigma term in
-  Sorts.is_prop sort
+  EConstr.ESorts.is_prop sigma sort
 
 type formula_op =
   { op_impl : EConstr.t option (* only for booleans *)

plugins/micromega/zify.ml

@@ -1022,7 +1022,7 @@ let arrow =
 
 let is_prop env sigma term =
   let sort = Retyping.get_sort_of env sigma term in
-  Sorts.is_prop sort
+  EConstr.ESorts.is_prop sigma sort
 
 let is_arrow env evd a p1 p2 =
   is_prop env evd p1

plugins/ssr/ssrfwd.ml

@@ -116,7 +116,7 @@ let combineCG t1 t2 f g = match t1, t2 with
       let _, info = Exninfo.capture e in
       Tacticals.tclZEROMSG ~info (str "Not a proposition or a type.")
     | sigma, s ->
-      let r = Sorts.relevance_of_sort s in
+      let r = ESorts.relevance_of_sort sigma s in
       let sigma, f, glf =
         match k with
         | HaveTransp ->

plugins/syntax/number.ml

@@ -193,6 +193,7 @@ let locate_global_sort_inductive_or_constant sigma qid =
     match Abbreviation.search_abbreviation kn with
     | [], Notation_term.NSort r ->
        let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family r) in
+       let c = EConstr.ESorts.kind sigma c in
        sigma,Constr.mkSort c
     | _ -> raise Not_found in
   try locate_sort qid

pretyping/cases.ml

@@ -1924,7 +1924,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t =
   (* [pb] is the auxiliary pattern-matching serving as skeleton for the
       return type of the original problem Xi *)
   let s = Retyping.get_sort_of !!env sigma t in
-  let sigma, s = Sorts.(match s with
+  let sigma, s = Sorts.(match ESorts.kind sigma s with
   | SProp | Prop | Set ->
     (* To anticipate a possible restriction on an elimination from
        SProp, Prop or (impredicative) Set we preserve the sort of the

pretyping/coercion.ml

@@ -555,7 +555,7 @@ let inh_app_fun ~program_mode ~resolve_tc ?use_coercions env sigma body typ =
 
 let type_judgment env sigma j =
   match EConstr.kind sigma (whd_all env sigma j.uj_type) with
-    | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind sigma s }
+    | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_a_type env sigma j
 
 let inh_tosort_force ?loc env sigma ({ uj_val; uj_type } as j) =
@@ -570,7 +570,7 @@ let inh_tosort_force ?loc env sigma ({ uj_val; uj_type } as j) =
 let inh_coerce_to_sort ?loc ?(use_coercions=true) env sigma j =
   let typ = whd_all env sigma j.uj_type in
     match EConstr.kind sigma typ with
-    | Sort s -> (sigma,{ utj_val = j.uj_val; utj_type = ESorts.kind sigma s })
+    | Sort s -> (sigma,{ utj_val = j.uj_val; utj_type = s })
     | Evar ev ->
         let (sigma,s) = Evardefine.define_evar_as_sort env sigma ev in
           (sigma,{ utj_val = j.uj_val; utj_type = s })

pretyping/evarconv.ml

@@ -1067,8 +1067,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 
         | Sort s1, Sort s2 when app_empty ->
             (try
-              let s1 = ESorts.kind evd s1 in
-              let s2 = ESorts.kind evd s2 in
                let evd' =
                  if pbty == CONV
                  then Evd.set_eq_sort env evd s1 s2