Merge PR #21424: Reduce the API reliance on PConstraints.ContextSet.t

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>

Author: coqbot-app[bot]

dev/ci/user-overlays/21424-ppedrot-chase-pconstraint-context-set.sh

@@ -0,0 +1 @@
+overlay elpi https://github.com/ppedrot/coq-elpi chase-pconstraint-context-set 21424

engine/uState.ml

@@ -473,7 +473,7 @@ let context uctx =
 type named_universes_entry = universes_entry * UnivNames.universe_binders
 
 let check_mono_sort_constraints uctx =
-  let (uvar, (qcst, ucst)) = uctx in
+  let (uvar, (qcst, ucst)) = uctx.local in
   (* This looks very stringent but it passes nonetheless all the tests? *)
   let () = assert (Sorts.ElimConstraints.is_empty qcst) in
   (uvar, ucst)
@@ -483,7 +483,7 @@ let univ_entry ~poly uctx =
   let entry =
     if poly then Polymorphic_entry (context uctx)
     else
-      let uctx = check_mono_sort_constraints (context_set uctx) in
+      let uctx = check_mono_sort_constraints uctx in
       Monomorphic_entry uctx
   in
   entry, binders
@@ -1091,18 +1091,20 @@ let check_template_univ_decl uctx ~template_qvars decl =
       if not (QVar.Set.equal template_qvars (QState.undefined uctx.sort_variables))
       then CErrors.anomaly Pp.(str "Bugged template univ declaration.")
   in
+  (* XXX: when the kernel takes template entries closer to the polymorphic ones,
+     we should perform some additional checks here. *)
+  let () = assert (Sorts.ElimConstraints.is_empty decl.univdecl_elim_constraints) in
   let levels, csts = uctx.local in
   let () =
     let prefix = decl.univdecl_instance in
     if not decl.univdecl_extensible_instance
     then check_universe_context_set ~prefix levels uctx.names
   in
-  if decl.univdecl_extensible_constraints then uctx.local
-  else begin
-    check_implication uctx
-      (univ_decl_csts decl) csts;
-    levels, (decl.univdecl_elim_constraints,decl.univdecl_univ_constraints)
-  end
+  if decl.univdecl_extensible_constraints then
+    PConstraints.ContextSet.univ_context_set uctx.local
+  else
+    let () = check_implication uctx (univ_decl_csts decl) csts in
+    (levels, decl.univdecl_univ_constraints)
 
 let check_mono_univ_decl uctx decl =
   (* Note: if [decl] is [default_univ_decl], behave like [uctx.local] *)
@@ -1117,7 +1119,7 @@ let check_mono_univ_decl uctx decl =
     if not decl.univdecl_extensible_instance
     then check_universe_context_set ~prefix levels uctx.names
   in
-  if decl.univdecl_extensible_constraints then check_mono_sort_constraints uctx.local
+  if decl.univdecl_extensible_constraints then check_mono_sort_constraints uctx
   else
     let () = assert (Sorts.ElimConstraints.is_empty (fst csts)) in
     let () = check_implication uctx (univ_decl_csts decl) csts in
@@ -1156,12 +1158,10 @@ let check_univ_decl ~poly uctx decl =
   in
   entry, binders
 
-let restrict_universe_context (univs, csts) keep =
+let restrict_universe_context (univs, univ_csts) keep =
   let removed = Level.Set.diff univs keep in
-  if Level.Set.is_empty removed then univs, csts
+  if Level.Set.is_empty removed then univs, univ_csts
   else
