aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/declarations.ml5
-rw-r--r--kernel/declareops.ml1
-rw-r--r--kernel/environ.ml58
-rw-r--r--kernel/environ.mli10
-rw-r--r--kernel/indTyping.ml70
-rw-r--r--kernel/indTyping.mli9
-rw-r--r--kernel/mod_typing.ml3
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/subtyping.ml3
-rw-r--r--kernel/uGraph.ml8
-rw-r--r--kernel/uGraph.mli4
11 files changed, 138 insertions, 35 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 8d32684b09..44676c9da5 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -87,6 +87,11 @@ type typing_flags = {
indices_matter: bool;
(** The universe of an inductive type must be above that of its indices. *)
+
+ check_template : bool;
+ (* If [false] then we don't check that the universes template-polymorphic
+ inductive parameterize on are necessarily local and unbounded from below.
+ This potentially introduces inconsistencies. *)
}
(* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 391b139496..7225671a1e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,6 +26,7 @@ let safe_flags oracle = {
enable_VM = true;
enable_native_compiler = true;
indices_matter = true;
+ check_template = true;
}
(** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 655094e88b..4a2aeea22d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -59,8 +59,9 @@ type globals = {
type stratification = {
env_universes : UGraph.t;
- env_engagement : engagement;
env_sprop_allowed : bool;
+ env_universes_lbound : Univ.Level.t;
+ env_engagement : engagement
}
type val_kind =
@@ -119,9 +120,9 @@ let empty_env = {
env_nb_rel = 0;
env_stratification = {
env_universes = UGraph.initial_universes;
- env_engagement = PredicativeSet;
env_sprop_allowed = false;
- };
+ env_universes_lbound = Univ.Level.set;
+ env_engagement = PredicativeSet };
env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
retroknowledge = Retroknowledge.empty;
indirect_pterms = Opaqueproof.empty_opaquetab;
@@ -262,8 +263,15 @@ let type_in_type env = not (typing_flags env).check_universes
let deactivated_guard env = not (typing_flags env).check_guarded
let indices_matter env = env.env_typing_flags.indices_matter
+let check_template env = env.env_typing_flags.check_template
let universes env = env.env_stratification.env_universes
+let universes_lbound env = env.env_stratification.env_universes_lbound
+
+let set_universes_lbound env lbound =
+ let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in
+ { env with env_stratification }
+
let named_context env = env.env_named_context.env_named_ctx
let named_context_val env = env.env_named_context
let rel_context env = env.env_rel_context.env_rel_ctx
@@ -382,29 +390,30 @@ let check_constraints c env =
let push_constraints_to_env (_,univs) env =
add_constraints univs env
-let add_universes strict ctx g =
+let add_universes ~lbound ~strict ctx g =
let g = Array.fold_left
- (fun g v -> UGraph.add_universe v strict g)
+ (fun g v -> UGraph.add_universe ~lbound ~strict v g)
g (Univ.Instance.to_array (Univ.UContext.instance ctx))
in
UGraph.merge_constraints (Univ.UContext.constraints ctx) g
let push_context ?(strict=false) ctx env =
- map_universes (add_universes strict ctx) env
+ map_universes (add_universes ~lbound:(universes_lbound env) ~strict ctx) env
-let add_universes_set strict ctx g =
+let add_universes_set ~lbound ~strict ctx g =
let g = Univ.LSet.fold
(* Be lenient, module typing reintroduces universes and constraints due to includes *)
- (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
+ (fun v g -> try UGraph.add_universe ~lbound ~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 strict ctx) env
+ map_universes (add_universes_set ~lbound:(universes_lbound env) ~strict ctx) env
let push_subgraph (levels,csts) env =
+ let lbound = universes_lbound env in
let add_subgraph g =
- let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in
+ let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) levels g in
let newg = UGraph.merge_constraints csts newg in
(if not (Univ.Constraint.is_empty csts) then
let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in
@@ -428,6 +437,7 @@ let same_flags {
share_reduction;
enable_VM;
enable_native_compiler;
+ check_template;
} alt =
check_guarded == alt.check_guarded &&
check_positive == alt.check_positive &&
@@ -436,7 +446,8 @@ let same_flags {
indices_matter == alt.indices_matter &&
share_reduction == alt.share_reduction &&
enable_VM == alt.enable_VM &&
- enable_native_compiler == alt.enable_native_compiler
+ enable_native_compiler == alt.enable_native_compiler &&
+ check_template == alt.check_template
[@warning "+9"]
let set_typing_flags c env = (* Unsafe *)
@@ -568,11 +579,20 @@ let polymorphic_pind (ind,u) env =
let type_in_type_ind (mind,_i) env =
not (lookup_mind mind env).mind_typing_flags.check_universes
+let template_checked_ind (mind,_i) env =
+ (lookup_mind mind env).mind_typing_flags.check_template
+
let template_polymorphic_ind (mind,i) env =
match (lookup_mind mind env).mind_packets.(i).mind_arity with
| TemplateArity _ -> true
| RegularArity _ -> false
+let template_polymorphic_variables (mind,i) env =
+ match (lookup_mind mind env).mind_packets.(i).mind_arity with
+ | TemplateArity { Declarations.template_param_levels = l; _ } ->
+ List.map_filter (fun level -> level) l
+ | RegularArity _ -> []
+
let template_polymorphic_pind (ind,u) env =
if not (Univ.Instance.is_empty u) then false
else template_polymorphic_ind ind env
@@ -762,6 +782,22 @@ let is_template_polymorphic env r =
| IndRef ind -> template_polymorphic_ind ind env
| ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env
+let get_template_polymorphic_variables env r =
+ let open Names.GlobRef in
+ match r with
+ | VarRef _id -> []
+ | ConstRef _c -> []
+ | IndRef ind -> template_polymorphic_variables ind env
+ | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env
+
+let is_template_checked env r =
+ let open Names.GlobRef in
+ match r with
+ | VarRef _id -> false
+ | ConstRef _c -> false
+ | IndRef ind -> template_checked_ind ind env
+ | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env
+
let is_type_in_type env r =
let open Names.GlobRef in
match r with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index e6d814ac7d..f7de98dcfb 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -51,8 +51,9 @@ type globals
type stratification = {
env_universes : UGraph.t;
- env_engagement : engagement;
env_sprop_allowed : bool;
+ env_universes_lbound : Univ.Level.t;
+ env_engagement : engagement
}
type named_context_val = private {
@@ -85,6 +86,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 rel_context : env -> Constr.rel_context
val named_context : env -> Constr.named_context
val named_context_val : env -> named_context_val
@@ -99,6 +102,7 @@ val is_impredicative_set : env -> bool
val type_in_type : env -> bool
val deactivated_guard : env -> bool
val indices_matter : env -> bool
+val check_template : env -> bool
val is_impredicative_sort : env -> Sorts.t -> bool
val is_impredicative_univ : env -> Univ.Universe.t -> bool
@@ -254,7 +258,9 @@ val type_in_type_ind : inductive -> env -> bool
(** Old-style polymorphism *)
val template_polymorphic_ind : inductive -> env -> bool
+val template_polymorphic_variables : inductive -> env -> Univ.Level.t list
val template_polymorphic_pind : pinductive -> env -> bool
+val template_checked_ind : inductive -> env -> bool
(** {5 Modules } *)
@@ -346,6 +352,8 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat
val is_polymorphic : env -> Names.GlobRef.t -> bool
val is_template_polymorphic : env -> GlobRef.t -> bool
+val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list
+val is_template_checked : env -> GlobRef.t -> bool
val is_type_in_type : env -> GlobRef.t -> bool
(** Native compiler *)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index c8e04b9fee..06d2e1bb21 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -236,22 +236,53 @@ let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_}
if not ind_squashed then InType
else Sorts.family (Sorts.sort_of_univ ind_univ)
+(* For a level to be template polymorphic, it must be introduced
+ by the definition (so have no constraint except lbound <= l)
+ and not to be constrained from below, so any universe l' <= l
+ can be used as an instance of l. All bounds from above, i.e.
+ l <=/< r will be valid for any l' <= l. *)
+let unbounded_from_below u cstrs =
+ Univ.Constraint.for_all (fun (l, d, r) ->
+ match d with
+ | Eq -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u)
+ | Lt | Le -> not (Univ.Level.equal r u))
+ cstrs
+
(* Returns the list [x_1, ..., x_n] of levels contributing to template
- polymorphism. The elements x_k is None if the k-th parameter (starting
- from the most recent and ignoring let-definitions) is not contributing
- or is Some u_k if its level is u_k and is contributing. *)
-let param_ccls paramsctxt =
+ polymorphism. The elements x_k is None if the k-th parameter
+ (starting from the most recent and ignoring let-definitions) is not
+ contributing to the inductive type's sort or is Some u_k if its level
+ is u_k and is contributing. *)
+let template_polymorphic_univs ~template_check uctx paramsctxt concl =
+ let check_level l =
+ if Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
+ unbounded_from_below l (Univ.ContextSet.constraints uctx) then
+ Some l
+ else None
+ in
+ let univs = Univ.Universe.levels concl in
+ let univs =
+ if template_check then
+ Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs
+ else univs (* Doesn't check the universes can be generalized *)
+ in
let fold acc = function
| (LocalAssum (_, p)) ->
(let c = Term.strip_prod_assum p in
match kind c with
- | Sort (Type u) -> Univ.Universe.level u
+ | Sort (Type u) ->
+ if template_check then
+ (match Univ.Universe.level u with
+ | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None
+ | None -> None)
+ else Univ.Universe.level u
| _ -> None) :: acc
| LocalDef _ -> acc
in
- List.fold_left fold [] paramsctxt
+ let params = List.fold_left fold [] paramsctxt in
+ params, univs
-let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
let arity = Vars.subst_univs_level_constr usubst arity in
let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in
let indices = Vars.subst_univs_level_context usubst indices in
@@ -264,14 +295,20 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
let ind_univ = Univ.subst_univs_level_universe usubst univ_info.ind_univ in
let arity = match univ_info.ind_min_univ with
- | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ}
+ | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ}
| Some min_univ ->
- ((match univs with
- | Monomorphic _ -> ()
+ let ctx = match univs with
+ | Monomorphic ctx -> ctx
| Polymorphic _ ->
CErrors.anomaly ~label:"polymorphic_template_ind"
- Pp.(strbrk "Template polymorphism and full polymorphism are incompatible."));
- TemplateArity {template_param_levels=param_ccls params; template_level=min_univ})
+ Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
+ let param_levels, concl_levels = template_polymorphic_univs ~template_check ctx params min_univ in
+ if template_check && List.for_all (fun x -> Option.is_empty x) param_levels
+ && Univ.LSet.is_empty concl_levels then
+ CErrors.anomaly ~label:"polymorphic_template_ind"
+ Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
+ else
+ TemplateArity {template_param_levels = param_levels; template_level = min_univ}
in
let kelim = allowed_sorts univ_info in
@@ -286,10 +323,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
mind_check_names mie;
assert (List.is_empty (Environ.rel_context env));
+ let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in
+
(* universes *)
let env_univs =
match mie.mind_entry_universes with
- | Monomorphic_entry ctx -> push_context_set ctx env
+ | Monomorphic_entry ctx ->
+ let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in
+ push_context_set ctx env
| Polymorphic_entry (_, ctx) -> push_context ctx env
in
@@ -335,7 +376,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
(* Abstract universes *)
let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
let params = Vars.subst_univs_level_context usubst params in
- let data = List.map (abstract_packets univs usubst params) data in
+ let template_check = Environ.check_template env in
+ let data = List.map (abstract_packets ~template_check univs usubst params) data in
let env_ar_par =
let ctx = Environ.rel_context env_ar_par in
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index aaa0d6a149..8da4e2885c 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -33,3 +33,12 @@ val typecheck_inductive : env -> mutual_inductive_entry ->
(Constr.rel_context * (Constr.rel_context * Constr.types) array) *
Sorts.family)
array
+
+(* Utility function to compute the actual universe parameters
+ of a template polymorphic inductive *)
+val template_polymorphic_univs :
+ template_check:bool ->
+ Univ.ContextSet.t ->
+ Constr.rel_context ->
+ Univ.Universe.t ->
+ Univ.Level.t option list * Univ.LSet.t
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 9305a91731..ccc218771a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -94,7 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
c', Monomorphic Univ.ContextSet.empty, cst
| Polymorphic uctx, Some ctx ->
let () =
- if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
+ if not (UGraph.check_subtype ~lbound:(Environ.universes_lbound env)
+ (Environ.universes env) uctx ctx) then
error_incorrect_with_constraint lab
in
(** Terms are compared in a context with De Bruijn universe indices *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 53f228c618..327cb2efeb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -777,7 +777,7 @@ let infer_cmp_universes env pb s0 s1 univs =
| Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs
| Set, Prop -> raise NotConvertible
| Set, Type u -> infer_pb Univ.type0_univ u
- | Type _u, Prop -> raise NotConvertible
+ | Type u, Prop -> infer_pb u Univ.type0m_univ
| Type u, Set -> infer_pb u Univ.type0_univ
| Type u0, Type u1 -> infer_pb u0 u1
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d47dc0c6e1..d22ec3b7ca 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -97,7 +97,8 @@ let check_universes error env u1 u2 =
match u1, u2 with
| Monomorphic _, Monomorphic _ -> env
| Polymorphic auctx1, Polymorphic auctx2 ->
- if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+ let lbound = Environ.universes_lbound env in
+ if not (UGraph.check_subtype ~lbound (Environ.universes env) auctx2 auctx1) then
error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
else
Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 6fde6e9c5f..33336079bb 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -149,10 +149,10 @@ let enforce_leq_alg u v g =
cg
exception AlreadyDeclared = G.AlreadyDeclared
-let add_universe u strict g =
+let add_universe u ~lbound ~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}
+ enforce_constraint (lbound,d,u) {g with graph}
let add_universe_unconstrained u g = {g with graph=G.add u g.graph}
@@ -164,11 +164,11 @@ let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop k
(** Subtyping of polymorphic contexts *)
-let check_subtype univs ctxT ctx =
+let check_subtype ~lbound univs ctxT ctx =
if AUContext.size ctxT == AUContext.size ctx then
let (inst, cst) = UContext.dest (AUContext.repr ctx) in
let cstT = UContext.constraints (AUContext.repr ctxT) in
- let push accu v = add_universe v false accu in
+ let push accu v = add_universe v ~lbound ~strict:false accu in
let univs = Array.fold_left push univs (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 e1b5868d55..d90f01d8d1 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -48,7 +48,7 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
exception AlreadyDeclared
-val add_universe : Level.t -> bool -> t -> t
+val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t
(** Add a universe without (Prop,Set) <= u *)
val add_universe_unconstrained : Level.t -> t -> t
@@ -86,7 +86,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t
val domain : t -> LSet.t
(** Known universes *)
-val check_subtype : AUContext.t check_function
+val check_subtype : lbound:Level.t -> AUContext.t check_function
(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
[ctx1]. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:08:58 +0000