From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- kernel/indtypes.ml | 548 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 548 insertions(+) create mode 100644 kernel/indtypes.ml (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml new file mode 100644 index 00000000..88f837aa --- /dev/null +++ b/kernel/indtypes.ml @@ -0,0 +1,548 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* idset + | c::cl -> + if Idset.mem c idset then + raise (InductiveError (SameNamesConstructors (id,c))) + else + check (Idset.add c idset) cl + in + check + +(* [mind_check_names mie] checks the names of an inductive types declaration, + and raises the corresponding exceptions when two types or two constructors + have the same name. *) + +let mind_check_names mie = + let rec check indset cstset = function + | [] -> () + | ind::inds -> + let id = ind.mind_entry_typename in + let cl = ind.mind_entry_consnames in + if Idset.mem id indset then + raise (InductiveError (SameNamesTypes id)) + else + let cstset' = check_constructors_names id cstset cl in + check (Idset.add id indset) cstset' inds + in + check Idset.empty Idset.empty mie.mind_entry_inds +(* The above verification is not necessary from the kernel point of + vue since inductive and constructors are not referred to by their + name, but only by the name of the inductive packet and an index. *) + +let mind_check_arities env mie = + let check_arity id c = + if not (is_arity env c) then + raise (InductiveError (NotAnArity id)) + in + List.iter + (fun {mind_entry_typename=id; mind_entry_arity=ar} -> check_arity id ar) + mie.mind_entry_inds + +(************************************************************************) +(************************************************************************) + +(* Typing the arities and constructor types *) + +let is_info_arity env c = + match dest_arity env c with + | (_,Prop Null) -> false + | (_,Prop Pos) -> true + | (_,Type _) -> true + +let is_info_type env t = + let s = t.utj_type in + if s = mk_Set then true + else if s = mk_Prop then false + else + try is_info_arity env t.utj_val + with UserError _ -> true + +(* [infos] is a sequence of pair [islogic,issmall] for each type in + the product of a constructor or arity *) + +let is_small infos = List.for_all (fun (logic,small) -> small) infos +let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos +let is_logic_arity infos = + List.for_all (fun (logic,small) -> logic || small) infos + +(* An inductive definition is a "unit" if it has only one constructor + and that all arguments expected by this constructor are + logical, this is the case for equality, conjonction of logical properties +*) +let is_unit constrsinfos = + match constrsinfos with (* One info = One constructor *) + | [constrinfos] -> is_logic_constr constrinfos + | [] -> (* type without constructors *) true + | _ -> false + +let rec infos_and_sort env t = + match kind_of_term t with + | Prod (name,c1,c2) -> + let (varj,_) = infer_type env c1 in + let env1 = Environ.push_rel (name,None,varj.utj_val) env in + let logic = not (is_info_type env varj) in + let small = Term.is_small varj.utj_type in + (logic,small) :: (infos_and_sort env1 c2) + | Cast (c,_) -> infos_and_sort env c + | _ -> [] + +let small_unit constrsinfos = + let issmall = List.for_all is_small constrsinfos + and isunit = is_unit constrsinfos in + issmall, isunit + +(* This (re)computes informations relevant to extraction and the sort of an + arity or type constructor; we do not to recompute universes constraints *) + +(* [smax] is the max of the sorts of the products of the constructor type *) + +let enforce_type_constructor env arsort smax cst = + match smax, arsort with + | Type uc, Type ua -> enforce_geq ua uc cst + | Type uc, Prop Pos when engagement env <> Some ImpredicativeSet -> + error "Large non-propositional inductive types must be in Type" + | _,_ -> cst + +let type_one_constructor env_ar_par params arsort c = + let infos = infos_and_sort env_ar_par c in + + (* Each constructor is typed-checked here *) + let (j,cst) = infer_type env_ar_par c in + let full_cstr_type = it_mkProd_or_LetIn j.utj_val params in + + (* If the arity is at some level Type arsort, then the sort of the + constructor must be below arsort; here we consider constructors with the + global parameters (which add a priori more constraints on their sort) *) + let cst2 = enforce_type_constructor env_ar_par arsort j.utj_type cst in + + (infos, full_cstr_type, cst2) + +let infer_constructor_packet env_ar params arsort vc = + let env_ar_par = push_rel_context params env_ar in + let (constrsinfos,jlc,cst) = + List.fold_right + (fun c (infosl,l,cst) -> + let (infos,ct,cst') = + type_one_constructor env_ar_par params arsort c in + (infos::infosl,ct::l, Constraint.union cst cst')) + vc + ([],[],Constraint.empty) in + let vc' = Array.of_list jlc in + let issmall,isunit = small_unit constrsinfos in + (issmall,isunit,vc', cst) + +(* Type-check an inductive definition. Does not check positivity + conditions. *) +let typecheck_inductive env mie = + if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration"; + (* Check unicity of names *) + mind_check_names mie; + mind_check_arities env mie; + (* We first type params and arity of each inductive definition *) + (* This allows to build the environment of arities and to share *) + (* the set of constraints *) + let cst, arities, rev_params_arity_list = + List.fold_left + (fun (cst,arities,l) ind -> + (* Params are typed-checked here *) + let params = ind.mind_entry_params in + let env_params, params, cst1 = + infer_local_decls env params in + (* Arities (without params) are typed-checked here *) + let arity, cst2 = + infer_type env_params ind.mind_entry_arity in + (* We do not need to generate the universe of full_arity; if + later, after the validation of the inductive definition, + full_arity is used as argument or subject to cast, an + upper universe will be generated *) + let id = ind.mind_entry_typename in + let full_arity = it_mkProd_or_LetIn arity.utj_val params in + Constraint.union cst (Constraint.union cst1 cst2), + Sign.add_rel_decl (Name id, None, full_arity) arities, + (params, id, full_arity, arity.utj_val)::l) + (Constraint.empty,empty_rel_context,[]) + mie.mind_entry_inds in + + let env_arities = push_rel_context arities env in + + let params_arity_list = List.rev rev_params_arity_list in + + (* Now, we type the constructors (without params) *) + let inds,cst = + List.fold_right2 + (fun ind (params,id,full_arity,short_arity) (inds,cst) -> + let (_,arsort) = dest_arity env full_arity in + let lc = ind.mind_entry_lc in + let (issmall,isunit,lc',cst') = + infer_constructor_packet env_arities params arsort lc in + let consnames = ind.mind_entry_consnames in + let ind' = (params,id,full_arity,consnames,issmall,isunit,lc') + in + (ind'::inds, Constraint.union cst cst')) + mie.mind_entry_inds + params_arity_list + ([],cst) in + (env_arities, Array.of_list inds, cst) + +(************************************************************************) +(************************************************************************) +(* Positivity *) + +type ill_formed_ind = + | LocalNonPos of int + | LocalNotEnoughArgs of int + | LocalNotConstructor + | LocalNonPar of int * int + +exception IllFormedInd of ill_formed_ind + +(* [mind_extract_params mie] extracts the params from an inductive types + declaration, and checks that they are all present (and all the same) + for all the given types. *) + +let mind_extract_params = decompose_prod_n_assum + +let explain_ind_err ntyp env0 nbpar c err = + let (lpar,c') = mind_extract_params nbpar c in + let env = push_rel_context lpar env0 in + match err with + | LocalNonPos kt -> + raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar)))) + | LocalNotEnoughArgs kt -> + raise (InductiveError + (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) + | LocalNotConstructor -> + raise (InductiveError + (NotConstructor (env,c',mkRel (ntyp+nbpar)))) + | LocalNonPar (n,l) -> + raise (InductiveError + (NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar)))) + +let failwith_non_pos_vect n ntypes v = + for i = 0 to Array.length v - 1 do + for k = n to n + ntypes - 1 do + if not (noccurn k v.(i)) then raise (IllFormedInd (LocalNonPos (k-n+1))) + done + done; + anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur in v" + +(* Check the inductive type is called with the expected parameters *) +let check_correct_par (env,n,ntypes,_) hyps l largs = + let nparams = rel_context_nhyps hyps in + let largs = Array.of_list largs in + if Array.length largs < nparams then + raise (IllFormedInd (LocalNotEnoughArgs l)); + let (lpar,largs') = array_chop nparams largs in + let nhyps = List.length hyps in + let rec check k index = function + | [] -> () + | (_,Some _,_)::hyps -> check k (index+1) hyps + | _::hyps -> + match kind_of_term (whd_betadeltaiota env lpar.(k)) with + | Rel w when w = index -> check (k-1) (index+1) hyps + | _ -> raise (IllFormedInd (LocalNonPar (k+1,l))) + in check (nparams-1) (n-nhyps) hyps; + if not (array_for_all (noccur_between n ntypes) largs') then + failwith_non_pos_vect n ntypes largs' + +(* This removes global parameters of the inductive types in lc (for + nested inductive types only ) *) +let abstract_mind_lc env ntyps npars lc = + if npars = 0 then + lc + else + let make_abs = + list_tabulate + (function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps + in + Array.map (substl make_abs) lc + +(* [env] is the typing environment + [n] is the dB of the last inductive type + [ntypes] is the number of inductive types in the definition + (i.e. range of inductives is [n; n+ntypes-1]) + [lra] is the list of recursive tree of each variable + *) +let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = + (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) + +let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = + let auxntyp = 1 in + let env' = + push_rel (Anonymous,None, + hnf_prod_applist env (type_of_inductive env mi) lpar) env in + let ra_env' = + (Imbr mi,Rtree.mk_param 0) :: + List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in + (* New index of the inductive types *) + let newidx = n + auxntyp in + (env', newidx, ntypes, ra_env') + +(* The recursive function that checks positivity and builds the list + of recursive arguments *) +let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc = + let nparams = rel_context_length hyps in + (* check the inductive types occur positively in [c] *) + let rec check_pos (env, n, ntypes, ra_env as ienv) c = + let x,largs = decompose_app (whd_betadeltaiota env c) in + match kind_of_term x with + | Prod (na,b,d) -> + assert (largs = []); + if not (noccur_between n ntypes b) then + raise (IllFormedInd (LocalNonPos n)); + check_pos (ienv_push_var ienv (na, b, mk_norec)) d + | Rel k -> + let (ra,rarg) = + try List.nth ra_env (k-1) + with Failure _ | Invalid_argument _ -> (Norec,mk_norec) in + (match ra with + Mrec _ -> check_correct_par ienv hyps (k-n+1) largs + | _ -> + if not (List.for_all (noccur_between n ntypes) largs) + then raise (IllFormedInd (LocalNonPos n))); + rarg + | Ind ind_kn -> + (* If the inductive type being defined appears in a + parameter, then we have an imbricated type *) + if List.for_all (noccur_between n ntypes) largs then mk_norec + else check_positive_imbr ienv (ind_kn, largs) + | err -> + if noccur_between n ntypes x && + List.for_all (noccur_between n ntypes) largs + then mk_norec + else raise (IllFormedInd (LocalNonPos n)) + + (* accesses to the environment are not factorised, but does it worth + it? *) + and check_positive_imbr (env,n,ntypes,ra_env as ienv) (mi, largs) = + let (mib,mip) = lookup_mind_specif env mi in + let auxnpar = mip.mind_nparams in + let (lpar,auxlargs) = + try list_chop auxnpar largs + with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in + (* If the inductive appears in the args (non params) then the + definition is not positive. *) + if not (List.for_all (noccur_between n ntypes) auxlargs) then + raise (IllFormedInd (LocalNonPos n)); + (* We do not deal with imbricated mutual inductive types *) + let auxntyp = mib.mind_ntypes in + if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n)); + (* The nested inductive type with parameters removed *) + let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in + (* Extends the environment with a variable corresponding to + the inductive def *) + let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in + (* Parameters expressed in env' *) + let lpar' = List.map (lift auxntyp) lpar in + let irecargs = + (* fails if the inductive type occurs non positively *) + (* when substituted *) + Array.map + (function c -> + let c' = hnf_prod_applist env' c lpar' in + check_constructors ienv' false c') + auxlcvect + in + (Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0) + + (* check the inductive types occur positively in the products of C, if + check_head=true, also check the head corresponds to a constructor of + the ith type *) + + and check_constructors ienv check_head c = + let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c = + let x,largs = decompose_app (whd_betadeltaiota env c) in + match kind_of_term x with + + | Prod (na,b,d) -> + assert (largs = []); + let recarg = check_pos ienv b in + let ienv' = ienv_push_var ienv (na,b,mk_norec) in + check_constr_rec ienv' (recarg::lrec) d + + | hd -> + if check_head then + if hd = Rel (n+ntypes-i-1) then + check_correct_par ienv hyps (ntypes-i) largs + else + raise (IllFormedInd LocalNotConstructor) + else + if not (List.for_all (noccur_between n ntypes) largs) + then raise (IllFormedInd (LocalNonPos n)); + List.rev lrec + in check_constr_rec ienv [] c + in + mk_paths (Mrec i) + (Array.map + (fun c -> + let c = body_of_type c in + let sign, rawc = mind_extract_params nparams c in + let env' = push_rel_context sign env in + try + check_constructors ienv true rawc + with IllFormedInd err -> + explain_ind_err (ntypes-i) env nparams c err) + indlc) + +let check_positivity env_ar inds = + let ntypes = Array.length inds in + let lra_ind = + List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in + let check_one i (params,_,_,_,_,_,lc) = + let nparams = rel_context_length params in + let ra_env = + list_tabulate (fun _ -> (Norec,mk_norec)) nparams @ lra_ind in + let ienv = (env_ar, 1+nparams, ntypes, ra_env) in + check_positivity_one ienv params i lc in + Rtree.mk_rec (Array.mapi check_one inds) + + +(************************************************************************) +(************************************************************************) +(* Build the inductive packet *) + +(* Elimination sorts *) +let is_recursive = Rtree.is_infinite +(* let rec one_is_rec rvec = + List.exists (function Mrec(i) -> List.mem i listind + | Imbr(_,lvec) -> array_exists one_is_rec lvec + | Norec -> false) rvec + in + array_exists one_is_rec +*) + +let all_sorts = [InProp;InSet;InType] +let impredicative_sorts = [InProp;InSet] +let logical_sorts = [InProp] + +let allowed_sorts env issmall isunit = function + | Type _ -> all_sorts + | Prop Pos -> + if issmall then all_sorts + else impredicative_sorts + | Prop Null -> +(* Added InType which is derivable :when the type is unit and small *) +(* unit+small types have all elimination + In predicative system, the + other inductive definitions have only Prop elimination. + In impredicative system, large unit type have also Set elimination +*) if isunit then + if issmall then all_sorts + else if Environ.engagement env = None + then logical_sorts else impredicative_sorts + else logical_sorts + +let build_inductive env env_ar finite inds recargs cst = + let ntypes = Array.length inds in + (* Compute the set of used section variables *) + let ids = + Array.fold_left + (fun acc (_,_,ar,_,_,_,lc) -> + Idset.union (Environ.global_vars_set env (body_of_type ar)) + (Array.fold_left + (fun acc c -> + Idset.union (global_vars_set env (body_of_type c)) acc) + acc + lc)) + Idset.empty inds in + let hyps = keep_hyps env ids in + (* Check one inductive *) + let build_one_packet (params,id,ar,cnames,issmall,isunit,lc) recarg = + (* Arity in normal form *) + let nparamargs = rel_context_nhyps params in + let (ar_sign,ar_sort) = dest_arity env ar in + let nf_ar = + if isArity (body_of_type ar) then ar + else it_mkProd_or_LetIn (mkSort ar_sort) ar_sign in + (* Type of constructors in normal form *) + let splayed_lc = Array.map (dest_prod_assum env_ar) lc in + let nf_lc = + array_map2 (fun (d,b) c -> it_mkProd_or_LetIn b d) splayed_lc lc in + let nf_lc = if nf_lc = lc then lc else nf_lc in + (* Elimination sorts *) + let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in + let kelim = allowed_sorts env issmall isunit ar_sort in + (* Build the inductive packet *) + { mind_typename = id; + mind_nparams = nparamargs; + mind_params_ctxt = params; + mind_user_arity = ar; + mind_nf_arity = nf_ar; + mind_nrealargs = rel_context_nhyps ar_sign - nparamargs; + mind_sort = ar_sort; + mind_kelim = kelim; + mind_consnames = Array.of_list cnames; + mind_user_lc = lc; + mind_nf_lc = nf_lc; + mind_recargs = recarg; + } in + let packets = array_map2 build_one_packet inds recargs in + (* Build the mutual inductive *) + { mind_ntypes = ntypes; + mind_finite = finite; + mind_hyps = hyps; + mind_packets = packets; + mind_constraints = cst; + mind_equiv = None; + } + +(************************************************************************) +(************************************************************************) + +let check_inductive env mie = + (* First type-check the inductive definition *) + let (env_arities, inds, cst) = typecheck_inductive env mie in + (* Then check positivity conditions *) + let recargs = check_positivity env_arities inds in + (* Build the inductive packets *) + build_inductive env env_arities mie.mind_entry_finite inds recargs cst + -- cgit v1.2.3