diff options
| -rw-r--r-- | kernel/indtypes.ml | 35 | ||||
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.mli | 2 | ||||
| -rw-r--r-- | kernel/typeops.ml | 20 | ||||
| -rw-r--r-- | kernel/typeops.mli | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 12 | ||||
| -rw-r--r-- | pretyping/retyping.mli | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 4 |
10 files changed, 51 insertions, 32 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b5de04221..41ca4e661 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -164,8 +164,8 @@ let small_unit constrsinfos = *) let inductive_levels arities inds = - let levels = Array.map (function _,_,Type u -> Some u | _ -> None) arities in - let cstrs_levels = Array.map (fun (_,_,_,_,_,lev) -> lev) inds in + let levels = Array.map pi3 arities in + let cstrs_levels = Array.map (fun (_,_,_,_,lev) -> lev) inds in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) solve_constraints_system levels cstrs_levels @@ -217,7 +217,12 @@ let typecheck_inductive env mie = let cst = Constraint.union cst cst2 in let id = ind.mind_entry_typename in let env_ar' = push_rel (Name id, None, full_arity) env_ar in - let lev = snd (dest_arity env_params arity.utj_val) in + let lev = + (* Decide that if the conclusion is not explicitly Type *) + (* then the inductive type is not polymorphic *) + match kind_of_term (snd (decompose_prod_assum arity.utj_val)) with + | Sort (Type u) -> Some u + | _ -> None in (cst,env_ar',(id,full_arity,lev)::l)) (cst1,env,[]) mie.mind_entry_inds in @@ -227,11 +232,11 @@ let typecheck_inductive env mie = (* Now, we type the constructors (without params) *) let inds,cst = List.fold_right2 - (fun ind (id,full_arity,_) (inds,cst) -> + (fun ind arity_data (inds,cst) -> let (info,lc',cstrs_univ,cst') = infer_constructor_packet env_arities params ind.mind_entry_lc in let consnames = ind.mind_entry_consnames in - let ind' = (id,full_arity,consnames,info,lc',cstrs_univ) in + let ind' = (arity_data,consnames,info,lc',cstrs_univ) in (ind'::inds, Constraint.union cst cst')) mie.mind_entry_inds arity_list @@ -249,23 +254,25 @@ let typecheck_inductive env mie = (* Compute/check the sorts of the inductive types *) let ind_min_levels = inductive_levels arities inds in - let inds = - array_map2 (fun (id,full_arity,cn,info,lc,_) lev -> + let inds, cst = + array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst -> let sign, s = dest_arity env full_arity in - let status = match s with - | Type _ -> + let status,cst = match s with + | Type _ when ar_level <> None (* Explicitly polymorphic *) -> (* The polymorphic level is a function of the level of the *) (* conclusions of the parameters *) - Inr (param_ccls, lev) + Inr (param_ccls, lev), cst + | Type u (* Not an explicit occurrence of Type *) -> + Inl (info,full_arity,s), enforce_geq u lev cst | Prop Pos when engagement env <> Some ImpredicativeSet -> (* Predicative set: check that the content is indeed predicative *) if not (is_empty_univ lev) & not (is_base_univ lev) then error "Large non-propositional inductive types must be in Type"; - Inl (info,full_arity,s) + Inl (info,full_arity,s), cst | Prop _ -> - Inl (info,full_arity,s) in - (id,cn,lc,(sign,status))) - inds ind_min_levels in + Inl (info,full_arity,s), cst in + (id,cn,lc,(sign,status)),cst) + inds ind_min_levels cst in (env_arities, params, inds, cst) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index efae466f8..52f2ea3db 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -164,7 +164,7 @@ let instantiate_inductive_with_param_levels env ar mip paramtyps = let subst = make_subst env ar.mind_param_levels args in sort_of_instantiated_universe mip subst ar.mind_level -let type_of_applied_inductive env mip paramtyps = +let type_of_inductive_knowing_parameters env mip paramtyps = match mip.mind_arity with | Monomorphic s -> s.mind_user_arity diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c0a138bde..0f05ffc6b 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -75,7 +75,7 @@ val check_cofix : env -> cofixpoint -> unit (*s Support for sort-polymorphic inductive types *) -val type_of_applied_inductive : +val type_of_inductive_knowing_parameters : env -> one_inductive_body -> types array -> types val set_inductive_level : env -> sorts -> types -> types diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 435b3e31c..4b5a6e01a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -245,16 +245,28 @@ let judge_of_cast env cj k tj = (* Inductive types. *) -let judge_of_applied_inductive env ind jl = +(* The type is parametric over the uniform parameters whose conclusion + is in Type; to enforce the internal constraints between the + parameters and the instances of Type occurring in the type of the + constructors, we use the level variables _statically_ assigned to + the conclusions of the parameters as mediators: e.g. if a parameter + has conclusion Type(alpha), static constraints of the form alpha<=v + exist between alpha and the Type's occurring in the constructor + types; when the parameters is finally instantiated by a term of + conclusion Type(u), then the constraints u<=alpha is computed in + the App case of execute; from this constraints, the expected + dynamic constraints of the form u<=v are enforced *) + +let judge_of_inductive_knowing_parameters env ind jl = let c = mkInd ind in let (mib,mip) = lookup_mind_specif env ind in check_args env c mib.mind_hyps; let paramstyp = Array.map (fun j -> j.uj_type) jl in - let t = Inductive.type_of_applied_inductive env mip paramstyp in + let t = Inductive.type_of_inductive_knowing_parameters env mip paramstyp in make_judge c t let judge_of_inductive env ind = - judge_of_applied_inductive env ind [||] + judge_of_inductive_knowing_parameters env ind [||] (* Constructors. *) @@ -340,7 +352,7 @@ let rec execute env cstr cu = let (j,cu2) = if isInd f then (* Sort-polymorphism of inductive types *) - judge_of_applied_inductive env (destInd f) jl, cu1 + judge_of_inductive_knowing_parameters env (destInd f) jl, cu1 else execute env f cu1 in diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 25f7d15db..6e20cd42d 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -78,7 +78,7 @@ val judge_of_cast : val judge_of_inductive : env -> inductive -> unsafe_judgment -val judge_of_applied_inductive : +val judge_of_inductive_knowing_parameters : env -> inductive -> unsafe_judgment array -> unsafe_judgment val judge_of_constructor : env -> constructor -> unsafe_judgment diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 01841641c..d1d30980b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -415,7 +415,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct match kind_of_term resj.uj_val with | App (f,args) when isInd f -> let sigma = evars_of !isevars in - let t = Retyping.type_of_applied_inductive env sigma (destInd f) args in + let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in let s = snd (splay_arity env sigma t) in on_judgment_type (set_inductive_level env s) resj (* Rem: no need to send sigma: no head evar, it's an arity *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 2fdb4148a..1756c8377 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -74,7 +74,7 @@ let typeur sigma metamap = | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) | App(f,args) when isInd f -> - let t = type_of_applied_inductive env (destInd f) args in + let t = type_of_inductive_knowing_parameters env (destInd f) args in strip_outer_cast (subst_type env sigma t (Array.to_list args)) | App(f,args) -> strip_outer_cast @@ -98,7 +98,7 @@ let typeur sigma metamap = | Prop Null, (Type _ as s) -> s | Type u1, Type u2 -> Type (Univ.sup u1 u2)) | App(f,args) when isInd f -> - let t = type_of_applied_inductive env (destInd f) args in + let t = type_of_inductive_knowing_parameters env (destInd f) args in sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | Lambda _ | Fix _ | Construct _ -> @@ -117,17 +117,17 @@ let typeur sigma metamap = anomaly "sort_of: Not a type (1)" | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) - and type_of_applied_inductive env ind args = + and type_of_inductive_knowing_parameters env ind args = let (_,mip) = lookup_mind_specif env ind in let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in - Inductive.type_of_applied_inductive env mip argtyps + Inductive.type_of_inductive_knowing_parameters env mip argtyps - in type_of, sort_of, sort_family_of, type_of_applied_inductive + in type_of, sort_of, sort_family_of, type_of_inductive_knowing_parameters let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c -let type_of_applied_inductive env sigma ind args = +let type_of_inductive_knowing_parameters env sigma ind args = let _,_,_,f = typeur sigma [] in f env ind args let get_type_of_with_meta env sigma metamap = diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 8631f5545..900a96829 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -34,5 +34,5 @@ val get_assumption_of : env -> evar_map -> constr -> types (* Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment -val type_of_applied_inductive : env -> evar_map -> inductive -> +val type_of_inductive_knowing_parameters : env -> evar_map -> inductive -> constr array -> types diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 8e10b0aff..57c83fa7e 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -92,7 +92,7 @@ let rec execute env evd cstr = let j = if isInd f then (* Sort-polymorphism of inductive types *) - judge_of_applied_inductive env (destInd f) + judge_of_inductive_knowing_parameters env (destInd f) (jv_nf_evar (evars_of evd) jl) else execute env evd f diff --git a/proofs/logic.ml b/proofs/logic.ml index bbc1e202c..209c3bb65 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -285,7 +285,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty) = if isInd f & not (array_exists occur_meta l) (* we could be finer *) - then (goalacc,type_of_applied_inductive env sigma (destInd f) l) + then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l) else mk_hdgoals sigma goal goalacc f in let (acc'',conclty') = @@ -327,7 +327,7 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty) = if isInd f & not (array_exists occur_meta l) (* we could be finer *) - then (goalacc,type_of_applied_inductive env sigma (destInd f) l) + then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l) else mk_hdgoals sigma goal goalacc f in mk_arggoals sigma goal acc' hdty (Array.to_list l) |