aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checkInductive.ml3
-rw-r--r--checker/values.ml2
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/indTyping.ml13
-rw-r--r--kernel/indTyping.mli4
-rw-r--r--kernel/inductive.ml8
-rw-r--r--kernel/inductive.mli2
-rw-r--r--kernel/sorts.ml7
-rw-r--r--kernel/sorts.mli6
-rw-r--r--kernel/type_errors.ml2
-rw-r--r--kernel/type_errors.mli4
-rw-r--r--pretyping/indrec.ml6
-rw-r--r--pretyping/inductiveops.ml5
-rw-r--r--pretyping/inductiveops.mli4
-rw-r--r--pretyping/pretype_errors.mli2
-rw-r--r--pretyping/typing.ml12
-rw-r--r--tactics/equality.ml6
-rw-r--r--vernac/auto_ind_decl.ml4
-rw-r--r--vernac/himsg.ml1
-rw-r--r--vernac/indschemes.ml11
20 files changed, 47 insertions, 57 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 4f4527ca12..b66e198234 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -75,8 +75,7 @@ let check_arity env ar1 ar2 = match ar1, ar2 with
(* template_level is inferred by indtypes, so functor application can produce a smaller one *)
| (RegularArity _ | TemplateArity _), _ -> false
-let check_kelim k1 k2 =
- List.for_all (fun x -> List.mem_f Sorts.family_equal x k2) k1
+let check_kelim k1 k2 = Sorts.family_leq k1 k2
(* Use [eq_ind_chk] because when we rebuild the recargs we have lost
the knowledge of who is the canonical version.
diff --git a/checker/values.ml b/checker/values.ml
index 4b651cafb6..adee9b8bde 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -257,7 +257,7 @@ let v_one_ind = v_tuple "one_inductive_body"
Array v_constr;
Int;
Int;
- List v_sortfam;
+ v_sortfam;
Array (v_pair v_rctxt v_constr);
Array Int;
Array Int;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 860d19fe26..388b4f14bf 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -165,7 +165,7 @@ type one_inductive_body = {
mind_nrealdecls : int; (** Length of realargs context (with let, no params) *)
- mind_kelim : Sorts.family list; (** List of allowed elimination sorts *)
+ mind_kelim : Sorts.family; (** Highest allowed elimination sort *)
mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 4e6e595331..65298938fa 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -232,18 +232,9 @@ let check_record data =
(* - all_sorts in case of small, unitary Prop (not smashed) *)
(* - logical_sorts in case of large, unitary Prop (smashed) *)
-let all_sorts = [InSProp;InProp;InSet;InType]
-let small_sorts = [InSProp;InProp;InSet]
-let logical_sorts = [InSProp;InProp]
-let sprop_sorts = [InSProp]
-
let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} =
- if not ind_squashed then all_sorts
- else match Sorts.family (Sorts.sort_of_univ ind_univ) with
- | InType -> assert false
- | InSet -> small_sorts
- | InProp -> logical_sorts
- | InSProp -> sprop_sorts
+ if not ind_squashed then InType
+ else Sorts.family (Sorts.sort_of_univ ind_univ)
(* 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
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index ad51af66a2..ef2c30b76a 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -22,7 +22,7 @@ open Declarations
- for each inductive,
(arity * constructors) (with params)
* (indices * splayed constructor types) (both without params)
- * allowed eliminations
+ * top allowed elimination
*)
val typecheck_inductive : env -> mutual_inductive_entry ->
env
@@ -31,5 +31,5 @@ val typecheck_inductive : env -> mutual_inductive_entry ->
* Constr.rel_context
* ((inductive_arity * Constr.types array) *
(Constr.rel_context * (Constr.rel_context * Constr.types) array) *
- Sorts.family list)
+ Sorts.family)
array
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ca7086a3e4..beff8f4421 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -289,7 +289,7 @@ let get_instantiated_arity (_ind,u) (mib,mip) params =
let sign, s = mind_arity mip in
full_inductive_instantiate mib u params sign, s
-let elim_sorts (_,mip) = mip.mind_kelim
+let elim_sort (_,mip) = mip.mind_kelim
let is_private (mib,_) = mib.mind_private = Some true
let is_primitive_record (mib,_) =
@@ -305,12 +305,12 @@ let build_dependent_inductive ind (_,mip) params =
@ Context.Rel.to_extended_list mkRel 0 realargs)
(* This exception is local *)
-exception LocalArity of (Sorts.family list * Sorts.family * Sorts.family * arity_error) option
+exception LocalArity of (Sorts.family * Sorts.family * Sorts.family * arity_error) option
let check_allowed_sort ksort specif =
- if not (CList.exists (Sorts.family_equal ksort) (elim_sorts specif)) then
+ if not (Sorts.family_leq ksort (elim_sort specif)) then
let s = inductive_sort_family (snd specif) in
- raise (LocalArity (Some(elim_sorts specif, ksort,s,error_elim_explain ksort s)))
+ raise (LocalArity (Some(elim_sort specif, ksort,s,error_elim_explain ksort s)))
let is_correct_arity env c pj ind specif params =
let arsign,_ = get_instantiated_arity ind specif params in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 997a620742..f705cdf646 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -52,7 +52,7 @@ val type_of_inductive : env -> mind_specif puniverses -> types
val type_of_inductive_knowing_parameters :
env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
-val elim_sorts : mind_specif -> Sorts.family list
+val elim_sort : mind_specif -> Sorts.family
val is_private : mind_specif -> bool
val is_primitive_record : mind_specif -> bool
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 09c98ca1bc..b5a929697e 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -91,6 +91,8 @@ let family_compare a b = match a,b with
let family_equal = (==)
+let family_leq a b = family_compare a b <= 0
+
open Hashset.Combine
let hash = function
@@ -101,11 +103,6 @@ let hash = function
let h = Univ.Universe.hash u in
combinesmall 2 h
-module List = struct
- let mem = List.memq
- let intersect l l' = CList.intersect family_equal l l'
-end
-
module Hsorts =
Hashcons.Make(
struct
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index c49728b146..3769e31465 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -37,11 +37,7 @@ val hcons : t -> t
val family_compare : family -> family -> int
val family_equal : family -> family -> bool
-
-module List : sig
- val mem : family -> family list -> bool
- val intersect : family list -> family list -> family list
-end
+val family_leq : family -> family -> bool
val univ_of_sort : t -> Univ.Universe.t
val sort_of_univ : Univ.Universe.t -> t
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index c45fe1cf00..857e4fabf7 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -49,7 +49,7 @@ type ('constr, 'types) ptype_error =
| BadAssumption of ('constr, 'types) punsafe_judgment
| ReferenceVariables of Id.t * 'constr
| ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
- * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option
+ * (Sorts.family * Sorts.family * Sorts.family * arity_error) option
| CaseNotInductive of ('constr, 'types) punsafe_judgment
| WrongCaseInfo of pinductive * case_info
| NumberBranches of ('constr, 'types) punsafe_judgment * int
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 88165a4f07..8e25236851 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -50,7 +50,7 @@ type ('constr, 'types) ptype_error =
| BadAssumption of ('constr, 'types) punsafe_judgment
| ReferenceVariables of Id.t * 'constr
| ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
- * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option
+ * (Sorts.family * Sorts.family * Sorts.family * arity_error) option
| CaseNotInductive of ('constr, 'types) punsafe_judgment
| WrongCaseInfo of pinductive * case_info
| NumberBranches of ('constr, 'types) punsafe_judgment * int
@@ -104,7 +104,7 @@ val error_reference_variables : env -> Id.t -> constr -> 'a
val error_elim_arity :
env -> pinductive -> constr -> unsafe_judgment ->
- (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'a
+ (Sorts.family * Sorts.family * Sorts.family * arity_error) option -> 'a
val error_case_not_inductive : env -> unsafe_judgment -> 'a
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 7615a17514..1c488a6974 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -84,7 +84,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
let () = if Option.is_empty projs then check_privacy_block mib in
let () =
- if not (Sorts.List.mem kind (elim_sorts specif)) then
+ if not (Sorts.family_leq kind (elim_sort specif)) then
raise
(RecursionSchemeError
(env, NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family kind), pind)))
@@ -557,8 +557,8 @@ let weaken_sort_scheme env evd set sort npars term ty =
let check_arities env listdepkind =
let _ = List.fold_left
(fun ln (((_,ni as mind),u),mibi,mipi,dep,kind) ->
- let kelim = elim_sorts (mibi,mipi) in
- if not (Sorts.List.mem kind kelim) then raise
+ let kelim = elim_sort (mibi,mipi) in
+ if not (Sorts.family_leq kind kelim) then raise
(RecursionSchemeError
(env, NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family kind),(mind,u))))
else if Int.List.mem ni ln then raise
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b1c98da2c7..12a7859b88 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -255,10 +255,13 @@ let inductive_has_local_defs env ind =
let l2 = mib.mind_nparams + mip.mind_nrealargs in
not (Int.equal l1 l2)
-let allowed_sorts env (kn,i as ind) =
+let top_allowed_sort env (kn,i as ind) =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
mip.mind_kelim
+let sorts_below top =
+ List.filter (fun s -> Sorts.family_leq s top) Sorts.[InSProp;InProp;InSet;InType]
+
let has_dependent_elim mib =
match mib.mind_record with
| PrimRecord _ -> mib.mind_finite == BiFinite
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index cfc650938e..aacbecf6c7 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -141,7 +141,9 @@ val constructor_nrealdecls_env : env -> constructor -> int
val constructor_has_local_defs : env -> constructor -> bool
val inductive_has_local_defs : env -> inductive -> bool
-val allowed_sorts : env -> inductive -> Sorts.family list
+val sorts_below : Sorts.family -> Sorts.family list
+
+val top_allowed_sort : env -> inductive -> Sorts.family
(** (Co)Inductive records with primitive projections do not have eta-conversion,
hence no dependent elimination. *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index a9e2b0ea8f..25e56602a5 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -107,7 +107,7 @@ val error_ill_typed_rec_body :
val error_elim_arity :
?loc:Loc.t -> env -> Evd.evar_map ->
pinductive -> constr ->
- unsafe_judgment -> (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'b
+ unsafe_judgment -> (Sorts.family * Sorts.family * Sorts.family * arity_error) option -> 'b
val error_not_a_type :
?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index be71f44a5e..00c52e7665 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -117,12 +117,12 @@ let check_branch_types env sigma (ind,u) cj (lfj,explft) =
sigma lfj explft
let max_sort l =
- if Sorts.List.mem InType l then InType else
- if Sorts.List.mem InSet l then InSet else InProp
+ if List.mem_f Sorts.family_equal InType l then InType else
+ if List.mem_f Sorts.family_equal InSet l then InSet else InProp
let is_correct_arity env sigma c pj ind specif params =
let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in
- let allowed_sorts = elim_sorts specif in
+ let allowed_sorts = sorts_below (elim_sort specif) in
let error () = Pretype_errors.error_elim_arity env sigma ind c pj None in
let rec srec env sigma pt ar =
let pt' = whd_all env sigma pt in
@@ -135,7 +135,7 @@ let is_correct_arity env sigma c pj ind specif params =
end
| Sort s, [] ->
let s = ESorts.kind sigma s in
- if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
+ if not (List.mem_f Sorts.family_equal (Sorts.family s) allowed_sorts)
then error ()
else sigma, s
| Evar (ev,_), [] ->
@@ -199,13 +199,13 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj =
(* FIXME: might depend on the level of actual parameters!*)
let check_allowed_sort env sigma ind c p =
let specif = lookup_mind_specif env (fst ind) in
- let sorts = elim_sorts specif in
+ let sorts = elim_sort specif in
let pj = Retyping.get_judgment_of env sigma p in
let _, s = splay_prod env sigma pj.uj_type in
let ksort = match EConstr.kind sigma s with
| Sort s -> Sorts.family (ESorts.kind sigma s)
| _ -> error_elim_arity env sigma ind c pj None in
- if not (List.exists ((==) ksort) sorts) then
+ if not (Sorts.family_leq ksort sorts) then
let s = inductive_sort_family (snd specif) in
error_elim_arity env sigma ind c pj
(Some(sorts,ksort,s,Type_errors.error_elim_explain ksort s))
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 45a4799ea1..51eee2a053 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -735,7 +735,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
let project env sorts posn t1 t2 =
let ty1 = get_type_of env sigma t1 in
let s = get_sort_family_of ~truncation_style:true env sigma ty1 in
- if Sorts.List.mem s sorts
+ if List.mem_f Sorts.family_equal s sorts
then [(List.rev posn,t1,t2)] else []
in
let rec findrec sorts posn t1 t2 =
@@ -746,7 +746,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
when Int.equal (List.length args1) (constructor_nallargs env sp1)
->
let sorts' =
- Sorts.List.intersect sorts (allowed_sorts env (fst sp1))
+ CList.intersect Sorts.family_equal sorts (sorts_below (top_allowed_sort env (fst sp1)))
in
(* both sides are fully applied constructors, so either we descend,
or we can discriminate here. *)
@@ -762,7 +762,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
List.flatten
(List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
0 rargs1 rargs2)
- else if Sorts.List.mem InType sorts' && not no_discr
+ else if List.mem_f Sorts.family_equal InType sorts' && not no_discr
then (* see build_discriminator *)
raise (DiscrFound (List.rev posn,sp1,sp2))
else
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 528829f3a5..5aec5cac2c 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -331,8 +331,8 @@ let build_beq_scheme mode kn =
eff := Safe_typing.concat_private eff' !eff
done;
(Array.init nb_ind (fun i ->
- let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
- if not (Sorts.List.mem InSet kelim) then
+ let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in
+ if not (Sorts.family_leq InSet kelim) then
raise (NonSingletonProp (kn,i));
let fix = match mib.mind_finite with
| CoFinite ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index b2382ce6fc..a1f7835cbe 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -219,6 +219,7 @@ let explain_elim_arity env sigma ind c pj okinds =
let pc = pr_leconstr_env env sigma c in
let msg = match okinds with
| Some(sorts,kp,ki,explanation) ->
+ let sorts = Inductiveops.sorts_below sorts in
let pki = Sorts.pr_sort_family ki in
let pkp = Sorts.pr_sort_family kp in
let explanation = match explanation with
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 6ac259b1fe..de7d2fd49a 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -216,11 +216,11 @@ let declare_one_case_analysis_scheme ind =
else if not (Inductiveops.has_dependent_elim mib) then
case_scheme_kind_from_type
else case_dep_scheme_kind_from_type in
- let kelim = elim_sorts (mib,mip) in
+ let kelim = elim_sort (mib,mip) in
(* in case the inductive has a type elimination, generates only one
induction scheme, the other ones share the same code with the
appropriate type *)
- if Sorts.List.mem InType kelim then
+ if Sorts.family_leq InType kelim then
ignore (define_individual_scheme dep UserAutomaticRequest None ind)
(* Induction/recursion schemes *)
@@ -248,16 +248,17 @@ let declare_one_induction_scheme ind =
let kind = inductive_sort_family mip in
let from_prop = kind == InProp in
let depelim = Inductiveops.has_dependent_elim mib in
- let kelim = elim_sorts (mib,mip) in
+ let kelim = Inductiveops.sorts_below (elim_sort (mib,mip)) in
let kelim = if Global.sprop_allowed () then kelim
else List.filter (fun s -> s <> InSProp) kelim
in
let elims =
List.map_filter (fun (sort,kind) ->
- if Sorts.List.mem sort kelim then Some kind else None)
+ if List.mem_f Sorts.family_equal sort kelim then Some kind else None)
(if from_prop then kinds_from_prop
else if depelim then kinds_from_type
- else nondep_kinds_from_type) in
+ else nondep_kinds_from_type)
+ in
List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
elims
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:35:03 +0000