Merge PR #19985: Stop using lbound:Prop

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

Author: coqbot-app[bot]

dev/ci/user-overlays/19985-SkySkimmer-cominductive-lbound.sh

@@ -0,0 +1 @@
+overlay lean_importer https://github.com/SkySkimmer/coq-lean-import cominductive-lbound 19985

engine/evd.ml

@@ -1063,8 +1063,8 @@ let check_univ_decl_early ~poly ~with_obls sigma udecl terms =
   let uctx = UState.restrict uctx vars in
   ignore (UState.check_univ_decl ~poly uctx udecl)
 
-let restrict_universe_context ?lbound evd vars =
-  { evd with universes = UState.restrict ?lbound evd.universes vars }
+let restrict_universe_context evd vars =
+  { evd with universes = UState.restrict evd.universes vars }
 
 let universe_subst evd =
   UState.subst evd.universes
@@ -1211,10 +1211,13 @@ let collapse_sort_variables evd =
   let universes = UState.collapse_sort_variables evd.universes in
   { evd with universes }
 
-let minimize_universes ?lbound evd =
-  let uctx' = UState.collapse_sort_variables evd.universes in
+let minimize_universes ?(collapse_sort_variables=true) evd =
+  let uctx' = if collapse_sort_variables
+    then UState.collapse_sort_variables evd.universes
+    else evd.universes
+  in
   let uctx' = UState.normalize_variables uctx' in
-  let uctx' = UState.minimize ?lbound uctx' in
+  let uctx' = UState.minimize uctx' in
   {evd with universes = uctx'}
 
 let universe_of_name evd s = UState.universe_of_name evd.universes s

engine/evd.mli

@@ -535,7 +535,7 @@ val univ_flexible_alg : rigid
 
 type 'a in_ustate = 'a * UState.t
 
-val restrict_universe_context : ?lbound:UGraph.Bound.t -> evar_map -> Univ.Level.Set.t -> evar_map
+val restrict_universe_context : evar_map -> Univ.Level.Set.t -> evar_map
 
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
@@ -616,8 +616,8 @@ val collapse_sort_variables : evar_map -> evar_map
 
 val fix_undefined_variables : evar_map -> evar_map
 
-(** Universe minimization *)
-val minimize_universes : ?lbound:UGraph.Bound.t -> evar_map -> evar_map
+(** Universe minimization (collapse_sort_variables is true by default) *)
+val minimize_universes : ?collapse_sort_variables:bool -> evar_map -> evar_map
 
 (** Lift [UState.update_sigma_univs] *)
 val update_sigma_univs : UGraph.t -> evar_map -> evar_map

engine/uState.ml

@@ -238,7 +238,7 @@ let empty =
     initial_universes = UGraph.initial_universes;
     minim_extra = UnivMinim.empty_extra; }
 
-let make ~lbound univs =
+let make univs =
   { empty with
     universes = univs;
     initial_universes = univs }
@@ -313,7 +313,7 @@ let union uctx uctx' =
     let newus = Level.Set.diff newus (UnivFlex.domain uctx.univ_variables) in
     let extra = UnivMinim.extra_union uctx.minim_extra uctx'.minim_extra in
     let declarenew g =
-      Level.Set.fold (fun u g -> UGraph.add_universe u ~lbound:UGraph.Bound.Set ~strict:false g) newus g
+      Level.Set.fold (fun u g -> UGraph.add_universe u ~strict:false g) newus g
     in
     let fail_union s q1 q2 =
       if UGraph.type_in_type uctx.universes then s
@@ -944,33 +944,30 @@ let check_univ_decl ~poly uctx decl =
     else Monomorphic_entry (check_mono_univ_decl uctx decl) in
   entry, binders
 
-let is_bound l lbound = match lbound with
-  | UGraph.Bound.Prop -> false
-  | UGraph.Bound.Set -> Level.is_set l
-
-let restrict_universe_context ?(lbound = UGraph.Bound.Set) (univs, csts) keep =
+let restrict_universe_context (univs, csts) keep =
   let removed = Level.Set.diff univs keep in
   if Level.Set.is_empty removed then univs, csts
   else
   let allunivs = Constraints.fold (fun (u,_,v) all -> Level.Set.add u (Level.Set.add v all)) csts univs in
   let g = UGraph.initial_universes in
