diff options
Diffstat (limited to 'checker/inductive.ml')
| -rw-r--r-- | checker/inductive.ml | 88 |
1 files changed, 23 insertions, 65 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index 43a32ea24d..c4ffc141ff 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic @@ -31,20 +31,20 @@ let lookup_mind_specif env (kn,tyi) = (mib, mib.mind_packets.(tyi)) let find_rectype env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match t with | Ind ind -> (ind, l) | _ -> raise Not_found let find_inductive env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match t with | Ind (ind,_) when (fst (lookup_mind_specif env ind)).mind_finite != CoFinite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match t with | Ind (ind,_) when (fst (lookup_mind_specif env ind)).mind_finite == CoFinite -> (ind, l) @@ -59,16 +59,6 @@ let inductive_instance mib = UContext.instance mib.mind_universes else Instance.empty -let inductive_context mib = - if mib.mind_polymorphic then - instantiate_univ_context mib.mind_universes - else UContext.empty - -let instantiate_inductive_constraints mib u = - if mib.mind_polymorphic then - subst_instance_constraints u (UContext.constraints mib.mind_universes) - else Constraint.empty - (************************************************************************) (* Build the substitution that replaces Rels by the appropriate *) @@ -190,8 +180,6 @@ let rec make_subst env = in make Univ.LMap.empty -exception SingletonInductiveBecomesProp of Id.t - let instantiate_universes env ctx ar argsorts = let args = Array.to_list argsorts in let subst = make_subst env (ctx,ar.template_param_levels,args) in @@ -208,11 +196,7 @@ let instantiate_universes env ctx ar argsorts = (* Type of an inductive type *) -let is_prop_sort = function - | Prop Null -> true - | _ -> false - -let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = +let type_of_inductive_gen env ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> if not mib.mind_polymorphic then a.mind_user_arity @@ -220,25 +204,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in let ctx,s = instantiate_universes env ctx ar paramtyps in - (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. - the situation where a non-Prop singleton inductive becomes Prop - when applied to Prop params *) - if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s - then raise (SingletonInductiveBecomesProp mip.mind_typename); - mkArity (List.rev ctx,s) - -let type_of_inductive env pind = - type_of_inductive_gen env pind [||] - -let constrained_type_of_inductive env ((mib,mip),u as pind) = - let ty = type_of_inductive_gen env pind [||] in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) - -let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = - let ty = type_of_inductive_gen env pind args in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) + mkArity (List.rev ctx,s) let type_of_inductive_knowing_parameters env mip args = type_of_inductive_gen env mip args @@ -275,16 +241,6 @@ let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = let type_of_constructor cstru mspec = type_of_constructor_gen cstru mspec -let type_of_constructor_in_ctx cstr (mib,mip as mspec) = - let u = Univ.UContext.instance mib.mind_universes in - let c = type_of_constructor_gen (cstr, u) mspec in - (c, mib.mind_universes) - -let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = - let ty = type_of_constructor_gen cstru ind in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) - let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in Array.map (constructor_instantiate kn u mib) specif @@ -343,7 +299,7 @@ let check_allowed_sort ksort specif = let is_correct_arity env c (p,pj) ind specif params = let arsign,_ = get_instantiated_arity ind specif params in let rec srec env pt ar = - let pt' = whd_betadeltaiota env pt in + let pt' = whd_all env pt in match pt', ar with | Prod (na1,a1,t), LocalAssum (_,a1')::ar' -> (try conv env a1 a1' @@ -351,7 +307,7 @@ let is_correct_arity env c (p,pj) ind specif params = srec (push_rel (LocalAssum (na1,a1)) env) t ar' | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) let env' = push_rel (LocalAssum (na1,a1)) env in - let ksort = match (whd_betadeltaiota env' a2) with + let ksort = match (whd_all env' a2) with | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in @@ -622,7 +578,7 @@ let check_inductive_codomain env p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,l' = decompose_app (whd_betadeltaiota env s) in + let i,l' = decompose_app (whd_all env s) in match i with Ind _ -> true | _ -> false (* The following functions are almost duplicated from indtypes.ml, except @@ -646,7 +602,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let rec ienv_decompose_prod (env,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else - let c' = whd_betadeltaiota env c in + let c' = whd_all env c in match c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -676,7 +632,7 @@ close to check_positive in indtypes.ml, but does no positivy check and does not compute the number of recursive arguments. *) let get_recargs_approx env tree ind args = let rec build_recargs (env, ra_env as ienv) tree c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match x with | Prod (na,b,d) -> assert (List.is_empty largs); @@ -735,7 +691,7 @@ let get_recargs_approx env tree ind args = and build_recargs_constructors ienv trees c = let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match x with | Prod (na,b,d) -> @@ -764,7 +720,7 @@ let restrict_spec env spec p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,args = decompose_app (whd_betadeltaiota env s) in + let i,args = decompose_app (whd_all env s) in match i with | Ind i -> begin match spec with @@ -786,7 +742,7 @@ let restrict_spec env spec p = let rec subterm_specif renv stack t = (* maybe reduction is not always necessary! *) - let f,l = decompose_app (whd_betadeltaiota renv.env t) in + let f,l = decompose_app (whd_all renv.env t) in match f with | Rel k -> subterm_var k renv @@ -900,11 +856,11 @@ let filter_stack_domain env ci p stack = if noccur_with_meta 1 (rel_context_length absctx) ar then stack else let env = push_rel_context absctx env in let rec filter_stack env ar stack = - let t = whd_betadeltaiota env ar in + let t = whd_all env ar in match stack, t with | elt :: stack', Prod (n,a,c0) -> let d = LocalAssum (n,a) in - let ty, args = decompose_app (whd_betadeltaiota env a) in + let ty, args = decompose_app (whd_all env a) in let elt = match ty with | Ind ind -> let spec' = stack_element_specif elt in @@ -1033,6 +989,10 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l + | Proj (p, c) -> + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + | Var _ -> anomaly (Pp.str "Section variable in Coqchk !") | Sort _ -> assert (l = []) @@ -1042,8 +1002,6 @@ let check_one_fix renv recpos trees def = | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) - | Proj (p, c) -> check_rec_call renv [] c - and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body @@ -1076,7 +1034,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (* check fi does not appear in the k+1 first abstractions, gives the type of the k+1-eme abstraction (must be an inductive) *) let rec check_occur env n def = - match (whd_betadeltaiota env def) with + match (whd_all env def) with | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then let env' = push_rel (LocalAssum (x,a)) env in @@ -1125,7 +1083,7 @@ let anomaly_ill_typed () = anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") let rec codomain_is_coind env c = - let b = whd_betadeltaiota env c in + let b = whd_all env c in match b with | Prod (x,a,b) -> codomain_is_coind (push_rel (LocalAssum (x,a)) env) b @@ -1137,7 +1095,7 @@ let rec codomain_is_coind env c = let check_one_cofix env nbfix def deftype = let rec check_rec_call env alreadygrd n tree vlra t = if not (noccur_with_meta n nbfix t) then - let c,args = decompose_app (whd_betadeltaiota env t) in + let c,args = decompose_app (whd_all env t) in match c with | Rel p when n <= p && p < n+nbfix -> (* recursive call: must be guarded and no nested recursive |