-  let elim_csts = PConstraints.qualities csts in
-  let univ_csts = PConstraints.univs csts in
   let allunivs = UnivConstraints.fold (fun (u,_,v) all -> Level.Set.add u (Level.Set.add v all)) univ_csts univs in
   let g = UGraph.initial_universes in
   let g = Level.Set.fold (fun v g ->
@@ -1171,17 +1171,21 @@ let restrict_universe_context (univs, csts) keep =
   let allkept = Level.Set.union (UGraph.domain UGraph.initial_universes) (Level.Set.diff allunivs removed) in
   let univ_csts = UGraph.constraints_for ~kept:allkept g in
   let univ_csts = UnivConstraints.filter (fun (l,d,r) -> not (Level.is_set l && d == Le)) univ_csts in
-  (Level.Set.inter univs keep, PConstraints.make elim_csts univ_csts)
+  (Level.Set.inter univs keep, univ_csts)
+
+let restrict_universe_pcontext (us, (qcst, ucst)) keep =
+  let (us, ucst) = restrict_universe_context (us, ucst) keep in
+  (us, (qcst, ucst))
 
 let restrict uctx vars =
   let vars = Id.Map.fold (fun na l vars -> Level.Set.add l vars)
       (snd (fst uctx.names)) vars
   in
-  let uctx' = restrict_universe_context uctx.local vars in
+  let uctx' = restrict_universe_pcontext uctx.local vars in
   { uctx with local = uctx' }
 
 let restrict_even_binders uctx vars =
-  let uctx' = restrict_universe_context uctx.local vars in
+  let uctx' = restrict_universe_pcontext uctx.local vars in
   { uctx with local = uctx' }
 
 let restrict_univ_constraints uctx csts =

engine/uState.mli

@@ -155,7 +155,7 @@ val name_level : Univ.Level.t -> Id.t -> t -> t
    the universes in [keep]. The constraints [csts] are adjusted so
    that transitive constraints between remaining universes (those in
    [keep] and those not in [univs]) are preserved. *)
-val restrict_universe_context : PConstraints.ContextSet.t -> Level.Set.t -> PConstraints.ContextSet.t
+val restrict_universe_context : Univ.ContextSet.t -> Level.Set.t -> Univ.ContextSet.t
 
 (** [restrict uctx ctx] restricts the local universes of [uctx] to
    [ctx] extended by local named universes and side effect universes
@@ -267,9 +267,9 @@ val check_uctx_impl : fail:(Pp.t -> unit) -> t -> t -> unit
 
 val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
 
-val check_template_univ_decl : t -> template_qvars:QVar.Set.t -> universe_decl -> PConstraints.ContextSet.t
+val check_template_univ_decl : t -> template_qvars:QVar.Set.t -> universe_decl -> Univ.ContextSet.t
 
-val check_mono_sort_constraints : PConstraints.ContextSet.t -> Univ.ContextSet.t
+val check_mono_sort_constraints : t -> Univ.ContextSet.t
 
 (** {5 TODO: Document me} *)
 

plugins/ring/ring.ml

@@ -180,8 +180,7 @@ let decl_constant name univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context univs vars in
-  let () = Global.push_qualities QGraph.Static (PConstraints.ContextSet.sort_context_set univs) in (* XXX *)
-  let () = Global.push_context_set (PConstraints.ContextSet.univ_context_set univs) in
+  let () = Global.push_context_set univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = UState.Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders in
   (* UnsafeMonomorphic: we always do poly:false *)
@@ -236,7 +235,8 @@ let exec_tactic env sigma n f args =
   let ((), pv, _, _, _) = Proofview.apply ~name:(Id.of_string "ring") ~poly:false (Global.env ()) tac pv in
   let sigma = Evd.minimize_universes (Proofview.return pv) in
   let nf c = constr_of sigma c in
-  Array.map nf !tactic_res, Evd.universe_context_set sigma
+  let uctx = UState.check_mono_univ_decl (Evd.ustate sigma) UState.default_univ_decl in
+  Array.map nf !tactic_res, uctx
 
 let gen_constant n = (); fun () -> (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Global.env ()) (Rocqlib.lib_ref n)))
 let gen_reference n = (); fun () -> (Rocqlib.lib_ref n)

vernac/comInductive.ml

@@ -535,15 +535,12 @@ let template_univ_entry sigma udecl ~template_univs pseudo_sort_poly =
   let uctx =
     UState.check_template_univ_decl (Evd.ustate sigma) ~template_qvars udecl
   in
-  (* XXX: it should be fine to drop the sort constraints but it should be reflected in the API *)
-  let elim_constraints = PConstraints.ContextSet.elim_constraints uctx in
-  let uctx = PConstraints.ContextSet.univ_context_set uctx in
   let ubinders = UState.Monomorphic_entry uctx, Evd.universe_binders sigma in
   let template_univs, global = split_universe_context template_univs uctx in
   let uctx =
     UVars.UContext.of_context_set
       (UState.compute_instance_binders @@ Evd.ustate sigma)
-      ((template_qvars, elim_constraints), template_univs)
+      ((template_qvars, Sorts.ElimConstraints.empty), template_univs)
   in
   let default_univs =
     let inst = UVars.UContext.instance uctx in

vernac/declare.ml

@@ -227,7 +227,7 @@ let instance_of_univs = function
 
 let add_mono_uctx uctx = function
   | UState.Monomorphic_entry ctx, ubinders ->
-    let uctx = UState.check_mono_sort_constraints @@ UState.context_set uctx in
+    let uctx = UState.check_mono_sort_constraints uctx in
     UState.Monomorphic_entry (Univ.ContextSet.union uctx ctx), ubinders
   | UState.Polymorphic_entry _, _ as x -> assert (PConstraints.ContextSet.is_empty (UState.context_set uctx)); x
 
@@ -273,8 +273,11 @@ let make_univs_immediate_private_poly ~uctx ~udecl ~eff ~used_univs body typ =
   let utyp = UState.check_univ_decl ~poly:true uctx' udecl in
   let ubody =
     let uctx = UState.restrict uctx used_univs in
-    let uctx = PConstraints.ContextSet.diff (UState.context_set uctx) (UState.context_set uctx') in
-    UState.check_mono_sort_constraints uctx
+    let uctx = UState.context_set uctx in
+    let uctx = PConstraints.ContextSet.diff uctx (UState.context_set uctx') in
+    (* XXX we should have a more principled check somewhere *)
+    let () = assert (Sorts.ElimConstraints.is_empty @@ PConstraints.ContextSet.elim_constraints uctx) in
+    PConstraints.ContextSet.univ_context_set uctx
   in
   uctx', utyp, used_univs, Default { body = body; opaque = Opaque (ubody, eff) }
 
@@ -1232,7 +1235,7 @@ module ProgramDecl = struct
       else
         (* declare global univs of the main constant before we do obligations *)
         let uctx = UState.collapse_sort_variables uctx in
-        let ctx = UState.check_mono_sort_constraints @@ UState.context_set uctx in
+        let ctx = UState.check_mono_sort_constraints uctx in
         let () = Global.push_context_set ctx in
         let cst = Constant.make2 (Lib.current_mp()) cinfo.CInfo.name in
         let () = DeclareUniv.declare_univ_binders (ConstRef cst)
@@ -2911,7 +2914,7 @@ let declare_entry ?loc ~name ?scope ~kind ?user_warns ?hook ~impargs ~uctx entry
 
 let declare_definition_full ~info ~cinfo ~opaque ~body ?using sigma =
   let c, uctx = declare_definition ~obls:[] ~info ~cinfo ~opaque ~body ?using sigma in
-  c, if info.poly then PConstraints.ContextSet.empty else UState.context_set uctx
+  c, if info.poly then Univ.ContextSet.empty else PConstraints.ContextSet.univ_context_set @@ UState.context_set uctx
 
 let declare_definition ~info ~cinfo ~opaque ~body ?using sigma =
   declare_definition ~obls:[] ~info ~cinfo ~opaque ~body ?using sigma |> fst

vernac/declare.mli

@@ -465,7 +465,7 @@ val declare_definition_full
   -> body:EConstr.t
   -> ?using:Vernacexpr.section_subset_expr
   -> Evd.evar_map
-  -> GlobRef.t * PConstraints.ContextSet.t
+  -> GlobRef.t * Univ.ContextSet.t
 
 (** Declaration messages, for internal use *)