Merge PR #20360: Cleanup univ.ml(i) (remove some aliases, move hcons functions)

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

Author: coqbot-app[bot]

dev/ci/user-overlays/20360-SkySkimmer-clean-univ.sh

@@ -0,0 +1 @@
+overlay metacoq https://github.com/SkySkimmer/metacoq clean-univ 20360

dev/top_printers.ml

@@ -286,7 +286,7 @@ let ppqvarset l = pp (hov 1 (str "{" ++ prlist_with_sep spc QVar.raw_pr (QVar.Se
 let ppuniverse_set l = pp (Level.Set.pr prlev l)
 let ppuniverse_instance l = pp (Instance.pr prqvar prlev l)
 let ppuniverse_context l = pp (pr_universe_context prqvar prlev l)
-let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
+let ppuniverse_context_set l = pp (ContextSet.pr prlev l)
 let ppuniverse_subst l = pp (UnivSubst.pr_universe_subst Level.raw_pr l)
 let ppuniverse_opt_subst l = pp (UnivFlex.pr Level.raw_pr l)
 let ppqvar_subst l = pp (UVars.pr_quality_level_subst QVar.raw_pr l)

engine/uState.ml

@@ -1320,7 +1320,7 @@ let pr ctx =
   else
     v 0
       (str"UNIVERSES:"++brk(0,1)++
-       h (Univ.pr_universe_context_set prl (context_set ctx)) ++ fnl () ++
+       h (Univ.ContextSet.pr prl (context_set ctx)) ++ fnl () ++
        UnivFlex.pr prl (subst ctx) ++ fnl() ++
        str"SORTS:"++brk(0,1)++
        h (pr_sort_opt_subst ctx) ++ fnl() ++

kernel/safe_typing.ml

@@ -1046,9 +1046,9 @@ let check_opaque senv (i : Opaqueproof.opaque_handle) pf =
   in
   let ctx = match ctx with
   | Opaqueproof.PrivateMonomorphic u ->
-    Opaqueproof.PrivateMonomorphic (snd @@ Univ.hcons_universe_context_set u)
+    Opaqueproof.PrivateMonomorphic (snd @@ Univ.ContextSet.hcons u)
   | Opaqueproof.PrivatePolymorphic u ->
-    Opaqueproof.PrivatePolymorphic (snd @@ Univ.hcons_universe_context_set u)
+    Opaqueproof.PrivatePolymorphic (snd @@ Univ.ContextSet.hcons u)
   in
   { opq_body = c; opq_univs = ctx; opq_handle = i; opq_nonce = nonce }
 

kernel/sorts.ml

@@ -407,11 +407,11 @@ module Hsorts =
 
       let hashcons = function
         | Type u as c ->
-          let hu, u' = hcons_univ u in
+          let hu, u' = Universe.hcons u in
           combinesmall 2 hu, if u' == u then c else Type u'
         | QSort (q, u) as c ->
           let hq, q' = QVar.hcons q in
-          let hu, u' = hcons_univ u in
+          let hu, u' = Universe.hcons u in
           combinesmall 3 (combine hu hq), if u' == u && q' == q then c else QSort (q', u')
         | SProp | Prop | Set as s -> hash s, s
       let eq s1 s2 = match (s1,s2) with

kernel/uVars.ml

@@ -315,7 +315,7 @@ struct
     let hqnames, qnames = Hashcons.hashcons_array Names.Name.hcons qnames in
     let hunames, unames = Hashcons.hashcons_array Names.Name.hcons unames in
     let hunivs, univs = Instance.hcons univs in
-    let hcsts, csts = hcons_constraints csts in
+    let hcsts, csts = Constraints.hcons csts in
     Hashset.Combine.combine4 hqnames hunames hunivs hcsts, ((qnames, unames), (univs, csts))
 
   let names ((names, _) : t) = names
@@ -380,7 +380,7 @@ struct
   let hcons ((qnames,unames), cst) =
     let hqnames, qnames = Hashcons.hashcons_array Names.Name.hcons qnames in
     let hunames, unames = Hashcons.hashcons_array Names.Name.hcons unames in
-    let hcst, cst = hcons_constraints cst in
+    let hcst, cst = Constraints.hcons cst in
     Hashset.Combine.combine3 hqnames hunames hcst, ((qnames, unames), cst)
 
   let empty = (([||],[||]), Constraints.empty)

kernel/univ.ml

@@ -229,14 +229,25 @@ module Level = struct
     let pr prl s =
       hov 1 (str"{" ++ prlist_with_sep spc prl (elements s) ++ str"}")
 
+
+    module Huniverse_set =
+      Hashcons.Make(
+      struct
+        type nonrec t = t
+        let hashcons s =
+          fold (fun x (h,acc) ->
+              let hx, x = hcons x in
+              Hashset.Combine.combine h hx, add x acc)
+            s
+            (0,empty)
+        let eq s s' = Map.Set.equal s s'
+      end)
+
+    let hcons = Hashcons.simple_hcons Huniverse_set.generate Huniverse_set.hcons ()
   end
 
 end
 
-type universe_level = Level.t
-
-type universe_set = Level.Set.t
-
 (* An algebraic universe [universe] is either a universe variable
    [Level.t] or a formal universe known to be greater than some
    universe variables and strictly greater than some (other) universe
@@ -444,6 +455,11 @@ let pr_constraint_type op =
     | Eq -> " = "
   in str op_str
 
+let hash_constraint_type = function
+  | Lt -> 0
+  | Le -> 1
+  | Eq -> 2
+
 module UConstraintOrd =
 struct
   type t = univ_constraint
@@ -456,23 +472,6 @@ struct
       else Level.compare v v'
 end
 
-module Constraints =
-struct
-  module S = Set.Make(UConstraintOrd)
-  include S
-
-  let pr prl c =
-    v 0 (prlist_with_sep spc (fun (u1,op,u2) ->
-      hov 0 (prl u1 ++ pr_constraint_type op ++ prl u2))
-       (elements c))
-
-end
-
-let hash_constraint_type = function
-  | Lt -> 0
-  | Le -> 1
-  | Eq -> 2
-
 module Hconstraint =
   Hashcons.Make(
     struct
@@ -487,13 +486,23 @@ module Hconstraint =
 
 let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate Hconstraint.hcons ()
 
-module Hconstraints = CSet.Hashcons(UConstraintOrd)(struct
-    type t = UConstraintOrd.t
-    let hcons = hcons_constraint
-  end)
+module Constraints =
+struct
+  module S = Set.Make(UConstraintOrd)
+  include S
 
-let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate Hconstraints.hcons ()
+  let pr prl c =
+    v 0 (prlist_with_sep spc (fun (u1,op,u2) ->
+      hov 0 (prl u1 ++ pr_constraint_type op ++ prl u2))
+        (elements c))
 
+  module Hconstraints = CSet.Hashcons(UConstraintOrd)(struct
+      type t = UConstraintOrd.t
+      let hcons = hcons_constraint
+    end)
+
+  let hcons = Hashcons.simple_hcons Hconstraints.generate Hconstraints.hcons ()
+end
 
 (** A value with universe constraints. *)
 type 'a constrained = 'a * Constraints.t
@@ -533,7 +542,7 @@ let univ_level_rem u v min =
 (** A universe level substitution, note that no algebraic universes are
     involved *)
 
-type universe_level_subst = universe_level Level.Map.t
+type universe_level_subst = Level.t Level.Map.t
 
 (** A set of universes with universe constraints.
     We linearize the set to a list after typechecking.
@@ -542,7 +551,7 @@ type universe_level_subst = universe_level Level.Map.t
 
 module ContextSet =
 struct
-  type t = universe_set constrained
+  type t = Level.Set.t constrained
 
   let empty = (Level.Set.empty, Constraints.empty)
   let is_empty (univs, cst) = Level.Set.is_empty univs && Constraints.is_empty cst
@@ -579,12 +588,16 @@ struct
   let levels (univs, _cst) = univs
 
   let size (univs,_) = Level.Set.cardinal univs
-end
 
-type universe_context_set = ContextSet.t
+  let hcons (v,c) =
+    let hv, v = Level.Set.hcons v in
+    let hc, c = Constraints.hcons c in
+    Hashset.Combine.combine hv hc, (v, c)
+
+end
 
 (** A value in a universe context (resp. context set). *)
-type 'a in_universe_context_set = 'a * universe_context_set
+type 'a in_universe_context_set = 'a * ContextSet.t
 
 (** Substitutions. *)
 
@@ -617,31 +630,5 @@ let subst_univs_level_constraints subst csts =
 
 (** Pretty-printing *)
 
-let pr_universe_context_set = ContextSet.pr
-
 let pr_universe_level_subst prl =
   Level.Map.pr prl (fun u -> str" := " ++ prl u ++ spc ())
-
-module Huniverse_set =
-  Hashcons.Make(
-    struct
-      type t = universe_set
-      let hashcons s =
-        Level.Set.fold (fun x (h,acc) ->
-            let hx, x = Level.hcons x in
-            Hashset.Combine.combine h hx, Level.Set.add x acc)
-          s
-          (0,Level.Set.empty)
-      let eq s s' =
-        Level.Set.equal s s'
-    end)
-
-let hcons_universe_set =
-  Hashcons.simple_hcons Huniverse_set.generate Huniverse_set.hcons ()
-
-let hcons_universe_context_set (v, c) =
-  let hv, v = hcons_universe_set v in
-  let hc, c = hcons_constraints c in
-  Hashset.Combine.combine hv hc, (v, c)
-
-let hcons_univ x = Universe.hcons x

kernel/univ.mli

@@ -72,6 +72,8 @@ sig
 
       val pr : (elt -> Pp.t) -> t -> Pp.t
       (** Pretty-printing *)
+
+      val hcons : t Hashcons.f
     end
 
   module Map :
@@ -181,6 +183,8 @@ module Constraints : sig
   include CSet.ExtS with type elt = univ_constraint
 
   val pr : (Level.t -> Pp.t) -> t -> Pp.t
+
+  val hcons : t Hashcons.f
 end
 
 (** A value with universe Constraints.t. *)
@@ -229,6 +233,11 @@ sig
   val size : t -> int
   (** The number of universes in the context *)
 
+  val hcons : t Hashcons.f
+
+  val pr : (Level.t -> Pp.t) -> t -> Pp.t
+
+
 end
 
 (** A value in a universe context set. *)
@@ -249,13 +258,5 @@ val subst_univs_level_constraints : universe_level_subst -> Constraints.t -> Con
 (** {6 Pretty-printing of universes. } *)
 
 val pr_constraint_type : constraint_type -> Pp.t
-val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
 
 val pr_universe_level_subst : (Level.t -> Pp.t) -> universe_level_subst -> Pp.t
-
-(** {6 Hash-consing } *)
-
-val hcons_univ : Universe.t Hashcons.f
-val hcons_constraints : Constraints.t Hashcons.f
-val hcons_universe_set : Level.Set.t Hashcons.f
-val hcons_universe_context_set : ContextSet.t Hashcons.f

printing/printer.ml

@@ -246,7 +246,7 @@ let universe_binders_with_opt_names orig names =
 
 let pr_universe_ctx_set sigma c =
   if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
-    fnl()++pr_in_comment (v 0 (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c))
+    fnl()++pr_in_comment (v 0 (Univ.ContextSet.pr (Termops.pr_evd_level sigma) c))
   else
     mt()
 
@@ -268,7 +268,7 @@ let pr_abstract_universe_ctx sigma ?variance ?priv c =
     let prqvar u = Termops.pr_evd_qvar sigma u in
     let prlev u = Termops.pr_evd_level sigma u in
     let pub = (if has_priv then str "Public universes:" ++ fnl() else mt()) ++ v 0 (UVars.pr_abstract_universe_context prqvar prlev ?variance c) in
-    let priv = if has_priv then fnl() ++ str "Private universes:" ++ fnl() ++ v 0 (Univ.pr_universe_context_set prlev priv) else mt() in
+    let priv = if has_priv then fnl() ++ str "Private universes:" ++ fnl() ++ v 0 (Univ.ContextSet.pr prlev priv) else mt() in
     fnl()++pr_in_comment (pub ++ priv)
   else
     mt()

vernac/vernacentries.ml

@@ -172,7 +172,7 @@ let show_universes ~proof =
   let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in
   UState.pr (Evd.ustate sigma) ++ fnl () ++
   v 1 (str "Normalized constraints:" ++ cut() ++
-       Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)
+       Univ.ContextSet.pr (Termops.pr_evd_level sigma) ctx)
 
 (* Simulate the Intro(s) tactic *)
 let show_intro ~proof all =