From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- kernel/indtypes.ml | 181 ++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 131 insertions(+), 50 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index de97268b..85be2146 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* let varj = infer_type env c1 in let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in - let max = Universe.sup max (univ_of_sort varj.utj_type) in + let max = Universe.sup max (Sorts.univ_of_sort varj.utj_type) in aux env1 c2 max | _ when is_constructor_head t -> max | _ -> (* don't fail if not positive, it is tested later *) max @@ -168,7 +171,7 @@ let infer_constructor_packet env_ar_par params lc = let jlc = List.map (infer_type env_ar_par) lc in let jlc = Array.of_list jlc in (* generalize the constructor over the parameters *) - let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in + let lc'' = Array.map (fun j -> Term.it_mkProd_or_LetIn j.utj_val params) jlc in (* compute the max of the sorts of the products of the constructors types *) let levels = List.map (infos_and_sort env_ar_par) lc in let isunit = is_unit levels in @@ -183,7 +186,7 @@ let cumulate_arity_large_levels env sign = match d with | LocalAssum (_,t) -> let tj = infer_type env t in - let u = univ_of_sort tj.utj_type in + let u = Sorts.univ_of_sort tj.utj_type in (Universe.sup u lev, push_rel d env) | LocalDef _ -> lev, push_rel d env) @@ -199,14 +202,67 @@ let is_impredicative env u = let param_ccls paramsctxt = let fold acc = function | (LocalAssum (_, p)) -> - (let c = strip_prod_assum p in - match kind_of_term c with + (let c = Term.strip_prod_assum p in + match kind c with | Sort (Type u) -> Univ.Universe.level u | _ -> None) :: acc | LocalDef _ -> acc in List.fold_left fold [] paramsctxt +(* Check arities and constructors *) +let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : types) numparams is_arity = + let numchecked = ref 0 in + let basic_check ev tp = + if !numchecked < numparams then () else conv_leq ev tp (subst tp); + numchecked := !numchecked + 1 + in + let check_typ typ typ_env = + match typ with + | LocalAssum (_, typ') -> + begin + try + basic_check typ_env typ'; Environ.push_rel typ typ_env + with NotConvertible -> + anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation") + end + | _ -> anomaly (Pp.str "") + in + let typs, codom = dest_prod env arcn in + let last_env = Context.Rel.fold_outside check_typ typs ~init:env in + if not is_arity then basic_check last_env codom else () + +(* Check that the subtyping information inferred for inductive types in the block is correct. *) +(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) +let check_subtyping cumi paramsctxt env_ar inds = + let numparams = Context.Rel.nhyps paramsctxt in + let uctx = CumulativityInfo.univ_context cumi in + let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in + let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) + LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels + in + let dosubst = subst_univs_level_constr lmap in + let instance_other = Instance.of_array new_levels in + let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in + let uctx_other = Univ.UContext.make (instance_other, constraints_other) in + let env = Environ.push_context uctx_other env_ar in + let subtyp_constraints = + CumulativityInfo.leq_constraints cumi + (UContext.instance uctx) instance_other + Constraint.empty + in + let env = Environ.add_constraints subtyp_constraints env in + (* process individual inductive types: *) + Array.iter (fun (id,cn,lc,(sign,arity)) -> + match arity with + | RegularArity (_, full_arity, _) -> + check_subtyping_arity_constructor env dosubst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc + | TemplateArity _ -> + anomaly ~label:"check_subtyping" + Pp.(str "template polymorphism and cumulative polymorphism are not compatible") + ) inds + (* Type-check an inductive definition. Does not check positivity conditions. *) (* TODO check that we don't overgeneralize construcors/inductive arities with @@ -214,13 +270,18 @@ let param_ccls paramsctxt = *) let typecheck_inductive env mie = let () = match mie.mind_entry_inds with - | [] -> anomaly (Pp.str "empty inductive types declaration") + | [] -> anomaly (Pp.str "empty inductive types declaration.") | _ -> () in (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let env' = push_context mie.mind_entry_universes env in + let env' = + match mie.mind_entry_universes with + | Monomorphic_ind_entry ctx -> push_context_set ctx env + | Polymorphic_ind_entry ctx -> push_context ctx env + | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env + in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) @@ -238,7 +299,7 @@ let typecheck_inductive env mie = (** We have an algebraic universe as the conclusion of the arity, typecheck the dummy Π ctx, Prop and do a special case for the conclusion. *) - let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in + let proparity = infer_type env_params (mkArity (ctx, Sorts.prop)) in let (cctx, _) = destArity proparity.utj_val in (* Any universe is well-formed, we don't need to check [s] here *) mkArity (cctx, s) @@ -300,7 +361,7 @@ let typecheck_inductive env mie = | None -> clev in let full_polymorphic () = - let defu = Term.univ_of_sort def_level in + let defu = Sorts.univ_of_sort def_level in let is_natural = type_in_type env || (UGraph.check_leq (universes env') infu defu) in @@ -313,7 +374,7 @@ let typecheck_inductive env mie = anomaly ~label:"check_inductive" (Pp.str"Incorrect universe " ++ Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr infu) + ++ Universe.pr infu ++ Pp.str ".") in RegularArity (not is_natural,full_arity,defu) in @@ -333,18 +394,27 @@ let typecheck_inductive env mie = anomaly ~label:"check_inductive" (Pp.str"Incorrect universe " ++ Universe.pr u ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr clev) + ++ Universe.pr clev ++ Pp.str ".") else TemplateArity (param_ccls paramsctxt, infu) | _ (* Not an explicit occurrence of Type *) -> full_polymorphic () in - let arity = - if mie.mind_entry_polymorphic then full_polymorphic () - else template_polymorphic () + let arity = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ -> template_polymorphic () + | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> full_polymorphic () in (id,cn,lc,(sign,arity))) inds + in + (* Check that the subtyping information inferred for inductive types in the block is correct. *) + (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) + let () = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ -> () + | Polymorphic_ind_entry _ -> () + | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) @@ -389,11 +459,11 @@ let failwith_non_pos n ntypes c = let failwith_non_pos_vect n ntypes v = Array.iter (failwith_non_pos n ntypes) v; - anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur.") let failwith_non_pos_list n ntypes l = List.iter (failwith_non_pos n ntypes) l; - anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.") (* Check the inductive type is called with the expected parameters *) (* [n] is the index of the last inductive type in [env] *) @@ -409,7 +479,7 @@ let check_correct_par (env,n,ntypes,_) paramdecls ind_index args = | LocalDef _ :: paramdecls -> check param_index (paramdecl_index+1) paramdecls | _::paramdecls -> - match kind_of_term (whd_all env params.(param_index)) with + match kind (whd_all env params.(param_index)) with | Rel w when Int.equal w paramdecl_index -> check (param_index-1) (paramdecl_index+1) paramdecls | _ -> @@ -436,7 +506,7 @@ if Int.equal nmr 0 then 0 else | (_,[]) -> assert false (* |paramsctxt|>=nmr *) | (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt) | (p::lp,_::paramsctxt) -> - ( match kind_of_term (whd_all env p) with + ( match kind (whd_all env p) with | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt) | _ -> k) in find 0 (n-1) (lpar,List.rev paramsctxt) @@ -467,7 +537,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else let c' = whd_all env c in - match kind_of_term c' with + match kind c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in ienv_decompose_prod ienv' (n-1) b @@ -496,7 +566,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( more generally, the arrows may be dependent). *) let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = let x,largs = decompose_app (whd_all env c) in - match kind_of_term x with + match kind x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in (** If one of the inductives of the mutually inductive @@ -604,7 +674,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( and check_constructors ienv check_head nmr c = let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = let x,largs = decompose_app (whd_all env c) in - match kind_of_term x with + match kind x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in @@ -651,7 +721,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( best-effort fashion. *) let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds = let ntypes = Array.length inds in - let recursive = finite != Decl_kinds.BiFinite in + let recursive = finite != BiFinite in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in let ra_env_ar = Array.rev_to_list rc in let nparamsctxt = Context.Rel.length paramsctxt in @@ -687,7 +757,7 @@ let allowed_sorts is_smashed s = as well. *) all_sorts else - match family_of_sort s with + match Sorts.family s with (* Type: all elimination allowed: above and below *) | InType -> all_sorts (* Smashed Set is necessarily impredicative: forbids large elimination *) @@ -728,13 +798,13 @@ exception UndefinableExpansion a substitution of the form [params, x : ind params] *) let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params mind_consnrealdecls mind_consnrealargs paramslet ctx = - let mp, dp, l = repr_mind kn in + let mp, dp, l = MutInd.repr3 kn in (** We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not matching with a parameter context. *) let indty, paramsletsubst = (* [ty] = [Ind inst] is typed in context [params] *) - let inst = Context.Rel.to_extended_vect 0 paramslet in + let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in let ty = mkApp (mkIndU indu, inst) in (* [Ind inst] is typed in context [params-wo-let] *) let inst' = rel_list 0 nparamargs in @@ -816,23 +886,35 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs = +let abstract_inductive_universes iu = + match iu with + | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) + | Polymorphic_ind_entry ctx -> + let (inst, auctx) = Univ.abstract_universes ctx in + let inst = Univ.make_instance_subst inst in + (inst, Polymorphic_ind auctx) + | Cumulative_ind_entry cumi -> + let (inst, acumi) = Univ.abstract_cumulativity_info cumi in + let inst = Univ.make_instance_subst inst in + (inst, Cumulative_ind acumi) + +let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in let nparamargs = Context.Rel.nhyps paramsctxt in let nparamsctxt = Context.Rel.length paramsctxt in - let subst, ctx = Univ.abstract_universes p ctx in - let paramsctxt = Vars.subst_univs_level_context subst paramsctxt in - let env_ar = - let ctx = Environ.rel_context env_ar in - let ctx' = Vars.subst_univs_level_context subst ctx in - Environ.push_rel_context ctx' env + let substunivs, aiu = abstract_inductive_universes iu in + let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in + let env_ar = + let ctxunivs = Environ.rel_context env_ar in + let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in + Environ.push_rel_context ctxunivs' env in (* Check one inductive *) let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg = (* Type of constructors in normal form *) - let lc = Array.map (Vars.subst_univs_level_constr subst) lc in + let lc = Array.map (Vars.subst_univs_level_constr substunivs) lc in let splayed_lc = Array.map (dest_prod_assum env_ar) lc in let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in let consnrealdecls = @@ -848,11 +930,11 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let ar = {template_param_levels = paramlevs; template_level = lev} in TemplateArity ar, all_sorts | RegularArity (info,ar,defs) -> - let s = sort_of_univ defs in + let s = Sorts.sort_of_univ defs in let kelim = allowed_sorts info s in let ar = RegularArity - { mind_user_arity = Vars.subst_univs_level_constr subst ar; - mind_sort = sort_of_univ (Univ.subst_univs_level_universe subst defs); } in + { mind_user_arity = Vars.subst_univs_level_constr substunivs ar; + mind_sort = Sorts.sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in ar, kelim in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in @@ -871,7 +953,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm (* Build the inductive packet *) { mind_typename = id; mind_arity = arkind; - mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign; + mind_arity_ctxt = Vars.subst_univs_level_context substunivs ar_sign; mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs; mind_nrealdecls = Context.Rel.length ar_sign - nparamsctxt; mind_kelim = kelim; @@ -893,10 +975,11 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm && Array.length pkt.mind_consnames == 1 && pkt.mind_consnrealargs.(0) > 0 -> (** The elimination criterion ensures that all projections can be defined. *) - let u = - if p then - subst_univs_level_instance subst (Univ.UContext.instance ctx) - else Univ.Instance.empty + let u = + match aiu with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx + | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi) in let indsp = ((kn, 0), u) in let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in @@ -919,8 +1002,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_nparams_rec = nmr; mind_params_ctxt = paramsctxt; mind_packets = packets; - mind_polymorphic = p; - mind_universes = ctx; + mind_universes = aiu; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } @@ -935,7 +1017,6 @@ let check_inductive env kn mie = let chkpos = (Environ.typing_flags env).check_guarded in let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in (* Build the inductive packets *) - build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private - mie.mind_entry_universes + build_inductive env mie.mind_entry_private mie.mind_entry_universes env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite inds nmr recargs -- cgit v1.2.3