diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declarations.ml | 2 | ||||
| -rw-r--r-- | kernel/indTyping.ml | 13 | ||||
| -rw-r--r-- | kernel/indTyping.mli | 4 | ||||
| -rw-r--r-- | kernel/inductive.ml | 8 | ||||
| -rw-r--r-- | kernel/inductive.mli | 2 | ||||
| -rw-r--r-- | kernel/sorts.ml | 7 | ||||
| -rw-r--r-- | kernel/sorts.mli | 6 | ||||
| -rw-r--r-- | kernel/type_errors.ml | 2 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 4 |
9 files changed, 16 insertions, 32 deletions
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 |