aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/indTyping.ml30
-rw-r--r--kernel/indTyping.mli1
-rw-r--r--kernel/reduction.ml10
-rw-r--r--kernel/retypeops.ml30
-rw-r--r--kernel/retypeops.mli4
5 files changed, 47 insertions, 28 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 06d2e1bb21..c91cb39fe2 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -253,10 +253,11 @@ let unbounded_from_below u cstrs =
(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 template_polymorphic_univs ~template_check ~ctor_levels 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
+ unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
+ not (Univ.LSet.mem l ctor_levels) then
Some l
else None
in
@@ -302,10 +303,31 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
| Polymorphic _ ->
CErrors.anomaly ~label:"polymorphic_template_ind"
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
+ let ctor_levels =
+ let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
+ let param_levels =
+ List.fold_left (fun levels d -> match d with
+ | LocalAssum _ -> levels
+ | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
+ Univ.LSet.empty params
+ in
+ Array.fold_left
+ (fun levels (d,c) ->
+ let levels =
+ List.fold_left (fun levels d ->
+ Context.Rel.Declaration.fold_constr add_levels d levels)
+ levels d
+ in
+ add_levels c levels)
+ param_levels
+ splayed_lc
+ in
+ let param_levels, concl_levels =
+ template_polymorphic_univs ~template_check ~ctor_levels 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"
+ CErrors.user_err
Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
else
TemplateArity {template_param_levels = param_levels; template_level = min_univ}
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 8da4e2885c..5c04e860a2 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -38,6 +38,7 @@ val typecheck_inductive : env -> mutual_inductive_entry ->
of a template polymorphic inductive *)
val template_polymorphic_univs :
template_check:bool ->
+ ctor_levels:Univ.LSet.t ->
Univ.ContextSet.t ->
Constr.rel_context ->
Univ.Universe.t ->
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f2cb9a8aec..b7bd4eef9a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -302,7 +302,7 @@ let unfold_ref_with_args infos tab fl v =
type conv_tab = {
cnv_inf : clos_infos;
- relevances : Sorts.relevance list;
+ relevances : Sorts.relevance Range.t;
lft_tab : clos_tab;
rgt_tab : clos_tab;
}
@@ -313,16 +313,16 @@ type conv_tab = {
passed to each respective side of the conversion function below. *)
let push_relevance infos r =
- { infos with relevances = r.Context.binder_relevance :: infos.relevances }
+ { infos with relevances = Range.cons r.Context.binder_relevance infos.relevances }
let push_relevances infos nas =
- { infos with relevances = Array.fold_left (fun l x -> x.Context.binder_relevance :: l) infos.relevances nas }
+ { infos with relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l) infos.relevances nas }
let rec skip_pattern infos relevances n c1 c2 =
if Int.equal n 0 then {infos with relevances}, c1, c2
else match kind c1, kind c2 with
| Lambda (x, _, c1), Lambda (_, _, c2) ->
- skip_pattern infos (x.Context.binder_relevance :: relevances) (pred n) c1 c2
+ skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2
| _ -> raise IrregularPatternShape
let skip_pattern infos n c1 c2 =
@@ -705,7 +705,7 @@ let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
let infos = create_clos_infos ~evars reds env in
let infos = {
cnv_inf = infos;
- relevances = List.map Context.Rel.Declaration.get_relevance (rel_context env);
+ relevances = Range.empty;
lft_tab = create_tab ();
rgt_tab = create_tab ();
} in
diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml
index 5c15257511..6a1b36ea94 100644
--- a/kernel/retypeops.ml
+++ b/kernel/retypeops.ml
@@ -39,16 +39,10 @@ let relevance_of_projection env p =
let mib = lookup_mind mind env in
Declareops.relevance_of_projection_repr mib (Projection.repr p)
-let rec relevance_of_rel_extra env extra n =
- match extra with
- | [] -> relevance_of_rel env n
- | r :: _ when Int.equal n 1 -> r
- | _ :: extra -> relevance_of_rel_extra env extra (n-1)
-
-let relevance_of_flex env extra lft = function
+let relevance_of_flex env = function
| ConstKey (c,_) -> relevance_of_constant env c
| VarKey x -> relevance_of_var env x
- | RelKey p -> relevance_of_rel_extra env extra (Esubst.reloc_rel p lft)
+ | RelKey p -> relevance_of_rel env p
let rec relevance_of_fterm env extra lft f =
let open CClosure in
@@ -57,9 +51,9 @@ let rec relevance_of_fterm env extra lft f =
| KnownI -> Sorts.Irrelevant
| Unknown ->
let r = match fterm_of f with
- | FRel n -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft)
+ | FRel n -> Range.get extra (Esubst.reloc_rel n lft - 1)
| FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c
- | FFlex key -> relevance_of_flex env extra lft key
+ | FFlex key -> relevance_of_flex env key
| FInt _ | FFloat _ -> Sorts.Relevant
| FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *)
| FConstruct (c,_) -> relevance_of_constructor env c
@@ -69,12 +63,12 @@ let rec relevance_of_fterm env extra lft f =
| FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance
| FCaseT (ci, _, _, _, _) -> ci.ci_relevance
| FLambda (len, tys, bdy, e) ->
- let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in
+ let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in
let lft = Esubst.el_liftn len lft in
let e = Esubst.subs_liftn len e in
relevance_of_term_extra env extra lft e bdy
| FLetIn (x, _, _, bdy, e) ->
- relevance_of_term_extra env (x.binder_relevance :: extra)
+ relevance_of_term_extra env (Range.cons x.binder_relevance extra)
(Esubst.el_lift lft) (Esubst.subs_lift e) bdy
| FLIFT (k, f) -> relevance_of_fterm env extra (Esubst.el_shft k lft) f
| FCLOS (c, e) -> relevance_of_term_extra env extra lft e c
@@ -88,16 +82,18 @@ let rec relevance_of_fterm env extra lft f =
and relevance_of_term_extra env extra lft subs c =
match kind c with
| Rel n ->
- (match Esubst.expand_rel n subs with
+ begin match Esubst.expand_rel n subs with
| Inl (k, f) -> relevance_of_fterm env extra (Esubst.el_liftn k lft) f
- | Inr (n, _) -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft))
+ | Inr (n, None) -> Range.get extra (Esubst.reloc_rel n lft - 1)
+ | Inr (_, Some p) -> relevance_of_rel env p
+ end
| Var x -> relevance_of_var env x
| Sort _ | Ind _ | Prod _ -> Sorts.Relevant (* types are always relevant *)
| Cast (c, _, _) -> relevance_of_term_extra env extra lft subs c
| Lambda ({binder_relevance=r;_}, _, bdy) ->
- relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
+ relevance_of_term_extra env (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
| LetIn ({binder_relevance=r;_}, _, _, bdy) ->
- relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
+ relevance_of_term_extra env (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
| App (c, _) -> relevance_of_term_extra env extra lft subs c
| Const (c,_) -> relevance_of_constant env c
| Construct (c,_) -> relevance_of_constructor env c
@@ -115,5 +111,5 @@ let relevance_of_fterm env extra lft c =
let relevance_of_term env c =
if Environ.sprop_allowed env
- then relevance_of_term_extra env [] Esubst.el_id (Esubst.subs_id 0) c
+ then relevance_of_term_extra env Range.empty Esubst.el_id (Esubst.subs_id 0) c
else Sorts.Relevant
diff --git a/kernel/retypeops.mli b/kernel/retypeops.mli
index f4497be44b..dd4513959f 100644
--- a/kernel/retypeops.mli
+++ b/kernel/retypeops.mli
@@ -14,14 +14,14 @@
val relevance_of_term : Environ.env -> Constr.constr -> Sorts.relevance
-val relevance_of_fterm : Environ.env -> Sorts.relevance list ->
+val relevance_of_fterm : Environ.env -> Sorts.relevance Range.t ->
Esubst.lift -> CClosure.fconstr ->
Sorts.relevance
(** Helpers *)
open Names
-val relevance_of_rel_extra : Environ.env -> Sorts.relevance list -> int -> Sorts.relevance
+val relevance_of_rel : Environ.env -> int -> Sorts.relevance
val relevance_of_var : Environ.env -> Id.t -> Sorts.relevance
val relevance_of_constant : Environ.env -> Constant.t -> Sorts.relevance
val relevance_of_constructor : Environ.env -> constructor -> Sorts.relevance
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 19:09:01 +0000