From f0dfe68527c0a2df37987ccf55271b63243ea5c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 17 Jan 2025 15:54:28 +0100 Subject: [PATCH] Delete UGraph.Bound (now unused) --- engine/uState.ml | 15 +++++++-------- engine/univMinim.ml | 4 ++-- kernel/environ.ml | 17 +++++++---------- kernel/environ.mli | 3 --- kernel/uGraph.ml | 13 ++----------- kernel/uGraph.mli | 8 +------- vernac/vernacentries.ml | 2 +- 7 files changed, 20 insertions(+), 42 deletions(-) diff --git a/engine/uState.ml b/engine/uState.ml index 0da0c9f77b..d606b14225 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -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 @@ -952,7 +952,7 @@ let restrict_universe_context (univs, csts) keep = 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:Set ~strict:false g) allunivs g in + 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 @@ -991,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 @@ -1052,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 @@ -1077,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 @@ -1119,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 diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 240a5489fa..661c50ab72 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -352,12 +352,12 @@ let normalize_context_set g ctx (us:UnivFlex.t) {weak_constraints=weak;above_pro 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 diff --git a/kernel/environ.ml b/kernel/environ.ml index c55cb06e62..ebb27195ee 100644 --- a/kernel/environ.ml +++ b/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 diff --git a/kernel/environ.mli b/kernel/environ.mli index 2a8d6ac575..19e636cb01 100644 --- a/kernel/environ.mli +++ b/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 diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 93dbd8913c..029349f3fd 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -161,20 +161,11 @@ let enforce_leq_alg u v g = let e = UniverseInconsistency (None, (c, mk u, mk v, Some (Path e))) in raise e -module Bound = -struct - type t = Prop | Set -end - exception AlreadyDeclared = G.AlreadyDeclared -let add_universe u ~lbound ~strict g = match lbound with -| Bound.Set -> +let add_universe u ~strict g = let graph = G.add u g.graph in let d = if strict then Lt else Le in enforce_constraint (Level.set, d, u) { g with graph } -| Bound.Prop -> - (* Do not actually add any constraint. This is a hack for template. *) - { g with graph = G.add u g.graph } let check_declared_universes g l = G.check_declared g.graph l @@ -195,7 +186,7 @@ let check_subtype univs ctxT ctx = let inst = UContext.instance uctx in let cst = UContext.constraints uctx in let cstT = UContext.constraints (AbstractContext.repr ctxT) in - let push accu v = add_universe v ~lbound:Bound.Set ~strict:false accu in + let push accu v = add_universe v ~strict:false accu in let univs = Array.fold_left push univs (snd (Instance.to_array inst)) in let univs = merge_constraints cstT univs in check_constraints cst univs diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 5270e7a717..0f5b8d8eb1 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -71,13 +71,7 @@ val enforce_leq_alg : Univ.Universe.t -> Univ.Universe.t -> t -> Univ.Constraint exception AlreadyDeclared -module Bound : -sig - type t = Prop | Set - (** The [Prop] bound is only used for template polymorphic inductive types. *) -end - -val add_universe : Level.t -> lbound:Bound.t -> strict:bool -> t -> t +val add_universe : Level.t -> strict:bool -> t -> t (** Check that the universe levels are declared. *) val check_declared_universes : t -> Univ.Level.Set.t -> (unit, Univ.Level.Set.t) result diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7d71e2f947..29f66409b0 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -449,7 +449,7 @@ let universe_subgraph kept univ = let csts = UGraph.constraints_for ~kept univ in let add u newgraph = let strict = UGraph.check_constraint univ (Level.set,Lt,u) in - UGraph.add_universe u ~lbound:UGraph.Bound.Set ~strict newgraph + UGraph.add_universe u ~strict newgraph in let univ = Level.Set.fold add kept UGraph.initial_universes in UGraph.merge_constraints csts univ -- knotmirror 0.0.1