aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/uState.ml14
-rw-r--r--engine/uState.mli6
-rw-r--r--engine/univMinim.ml8
-rw-r--r--engine/univMinim.mli2
-rw-r--r--engine/univops.mli2
-rw-r--r--kernel/environ.ml4
-rw-r--r--kernel/environ.mli6
-rw-r--r--kernel/indTyping.ml2
-rw-r--r--kernel/uGraph.ml6
-rw-r--r--kernel/uGraph.mli10
-rw-r--r--library/global.mli2
-rw-r--r--vernac/comInductive.ml2
-rw-r--r--vernac/record.ml2
13 files changed, 43 insertions, 23 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 00649ce042..99ac5f2ce8 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -34,7 +34,7 @@ type t =
(** The subset of unification variables that can be instantiated with
algebraic universes as they appear in inferred types only. *)
uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
- uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *)
+ uctx_universes_lbound : UGraph.Bound.t; (** The lower bound on universes (e.g. Set or Prop) *)
uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
uctx_weak_constraints : UPairSet.t
}
@@ -48,7 +48,7 @@ let empty =
uctx_univ_variables = LMap.empty;
uctx_univ_algebraic = LSet.empty;
uctx_universes = initial_sprop_cumulative;
- uctx_universes_lbound = Univ.Level.set;
+ uctx_universes_lbound = UGraph.Bound.Set;
uctx_initial_universes = initial_sprop_cumulative;
uctx_weak_constraints = UPairSet.empty; }
@@ -443,6 +443,10 @@ let check_univ_decl ~poly uctx decl =
(ContextSet.constraints uctx.uctx_local);
ctx
+let is_bound l lbound = match lbound with
+| UGraph.Bound.Prop -> Level.is_prop l
+| UGraph.Bound.Set -> Level.is_set l
+
let restrict_universe_context ~lbound (univs, csts) keep =
let removed = LSet.diff univs keep in
if LSet.is_empty removed then univs, csts
@@ -455,7 +459,7 @@ let restrict_universe_context ~lbound (univs, csts) keep =
let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in
let csts = UGraph.constraints_for ~kept:allkept g in
let csts = Constraint.filter (fun (l,d,r) ->
- not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
+ not ((is_bound l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
(LSet.inter univs keep, csts)
let restrict ctx vars =
@@ -600,10 +604,10 @@ let make_with_initial_binders ~lbound e us =
let add_global_univ uctx u =
let initial =
- UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes
+ UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_initial_universes
in
let univs =
- UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes
+ UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_universes
in
{ uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local;
uctx_initial_universes = initial;
diff --git a/engine/uState.mli b/engine/uState.mli
index 6707826aae..533a501b59 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -25,9 +25,9 @@ type t
val empty : t
-val make : lbound:Univ.Level.t -> UGraph.t -> t
+val make : lbound:UGraph.Bound.t -> UGraph.t -> t
-val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t
+val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
val is_empty : t -> bool
@@ -90,7 +90,7 @@ val universe_of_name : t -> Id.t -> Univ.Level.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 : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:UGraph.Bound.t -> ContextSet.t -> LSet.t -> ContextSet.t
(** [restrict uctx ctx] restricts the local universes of [uctx] to
[ctx] extended by local named universes and side effect universes
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index c05a7a800d..4dd7fe7e70 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -267,12 +267,16 @@ let minimize_univ_variables ctx us algs left right cstrs =
module UPairs = OrderedType.UnorderedPair(Univ.Level)
module UPairSet = Set.Make (UPairs)
+let is_bound l lbound = match lbound with
+| UGraph.Bound.Prop -> Level.is_prop l
+| UGraph.Bound.Set -> Level.is_set l
+
(* TODO check is_small/sprop *)
let normalize_context_set ~lbound g ctx us algs weak =
let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
(* Keep the Prop/Set <= i constraints separate for minimization *)
let smallles, csts =
- Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts
+ Constraint.partition (fun (l,d,r) -> d == Le && (is_bound l lbound || Level.is_sprop l)) csts
in
let smallles = if get_set_minimization ()
then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles
@@ -299,7 +303,7 @@ let normalize_context_set ~lbound g ctx us algs weak =
(* We ignore the trivial Prop/Set <= i constraints. *)
let noneqs =
Constraint.filter
- (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) ||
+ (fun (l,d,r) -> not ((d == Le && is_bound l lbound) ||
(Level.is_prop l && d == Lt && Level.is_set r)))
csts
in
diff --git a/engine/univMinim.mli b/engine/univMinim.mli
index 2a46d87609..58853e47b8 100644
--- a/engine/univMinim.mli
+++ b/engine/univMinim.mli
@@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t)
(a global one if there is one) and transitively saturate
the constraints w.r.t to the equalities. *)
-val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t ->
+val normalize_context_set : lbound:UGraph.Bound.t -> UGraph.t -> ContextSet.t ->
universe_opt_subst (* The defined and undefined variables *) ->
LSet.t (* univ variables that can be substituted by algebraics *) ->
UPairSet.t (* weak equality constraints *) ->
diff --git a/engine/univops.mli b/engine/univops.mli
index 02a731ad49..d0145f5643 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -15,5 +15,5 @@ open Univ
val universes_of_constr : constr -> LSet.t
[@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
-val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:UGraph.Bound.t -> ContextSet.t -> LSet.t -> ContextSet.t
[@@ocaml.deprecated "Use [UState.restrict_universe_context]"]
diff --git a/kernel/environ.ml b/kernel/environ.ml
index d6d52dbc2b..182ed55d0e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -67,7 +67,7 @@ end
type stratification = {
env_universes : UGraph.t;
env_sprop_allowed : bool;
- env_universes_lbound : Univ.Level.t;
+ env_universes_lbound : UGraph.Bound.t;
env_engagement : engagement
}
@@ -129,7 +129,7 @@ let empty_env = {
env_stratification = {
env_universes = UGraph.initial_universes;
env_sprop_allowed = true;
- env_universes_lbound = Univ.Level.set;
+ env_universes_lbound = UGraph.Bound.Set;
env_engagement = PredicativeSet };
env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
retroknowledge = Retroknowledge.empty;
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 7a46538772..79e632daa0 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -62,7 +62,7 @@ end
type stratification = {
env_universes : UGraph.t;
env_sprop_allowed : bool;
- env_universes_lbound : Univ.Level.t;
+ env_universes_lbound : UGraph.Bound.t;
env_engagement : engagement
}
@@ -96,8 +96,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
val empty_env : env
val universes : env -> UGraph.t
-val universes_lbound : env -> Univ.Level.t
-val set_universes_lbound : env -> Univ.Level.t -> env
+val universes_lbound : env -> UGraph.Bound.t
+val set_universes_lbound : env -> UGraph.Bound.t -> env
val rel_context : env -> Constr.rel_context
val named_context : env -> Constr.named_context
val named_context_val : env -> named_context_val
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 8ac96a6481..e9687991c0 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -321,7 +321,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
if has_template_poly then
(* For that particular case, we typecheck the inductive in an environment
where the universes introduced by the definition are only [>= Prop] *)
- let env = set_universes_lbound env Univ.Level.prop in
+ let env = set_universes_lbound env UGraph.Bound.Prop in
push_context_set ~strict:false ctx env
else
(* In the regular case, all universes are [> Set] *)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5f5f0ef8cd..927db9e9e6 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -148,8 +148,14 @@ let enforce_leq_alg u v g =
assert (check_leq g u v);
cg
+module Bound =
+struct
+ type t = Prop | Set
+end
+
exception AlreadyDeclared = G.AlreadyDeclared
let add_universe u ~lbound ~strict g =
+ let lbound = match lbound with Bound.Prop -> Level.prop | Bound.Set -> Level.set in
let graph = G.add u g.graph in
let d = if strict then Lt else Le in
enforce_constraint (lbound,d,u) {g with graph}
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 8d9afb0990..c9fbd7f694 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -48,7 +48,13 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
exception AlreadyDeclared
-val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t
+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
(** Add a universe without (Prop,Set) <= u *)
val add_universe_unconstrained : Level.t -> t -> t
@@ -86,7 +92,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t
val domain : t -> LSet.t
(** Known universes *)
-val check_subtype : lbound:Level.t -> AUContext.t check_function
+val check_subtype : lbound:Bound.t -> AUContext.t check_function
(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
[ctx1]. *)
diff --git a/library/global.mli b/library/global.mli
index 2acd7e2a67..2767594171 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -22,7 +22,7 @@ val env : unit -> Environ.env
val env_is_initial : unit -> bool
val universes : unit -> UGraph.t
-val universes_lbound : unit -> Univ.Level.t
+val universes_lbound : unit -> UGraph.Bound.t
val named_context_val : unit -> Environ.named_context_val
val named_context : unit -> Constr.named_context
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index cc9b840bed..4242f06844 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -475,7 +475,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let indnames = List.map (fun ind -> ind.ind_name) indl in
(* In case of template polymorphism, we need to compute more constraints *)
- let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in
+ let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) =
interp_params env0 udecl uparamsl paramsl
diff --git a/vernac/record.ml b/vernac/record.ml
index 9fda98d08e..36254780cd 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -121,7 +121,7 @@ let typecheck_params_and_fields def poly pl ps records =
any Set <= i constraint for universes that might actually be instantiated with Prop. *)
let is_template =
List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
- let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in
+ let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
let () =
let error bk {CAst.loc; v=name} =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:30:38 +0000