-  let g = Level.Set.fold (fun v g -> if Level.is_set v then g else
-                        UGraph.add_universe v ~lbound ~strict:false g) allunivs g in
+  let g = Level.Set.fold (fun v g ->
+      if Level.is_set v then g else
+        UGraph.add_universe v ~strict:false g) allunivs g in
   let g = UGraph.merge_constraints csts g in
   let allkept = Level.Set.union (UGraph.domain UGraph.initial_universes) (Level.Set.diff allunivs removed) in
   let csts = UGraph.constraints_for ~kept:allkept g in
-  let csts = Constraints.filter (fun (l,d,r) -> not (is_bound l lbound && d == Le)) csts in
+  let csts = Constraints.filter (fun (l,d,r) -> not (Level.is_set l && d == Le)) csts in
   (Level.Set.inter univs keep, csts)
 
-let restrict ?lbound uctx vars =
+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 ?lbound uctx.local vars in
+  let uctx' = restrict_universe_context uctx.local vars in
   { uctx with local = uctx' }
 
-let restrict_even_binders ?lbound uctx vars =
-  let uctx' = restrict_universe_context ?lbound uctx.local vars in
+let restrict_even_binders uctx vars =
+  let uctx' = restrict_universe_context uctx.local vars in
   { uctx with local = uctx' }
 
 let restrict_constraints uctx csts =
@@ -994,7 +991,7 @@ let merge ?loc ~sideff rigid uctx uctx' =
   let local = ContextSet.append uctx' uctx.local in
   let declare g =
     Level.Set.fold (fun u g ->
-        try UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:false u g
+        try UGraph.add_universe ~strict:false u g
         with UGraph.AlreadyDeclared when sideff -> g)
       levels g
   in
@@ -1055,7 +1052,7 @@ let demote_global_univs (lvl_set,csts_set) uctx =
   let univ_variables = Level.Set.fold UnivFlex.remove lvl_set uctx.univ_variables in
   let update_ugraph g =
     let g = Level.Set.fold (fun u g ->
-        try UGraph.add_universe u ~lbound:Set ~strict:true g
+        try UGraph.add_universe u ~strict:true g
         with UGraph.AlreadyDeclared -> g)
         lvl_set
         g
@@ -1080,7 +1077,7 @@ let merge_seff uctx uctx' =
   let levels = ContextSet.levels uctx' in
   let declare g =
     Level.Set.fold (fun u g ->
-        try UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:false u g
+        try UGraph.add_universe ~strict:false u g
         with UGraph.AlreadyDeclared -> g)
       levels g
   in
@@ -1122,9 +1119,8 @@ let add_loc l loc (names, (qnames_rev,unames_rev) as orig) =
   | Some _ -> (names, (qnames_rev, Level.Map.add l { uname = None; uloc = loc } unames_rev))
 
 let add_universe ?loc name strict uctx u =
-  let lbound = UGraph.Bound.Set in
-  let initial_universes = UGraph.add_universe ~lbound ~strict u uctx.initial_universes in
-  let universes = UGraph.add_universe ~lbound ~strict u uctx.universes in
+  let initial_universes = UGraph.add_universe ~strict u uctx.initial_universes in
+  let universes = UGraph.add_universe ~strict u uctx.universes in
   let local = ContextSet.add_universe u uctx.local in
   let names =
     match name with
@@ -1159,15 +1155,15 @@ let new_univ_variable ?loc rigid name uctx =
 
 let add_forgotten_univ uctx u = add_universe None true uctx u
 
-let make_with_initial_binders ~lbound univs binders =
-  let uctx = make ~lbound univs in
+let make_with_initial_binders univs binders =
+  let uctx = make univs in
   List.fold_left
     (fun uctx { CAst.loc; v = id } ->
        fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
     uctx binders
 
 let from_env ?(binders=[]) env =
-  make_with_initial_binders ~lbound:UGraph.Bound.Set (Environ.universes env) binders
+  make_with_initial_binders (Environ.universes env) binders
 
 let make_nonalgebraic_variable uctx u =
   { uctx with univ_variables = UnivFlex.make_nonalgebraic_variable uctx.univ_variables u }
@@ -1198,10 +1194,10 @@ let collapse_above_prop_sort_variables ~to_prop uctx =
 let collapse_sort_variables uctx =
   { uctx with sort_variables = QState.collapse uctx.sort_variables }
 
-let minimize ?(lbound = UGraph.Bound.Set) uctx =
+let minimize uctx =
   let open UnivMinim in
   let (vars', us') =
-    normalize_context_set ~lbound uctx.universes uctx.local uctx.univ_variables
+    normalize_context_set uctx.universes uctx.local uctx.univ_variables
       uctx.minim_extra
   in
   if ContextSet.equal us' uctx.local then uctx

engine/uState.mli

@@ -32,10 +32,10 @@ type t
 
 val empty : t
 
-val make : lbound:UGraph.Bound.t -> UGraph.t -> t
+val make : UGraph.t -> t
 [@@ocaml.deprecated "(8.13) Use from_env"]
 
-val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
+val make_with_initial_binders : UGraph.t -> lident list -> t
 [@@ocaml.deprecated "(8.13) Use from_env"]
 
 val from_env : ?binders:lident list -> Environ.env -> t
@@ -143,24 +143,24 @@ val name_level : Univ.Level.t -> Id.t -> t -> t
 
 (** {5 Unification} *)
 
-(** [restrict_universe_context lbound (univs,csts) keep] restricts [univs] to
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
    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 : ?lbound:UGraph.Bound.t -> ContextSet.t -> Level.Set.t -> ContextSet.t
+val restrict_universe_context : ContextSet.t -> Level.Set.t -> ContextSet.t
 
 (** [restrict uctx ctx] restricts the local universes of [uctx] to
    [ctx] extended by local named universes and side effect universes
    (from [demote_seff_univs]). Transitive constraints between retained
    universes are preserved. *)
-val restrict : ?lbound:UGraph.Bound.t -> t -> Univ.Level.Set.t -> t
+val restrict : t -> Univ.Level.Set.t -> t
 
 
 (** [restrict_even_binders uctx ctx] restricts the local universes of [uctx] to
    [ctx] extended by side effect universes
    (from [demote_seff_univs]). Transitive constraints between retained
    universes are preserved. *)
-val restrict_even_binders : ?lbound:UGraph.Bound.t -> t -> Univ.Level.Set.t -> t
+val restrict_even_binders : t -> Univ.Level.Set.t -> t
 
 type rigid =
   | UnivRigid
@@ -222,7 +222,7 @@ val fix_undefined_variables : t -> t
 (** cf UnivFlex *)
 
 (** Universe minimization *)
-val minimize : ?lbound:UGraph.Bound.t -> t -> t
+val minimize : t -> t
 
 val collapse_above_prop_sort_variables : to_prop:bool -> t -> t
 

engine/univMinim.ml

@@ -306,7 +306,7 @@ let extra_union a b = {
   above_prop = Level.Set.union a.above_prop b.above_prop;
 }
 
-let normalize_context_set ~lbound g ctx (us:UnivFlex.t) {weak_constraints=weak;above_prop} =
+let normalize_context_set g ctx (us:UnivFlex.t) {weak_constraints=weak;above_prop} =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (* Keep the Set <= i constraints separate *)
   let smallles, csts =
@@ -338,11 +338,9 @@ let normalize_context_set ~lbound g ctx (us:UnivFlex.t) {weak_constraints=weak;a
         else acc)
       weak (smallles, csts, g)
   in
-  let smallles = match (lbound : UGraph.Bound.t) with
-    | Prop -> smallles
-    | Set when get_set_minimization () ->
+  let smallles = if get_set_minimization () then
       Constraints.filter (fun (l,d,r) -> UnivFlex.mem r us) smallles
-    | Set -> Constraints.empty (* constraints Set <= u may be dropped *)
+    else  Constraints.empty (* constraints Set <= u may be dropped *)
   in
   let smallles = if get_set_minimization() then
       let fold u accu = if UnivFlex.mem u us then Constraints.add (Level.set, Le, u) accu else accu in
@@ -354,12 +352,12 @@ let normalize_context_set ~lbound g ctx (us:UnivFlex.t) {weak_constraints=weak;a
        to equalities. *)
     let g = UGraph.initial_universes_with g in
     (* use lbound:Set to collapse [u <= v <= Set] into [u = v = Set] *)
-    let g = Level.Set.fold (fun v g -> UGraph.add_universe ~lbound:Set ~strict:false v g)
+    let g = Level.Set.fold (fun v g -> UGraph.add_universe ~strict:false v g)
         ctx g
     in
     let add_soft u g =
       if not (Level.is_set u || Level.Set.mem u ctx)
-      then try UGraph.add_universe ~lbound:Set ~strict:false u g with UGraph.AlreadyDeclared -> g
+      then try UGraph.add_universe ~strict:false u g with UGraph.AlreadyDeclared -> g
       else g
     in
     let g = Constraints.fold

engine/univMinim.mli

@@ -33,7 +33,7 @@ val extra_union : extra -> extra -> extra
     (a global one if there is one) and transitively saturate
     the constraints w.r.t to the equalities. *)
 
-val normalize_context_set : lbound:UGraph.Bound.t -> UGraph.t -> ContextSet.t ->
+val normalize_context_set : UGraph.t -> ContextSet.t ->
   UnivFlex.t (* The defined and undefined variables *) ->
   extra ->
   UnivFlex.t in_universe_context_set

kernel/declareops.ml

@@ -49,7 +49,8 @@ let map_decl_arity f g = function
   | TemplateArity a -> TemplateArity (g a)
 
 let hcons_template_arity ar =
-  { template_level = Sorts.hcons ar.template_level; }
+  { template_level = Sorts.hcons ar.template_level;
+  }
 
 let hcons_template_universe ar =
   { template_param_arguments = ar.template_param_arguments;

kernel/environ.ml

@@ -459,10 +459,10 @@ let add_constraints c env =
 let check_constraints c env =
   UGraph.check_constraints c env.env_universes
 
-let add_universes ~lbound ~strict ctx g =
+let add_universes ~strict ctx g =
   let _qs, us = UVars.Instance.to_array (UVars.UContext.instance ctx) in
   let g = Array.fold_left
-      (fun g v -> UGraph.add_universe ~lbound ~strict v g)
+      (fun g v -> UGraph.add_universe ~strict v g)
       g us
   in
   UGraph.merge_constraints (UVars.UContext.constraints ctx) g
@@ -482,24 +482,21 @@ let add_qualities qs known =
 let push_context ?(strict=false) ctx env =
   let qs, _us = UVars.Instance.to_array (UVars.UContext.instance ctx) in
   let env = { env with env_qualities = add_qualities qs env.env_qualities } in
-  map_universes (add_universes ~lbound:UGraph.Bound.Set ~strict ctx) env
+  map_universes (add_universes ~strict ctx) env
 
-let add_universes_set ~lbound ~strict ctx g =
+let add_universes_set ~strict ctx g =
   let g = Univ.Level.Set.fold
             (* Be lenient, module typing reintroduces universes and constraints due to includes *)
-            (fun v g -> try UGraph.add_universe ~lbound ~strict v g with UGraph.AlreadyDeclared -> g)
+            (fun v g -> try UGraph.add_universe ~strict v g with UGraph.AlreadyDeclared -> g)
             (Univ.ContextSet.levels ctx) g
   in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g
 
 let push_context_set ?(strict=false) ctx env =
-  map_universes (add_universes_set ~lbound:UGraph.Bound.Set ~strict ctx) env
-
-let push_floating_context_set ctx env =
-  map_universes (add_universes_set ~lbound:UGraph.Bound.Prop ~strict:false ctx) env
+  map_universes (add_universes_set ~strict ctx) env
 
 let push_subgraph (levels,csts) env =
   let add_subgraph g =
-    let newg = Univ.Level.Set.fold (fun v g -> UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:false v g) levels g in
+    let newg = Univ.Level.Set.fold (fun v g -> UGraph.add_universe ~strict:false v g) levels g in
     let newg = UGraph.merge_constraints csts newg in
     (if not (Univ.Constraints.is_empty csts) then
        let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in

kernel/environ.mli

@@ -372,9 +372,6 @@ val push_context_set : ?strict:bool -> ContextSet.t -> env -> env
     context set to the environment. It does not fail even if one of the
     universes is already declared. *)
 
-val push_floating_context_set : ContextSet.t -> env -> env
-(** Same as above but keep the universes floating for template. Do not use. *)
-
 val push_subgraph : ContextSet.t -> env -> env
 (** [push_subgraph univs env] adds the universes and constraints in
    [univs] to [env] as [push_context_set ~strict:false univs env], and