From 02cd67abde6a52d8a7c243a00474ae8115fe8696 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 6 Jan 2025 17:34:47 +0100 Subject: [PATCH] Cleanup "lbound" arguments which are always Set --- engine/evd.ml | 4 ++-- engine/evd.mli | 2 +- engine/uState.ml | 33 +++++++++++++++------------------ engine/uState.mli | 14 +++++++------- engine/univMinim.ml | 8 +++----- engine/univMinim.mli | 2 +- 6 files changed, 29 insertions(+), 34 deletions(-) diff --git a/engine/evd.ml b/engine/evd.ml index 2f5fe69fe670..b9f929f2f67a 100644 --- a/engine/evd.ml +++ b/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 diff --git a/engine/evd.mli b/engine/evd.mli index 9b8c47041487..57c6e598a892 100644 --- a/engine/evd.mli +++ b/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 diff --git a/engine/uState.ml b/engine/uState.ml index 9528b4263e24..0da0c9f77bca 100644 --- a/engine/uState.ml +++ b/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 } @@ -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 ~lbound:Set ~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 = @@ -1159,15 +1156,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 +1195,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 diff --git a/engine/uState.mli b/engine/uState.mli index 1d6a84e65676..dece121da634 100644 --- a/engine/uState.mli +++ b/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 diff --git a/engine/univMinim.ml b/engine/univMinim.ml index e024089c37b1..240a5489fa61 100644 --- a/engine/univMinim.ml +++ b/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 diff --git a/engine/univMinim.mli b/engine/univMinim.mli index 5a5d384d57c3..f1661730809b 100644 --- a/engine/univMinim.mli +++ b/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