summaryrefslogtreecommitdiff
path: root/kernel/indtypes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/indtypes.ml')
-rw-r--r--kernel/indtypes.ml548
1 files changed, 548 insertions, 0 deletions
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 *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: indtypes.ml,v 1.59.2.1 2004/07/16 19:30:25 herbelin Exp $ *)
+
+open Util
+open Names
+open Univ
+open Term
+open Declarations
+open Inductive
+open Sign
+open Environ
+open Reduction
+open Typeops
+open Entries
+
+(* [check_constructors_names id s cl] checks that all the constructors names
+ appearing in [l] are not present in the set [s], and returns the new set
+ of names. The name [id] is the name of the current inductive type, used
+ when reporting the error. *)
+
+(************************************************************************)
+(* Various well-formedness check for inductive declarations *)
+
+type inductive_error =
+ (* These are errors related to inductive constructions in this module *)
+ | NonPos of env * constr * constr
+ | NotEnoughArgs of env * constr * constr
+ | NotConstructor of env * constr * constr
+ | NonPar of env * constr * int * constr * constr
+ | SameNamesTypes of identifier
+ | SameNamesConstructors of identifier * identifier
+ | SameNamesOverlap of identifier list
+ | NotAnArity of identifier
+ | BadEntry
+ (* These are errors related to recursors building in Indrec *)
+ | NotAllowedCaseAnalysis of bool * sorts * inductive
+ | BadInduction of bool * identifier * sorts
+ | NotMutualInScheme
+
+exception InductiveError of inductive_error
+
+let check_constructors_names id =
+ let rec check idset = function
+ | [] -> 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
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 19:36:06 +0000