From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- kernel/inductive.ml | 757 +++++++++++++++++++++++++++++++++++----------------- 1 file changed, 510 insertions(+), 247 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index b78fb5ae..bb57ad25 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1,17 +1,20 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (ind, l) + when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in match kind_of_term t with | Ind ind - when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l) + when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l) | _ -> raise Not_found let inductive_params (mib,_) = mib.mind_nparams +let inductive_paramdecls (mib,u) = + Vars.subst_instance_context u mib.mind_params_ctxt + +let instantiate_inductive_constraints mib u = + if mib.mind_polymorphic then + Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes) + else Univ.Constraint.empty + + (************************************************************************) (* Build the substitution that replaces Rels by the appropriate *) (* inductives *) -let ind_subst mind mib = +let ind_subst mind mib u = let ntypes = mib.mind_ntypes in - let make_Ik k = mkInd (mind,ntypes-k-1) in - list_tabulate make_Ik ntypes + let make_Ik k = mkIndU ((mind,ntypes-k-1),u) in + List.init ntypes make_Ik (* Instantiate inductives in constructor type *) -let constructor_instantiate mind mib c = - let s = ind_subst mind mib in - substl s c +let constructor_instantiate mind u mib c = + let s = ind_subst mind mib u in + substl s (subst_instance_constr u c) let instantiate_params full t args sign = let fail () = - anomaly "instantiate_params: type, ctxt and args mismatch" in + anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = - Sign.fold_rel_context + Context.fold_rel_context (fun (_,copt,_) (largs,subs,ty) -> match (copt, largs, kind_of_term ty) with | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) @@ -75,16 +87,17 @@ let instantiate_params full t args sign = sign ~init:(args,[],t) in - if rem_args <> [] then fail(); + let () = if not (List.is_empty rem_args) then fail () in substl subs ty -let full_inductive_instantiate mib params sign = +let full_inductive_instantiate mib u params sign = let dummy = prop_sort in let t = mkArity (sign,dummy) in - fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) + let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in + Vars.subst_instance_context u ar -let full_constructor_instantiate ((mind,_),(mib,_),params) = - let inst_ind = constructor_instantiate mind mib in +let full_constructor_instantiate ((mind,_),u,(mib,_),params) = + let inst_ind = constructor_instantiate mind u mib in (fun t -> instantiate_params true (inst_ind t) params mib.mind_params_ctxt) @@ -116,18 +129,13 @@ Remark: Set (predicative) is encoded as Type(0) let sort_as_univ = function | Type u -> u -| Prop Null -> type0m_univ -| Prop Pos -> type0_univ - -let cons_subst u su subst = - try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst - with Not_found -> (u, su) :: subst +| Prop Null -> Universe.type0m +| Prop Pos -> Universe.type0 -let actualize_decl_level env lev t = - let sign,s = dest_arity env t in - mkArity (sign,lev) +(* Template polymorphism *) -let polymorphism_on_non_applied_parameters = false +let cons_subst u su subst = + Univ.LMap.add u su subst (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) @@ -145,7 +153,7 @@ let rec make_subst env = function (* arity is a global level which, at typing time, will be enforce *) (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) - let s = sort_as_univ (snd (dest_arity env a)) in + let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in let ctx,subst = make_subst env (sign, exp, args) in d::ctx, cons_subst u s subst | (na,None,t as d)::sign, Some u::exp, [] -> @@ -154,82 +162,96 @@ let rec make_subst env = function (* (actualize_decl_level), then to the conclusion of the arity (via *) (* the substitution) *) let ctx,subst = make_subst env (sign, exp, []) in - if polymorphism_on_non_applied_parameters then - let s = fresh_local_univ () in - let t = actualize_decl_level env (Type s) t in - (na,None,t)::ctx, cons_subst u s subst - else d::ctx, subst | sign, [], _ -> (* Uniform parameters are exhausted *) - sign,[] + sign, Univ.LMap.empty | [], _, _ -> assert false +exception SingletonInductiveBecomesProp of Id.t + let instantiate_universes env ctx ar argsorts = let args = Array.to_list argsorts in - let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in - let level = subst_large_constraints subst ar.poly_level in - ctx, - (* Singleton type not containing types are interpretable in Prop *) - if is_type0m_univ level then prop_sort - (* Non singleton type not containing types are interpretable in Set *) - else if is_type0_univ level then set_sort - (* This is a Type with constraints *) - else Type level - -exception SingletonInductiveBecomesProp of identifier - -let type_of_inductive_knowing_parameters ?(polyprop=true) env mip paramtyps = + let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in + let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in + let ty = + (* Singleton type not containing types are interpretable in Prop *) + if is_type0m_univ level then prop_sort + (* Non singleton type not containing types are interpretable in Set *) + else if is_type0_univ level then set_sort + (* This is a Type with constraints *) + else Type level + in + (ctx, ty) + +(* Type of an inductive type *) + +let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = match mip.mind_arity with - | Monomorphic s -> - s.mind_user_arity - | Polymorphic ar -> - let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes env ctx ar paramtyps in + | RegularArity a -> subst_instance_constr u a.mind_user_arity + | 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 (is_type0m_univ ar.poly_level) && s = prop_sort + if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s then raise (SingletonInductiveBecomesProp mip.mind_typename); mkArity (List.rev ctx,s) -(* Type of a (non applied) inductive type *) +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 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) -let type_of_inductive env (_,mip) = - type_of_inductive_knowing_parameters env mip [||] +let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = + type_of_inductive_gen env mip args (* The max of an array of universes *) let cumulate_constructor_univ u = function | Prop Null -> u - | Prop Pos -> sup type0_univ u - | Type u' -> sup u u' + | Prop Pos -> Universe.sup Universe.type0 u + | Type u' -> Universe.sup u u' let max_inductive_sort = - Array.fold_left cumulate_constructor_univ type0m_univ + Array.fold_left cumulate_constructor_univ Universe.type0m (************************************************************************) (* Type of a constructor *) -let type_of_constructor cstr (mib,mip) = +let type_of_constructor (cstr, u) (mib,mip) = let ind = inductive_of_constructor cstr in let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in if i > nconstr then error "Not enough constructors in the type."; - constructor_instantiate (fst ind) mib specif.(i-1) + constructor_instantiate (fst ind) u mib specif.(i-1) -let arities_of_specif kn (mib,mip) = +let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = + let ty = type_of_constructor 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 mib) specif + Array.map (constructor_instantiate kn u mib) specif let arities_of_constructors ind specif = - arities_of_specif (fst ind) specif + arities_of_specif (fst (fst ind), snd ind) specif -let type_of_constructors ind (mib,mip) = +let type_of_constructors (ind,u) (mib,mip) = let specif = mip.mind_user_lc in - Array.map (constructor_instantiate (fst ind) mib) specif + Array.map (constructor_instantiate (fst ind) u mib) specif (************************************************************************) @@ -237,7 +259,7 @@ let type_of_constructors ind (mib,mip) = let local_rels ctxt = let (rels,_) = - Sign.fold_rel_context_reverse + Context.fold_rel_context_reverse (fun (rels,n) (_,copt,_) -> match copt with None -> (mkRel n :: rels, n+1) @@ -251,18 +273,24 @@ let local_rels ctxt = let inductive_sort_family mip = match mip.mind_arity with - | Monomorphic s -> family_of_sort s.mind_sort - | Polymorphic _ -> InType + | RegularArity s -> family_of_sort s.mind_sort + | TemplateArity _ -> InType let mind_arity mip = mip.mind_arity_ctxt, inductive_sort_family mip -let get_instantiated_arity (mib,mip) params = +let get_instantiated_arity (ind,u) (mib,mip) params = let sign, s = mind_arity mip in - full_inductive_instantiate mib params sign, s + full_inductive_instantiate mib u params sign, s let elim_sorts (_,mip) = mip.mind_kelim +let is_private (mib,_) = mib.mind_private = Some true +let is_primitive_record (mib,_) = + match mib.mind_record with + | Some (Some _) -> true + | _ -> false + let extended_rel_list n hyps = let rec reln l p = function | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps @@ -272,30 +300,33 @@ let extended_rel_list n hyps = reln [] 1 hyps let build_dependent_inductive ind (_,mip) params = - let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist - (mkInd ind, - List.map (lift mip.mind_nrealargs_ctxt) params + (mkIndU ind, + List.map (lift mip.mind_nrealdecls) params @ extended_rel_list 0 realargs) (* This exception is local *) exception LocalArity of (sorts_family * sorts_family * arity_error) option let check_allowed_sort ksort specif = - if not (List.exists ((=) ksort) (elim_sorts specif)) then + let eq_ksort s = match ksort, s with + | InProp, InProp | InSet, InSet | InType, InType -> true + | _ -> false in + if not (List.exists eq_ksort (elim_sorts specif)) then let s = inductive_sort_family (snd specif) in raise (LocalArity (Some(ksort,s,error_elim_explain ksort s))) let is_correct_arity env c pj ind specif params = - let arsign,_ = get_instantiated_arity specif params in - let rec srec env pt ar u = + let arsign,_ = get_instantiated_arity ind specif params in + let rec srec env pt ar = let pt' = whd_betadeltaiota env pt in match kind_of_term pt', ar with | Prod (na1,a1,t), (_,None,a1')::ar' -> - let univ = + let () = try conv env a1 a1' with NotConvertible -> raise (LocalArity None) in - srec (push_rel (na1,None,a1) env) t ar' (union_constraints u univ) + srec (push_rel (na1,None,a1) env) t ar' (* The last Prod domain is the type of the scrutinee *) | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) let env' = push_rel (na1,None,a1) env in @@ -303,17 +334,16 @@ let is_correct_arity env c pj ind specif params = | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in - let univ = + let _ = try conv env a1 dep_ind with NotConvertible -> raise (LocalArity None) in - check_allowed_sort ksort specif; - union_constraints u univ + check_allowed_sort ksort specif | _, (_,Some _,_ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' u + srec (push_rel d env) (lift 1 pt') ar' | _ -> raise (LocalArity None) in - try srec env pj.uj_type (List.rev arsign) empty_constraint + try srec env pj.uj_type (List.rev arsign) with LocalArity kinds -> error_elim_arity env ind (elim_sorts specif) c pj kinds @@ -323,16 +353,16 @@ let is_correct_arity env c pj ind specif params = (* [p] is the predicate, [i] is the constructor number (starting from 0), and [cty] is the type of the constructor (params not instantiated) *) -let build_branches_type ind (_,mip as specif) params p = +let build_branches_type (ind,u) (_,mip as specif) params p = let build_one_branch i cty = - let typi = full_constructor_instantiate (ind,specif,params) cty in + let typi = full_constructor_instantiate (ind,u,specif,params) cty in let (args,ccl) = decompose_prod_assum typi in let nargs = rel_context_length args in let (_,allargs) = decompose_app ccl in - let (lparams,vargs) = list_chop (inductive_params specif) allargs in + let (lparams,vargs) = List.chop (inductive_params specif) allargs in let cargs = let cstr = ith_constructor_of_inductive ind (i+1) in - let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in + let dep_cstr = applist (mkConstructU (cstr,u),lparams@(local_rels args)) in vargs @ [dep_cstr] in let base = beta_appvect (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base args in @@ -340,30 +370,32 @@ let build_branches_type ind (_,mip as specif) params p = (* [p] is the predicate, [c] is the match object, [realargs] is the list of real args of the inductive type *) -let build_case_type n p c realargs = - whd_betaiota (betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) +let build_case_type env n p c realargs = + whd_betaiota env (betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) -let type_case_branches env (ind,largs) pj c = - let specif = lookup_mind_specif env ind in +let type_case_branches env (pind,largs) pj c = + let specif = lookup_mind_specif env (fst pind) in let nparams = inductive_params specif in - let (params,realargs) = list_chop nparams largs in + let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in - let univ = is_correct_arity env c pj ind specif params in - let lc = build_branches_type ind specif params p in - let ty = build_case_type (snd specif).mind_nrealargs_ctxt p c realargs in - (lc, ty, univ) + let () = is_correct_arity env c pj pind specif params in + let lc = build_branches_type pind specif params p in + let ty = build_case_type env (snd specif).mind_nrealdecls p c realargs in + (lc, ty) (************************************************************************) -(* Checking the case annotation is relevent *) +(* Checking the case annotation is relevant *) -let check_case_info env indsp ci = - let (mib,mip) = lookup_mind_specif env indsp in +let check_case_info env (indsp,u) ci = + let (mib,mip as spec) = lookup_mind_specif env indsp in if - not (eq_ind indsp ci.ci_ind) or - (mib.mind_nparams <> ci.ci_npar) or - (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) - then raise (TypeError(env,WrongCaseInfo(indsp,ci))) + not (eq_ind indsp ci.ci_ind) || + not (Int.equal mib.mind_nparams ci.ci_npar) || + not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) || + not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs) || + is_primitive_record spec + then raise (TypeError(env,WrongCaseInfo((indsp,u),ci))) (************************************************************************) (************************************************************************) @@ -413,23 +445,43 @@ type subterm_spec = | Dead_code | Not_subterm -let spec_of_tree t = lazy - (if Rtree.eq_rtree (=) (Lazy.force t) mk_norec - then Not_subterm - else Subterm(Strict,Lazy.force t)) +let eq_wf_paths = Rtree.equal Declareops.eq_recarg + +let pp_recarg = function + | Norec -> Pp.str "Norec" + | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i)) + | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i)) + +let pp_wf_paths = Rtree.pp_tree pp_recarg + +let inter_recarg r1 r2 = match r1, r2 with +| Norec, Norec -> Some r1 +| Mrec i1, Mrec i2 +| Imbr i1, Imbr i2 +| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None +| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None +| _ -> None + +let inter_wf_paths = Rtree.inter Declareops.eq_recarg inter_recarg Norec + +let incl_wf_paths = Rtree.incl Declareops.eq_recarg inter_recarg Norec + +let spec_of_tree t = + if eq_wf_paths t mk_norec + then Not_subterm + else Subterm (Strict, t) + +let inter_spec s1 s2 = + match s1, s2 with + | _, Dead_code -> s1 + | Dead_code, _ -> s2 + | Not_subterm, _ -> s1 + | _, Not_subterm -> s2 + | Subterm (a1,t1), Subterm (a2,t2) -> + Subterm (size_glb a1 a2, inter_wf_paths t1 t2) let subterm_spec_glb = - let glb2 s1 s2 = - match s1, s2 with - s1, Dead_code -> s1 - | Dead_code, s2 -> s2 - | Not_subterm, _ -> Not_subterm - | _, Not_subterm -> Not_subterm - | Subterm (a1,t1), Subterm (a2,t2) -> - if Rtree.eq_rtree (=) t1 t2 then Subterm (size_glb a1 a2, t1) - (* branches do not return objects with same spec *) - else Not_subterm in - Array.fold_left glb2 Dead_code + Array.fold_left inter_spec Dead_code type guard_env = { env : env; @@ -439,13 +491,10 @@ type guard_env = genv : subterm_spec Lazy.t list; } -let make_renv env recarg (kn,tyi) = - let mib = Environ.lookup_mind kn env in - let mind_recvec = - Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in +let make_renv env recarg tree = { env = env; - rel_min = recarg+2; - genv = [Lazy.lazy_from_val(Subterm(Large,mind_recvec.(tyi)))] } + rel_min = recarg+2; (* recarg = 0 ==> Rel 1 -> recarg; Rel 2 -> fix *) + genv = [Lazy.lazy_from_val(Subterm(Large,tree))] } let push_var renv (x,ty,spec) = { env = push_rel (x,None,ty) renv.env; @@ -453,7 +502,7 @@ let push_var renv (x,ty,spec) = genv = spec:: renv.genv } let assign_var_spec renv (i,spec) = - { renv with genv = list_assign renv.genv (i-1) spec } + { renv with genv = List.assign renv.genv (i-1) spec } let push_var_renv renv (x,ty) = push_var renv (x,ty,lazy Not_subterm) @@ -492,7 +541,6 @@ let lookup_subterms env ind = let (_,mip) = lookup_mind_specif env ind in mip.mind_recargs - let match_inductive ind ra = match ra with | (Mrec i | Imbr i) -> eq_ind ind i @@ -517,15 +565,174 @@ let branches_specif renv c_spec ci = (match Lazy.force c_spec with Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) -> let vra = Array.of_list (dest_subterms t).(i) in - assert (nca = Array.length vra); - Array.map - (fun t -> Lazy.force (spec_of_tree (lazy t))) - vra - | Dead_code -> Array.create nca Dead_code - | _ -> Array.create nca Not_subterm) in - list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca) + assert (Int.equal nca (Array.length vra)); + Array.map spec_of_tree vra + | Dead_code -> Array.make nca Dead_code + | _ -> Array.make nca Not_subterm) in + List.init nca (fun j -> lazy (Lazy.force lvra).(j))) car +let check_inductive_codomain env p = + let absctx, ar = dest_lam_assum env p in + 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 + isInd i + +(* The following functions are almost duplicated from indtypes.ml, except +that they carry here a poorer environment (containing less information). *) +let ienv_push_var (env, lra) (x,a,ra) = + (push_rel (x,None,a) env, (Norec,ra)::lra) + +let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = + let mib = Environ.lookup_mind mind env in + let ntypes = mib.mind_ntypes in + let push_ind specif env = + push_rel (Anonymous,None, + hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env + in + let env = Array.fold_right push_ind mib.mind_packets env in + let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in + let lra_ind = Array.rev_to_list rc in + let ra_env = List.map (fun (r,t) -> (r,Rtree.lift ntypes t)) ra_env in + (env, lra_ind @ ra_env) + +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 + match kind_of_term c' with + Prod(na,a,b) -> + let ienv' = ienv_push_var ienv (na,a,mk_norec) in + ienv_decompose_prod ienv' (n-1) b + | _ -> assert false + +let lambda_implicit_lift n a = + let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in + let implicit_sort = mkType (Universe.make level) in + let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in + iterate lambda_implicit n (lift n a) + +(* This removes global parameters of the inductive types in lc (for + nested inductive types only ) *) +let abstract_mind_lc ntyps npars lc = + if Int.equal npars 0 then + lc + else + let make_abs = + List.init ntyps + (function i -> lambda_implicit_lift npars (mkRel (i+1))) + in + Array.map (substl make_abs) lc + +(* [get_recargs_approx env tree ind args] builds an approximation of the recargs +tree for ind, knowing args. The argument tree is used to know when candidate +nested types should be traversed, pruning the tree otherwise. This code is very +close to check_positive in indtypes.ml, but does no positivity 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 + match kind_of_term x with + | Prod (na,b,d) -> + assert (List.is_empty largs); + build_recargs (ienv_push_var ienv (na, b, mk_norec)) tree d + | Rel k -> + (* Free variables are allowed and assigned Norec *) + (try snd (List.nth ra_env (k-1)) + with Failure _ | Invalid_argument _ -> mk_norec) + | Ind ind_kn -> + (* When the inferred tree allows it, we consider that we have a potential + nested inductive type *) + begin match dest_recarg tree with + | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' -> + build_recargs_nested ienv tree (ind_kn, largs) + | _ -> mk_norec + end + | err -> + mk_norec + + and build_recargs_nested (env,ra_env as ienv) tree (((mind,i),u), largs) = + (* If the inferred tree already disallows recursion, no need to go further *) + if eq_wf_paths tree mk_norec then tree + else + let mib = Environ.lookup_mind mind env in + let auxnpar = mib.mind_nparams_rec in + let nonrecpar = mib.mind_nparams - auxnpar in + let (lpar,_) = List.chop auxnpar largs in + let auxntyp = mib.mind_ntypes in + (* Extends the environment with a variable corresponding to + the inductive def *) + let (env',_ as ienv') = ienv_push_inductive ienv ((mind,u),lpar) in + (* Parameters expressed in env' *) + let lpar' = List.map (lift auxntyp) lpar in + (* In case of mutual inductive types, we use the recargs tree which was + computed statically. This is fine because nested inductive types with + mutually recursive containers are not supported. *) + let trees = + if Int.equal auxntyp 1 then [|dest_subterms tree|] + else Array.map (fun mip -> dest_subterms mip.mind_recargs) mib.mind_packets + in + let mk_irecargs j specif = + (* The nested inductive type with parameters removed *) + let auxlcvect = abstract_mind_lc auxntyp auxnpar specif.mind_nf_lc in + let paths = Array.mapi + (fun k c -> + let c' = hnf_prod_applist env' c lpar' in + (* skip non-recursive parameters *) + let (ienv',c') = ienv_decompose_prod ienv' nonrecpar c' in + build_recargs_constructors ienv' trees.(j).(k) c') + auxlcvect + in + mk_paths (Imbr (mind,j)) paths + in + let irecargs = Array.mapi mk_irecargs mib.mind_packets in + (Rtree.mk_rec irecargs).(i) + + 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 + match kind_of_term x with + + | Prod (na,b,d) -> + let () = assert (List.is_empty largs) in + let recarg = build_recargs ienv (List.hd trees) b in + let ienv' = ienv_push_var ienv (na,b,mk_norec) in + recargs_constr_rec ienv' (List.tl trees) (recarg::lrec) d + | hd -> + List.rev lrec + in + recargs_constr_rec ienv trees [] c + in + (* starting with ra_env = [] seems safe because any unbounded Rel will be + assigned Norec *) + build_recargs_nested (env,[]) tree (ind, args) + +(* [restrict_spec env spec p] restricts the size information in spec to what is + allowed to flow through a match with predicate p in environment env. *) +let restrict_spec env spec p = + if spec = Not_subterm then spec + else let absctx, ar = dest_lam_assum env p in + (* Optimization: if the predicate is not dependent, no restriction is needed + and we avoid building the recargs tree. *) + if noccur_with_meta 1 (rel_context_length absctx) ar then spec + else + 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 + match kind_of_term i with + | Ind i -> + begin match spec with + | Dead_code -> spec + | Subterm(st,tree) -> + let recargs = get_recargs_approx env tree i args in + let recargs = inter_wf_paths tree recargs in + Subterm(st,recargs) + | _ -> assert false + end + | _ -> Not_subterm + (* [subterm_specif renv t] computes the recursive structure of [t] and compare its size with the size of the initial recursive argument of the fixpoint we are checking. [renv] collects such information @@ -536,67 +743,77 @@ let rec subterm_specif renv stack t = (* maybe reduction is not always necessary! *) let f,l = decompose_app (whd_betadeltaiota renv.env t) in match kind_of_term f with - | Rel k -> subterm_var k renv - - | Case (ci,_,c,lbr) -> - let stack' = push_stack_closures renv l stack in - let cases_spec = branches_specif renv - (lazy_subterm_specif renv [] c) ci in - let stl = - Array.mapi (fun i br' -> - let stack_br = push_stack_args (cases_spec.(i)) stack' in - subterm_specif renv stack_br br') - lbr in - subterm_spec_glb stl - - | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> - (* when proving that the fixpoint f(x)=e is less than n, it is enough - to prove that e is less than n assuming f is less than n - furthermore when f is applied to a term which is strictly less than - n, one may assume that x itself is strictly less than n - *) - let (ctxt,clfix) = dest_prod renv.env typarray.(i) in - let oind = - let env' = push_rel_context ctxt renv.env in - try Some(fst(find_inductive env' clfix)) - with Not_found -> None in - (match oind with - None -> Not_subterm (* happens if fix is polymorphic *) - | Some ind -> - let nbfix = Array.length typarray in - let recargs = lookup_subterms renv.env ind in - (* pushing the fixpoints *) - let renv' = push_fix_renv renv recdef in - let renv' = + | Rel k -> subterm_var k renv + | Case (ci,p,c,lbr) -> + let stack' = push_stack_closures renv l stack in + let cases_spec = + branches_specif renv (lazy_subterm_specif renv [] c) ci + in + let stl = + Array.mapi (fun i br' -> + let stack_br = push_stack_args (cases_spec.(i)) stack' in + subterm_specif renv stack_br br') + lbr in + let spec = subterm_spec_glb stl in + restrict_spec renv.env spec p + + | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> + (* when proving that the fixpoint f(x)=e is less than n, it is enough + to prove that e is less than n assuming f is less than n + furthermore when f is applied to a term which is strictly less than + n, one may assume that x itself is strictly less than n + *) + if not (check_inductive_codomain renv.env typarray.(i)) then Not_subterm + else + let (ctxt,clfix) = dest_prod renv.env typarray.(i) in + let oind = + let env' = push_rel_context ctxt renv.env in + try Some(fst(find_inductive env' clfix)) + with Not_found -> None in + (match oind with + None -> Not_subterm (* happens if fix is polymorphic *) + | Some (ind, _) -> + let nbfix = Array.length typarray in + let recargs = lookup_subterms renv.env ind in + (* pushing the fixpoints *) + let renv' = push_fix_renv renv recdef in + let renv' = (* Why Strict here ? To be general, it could also be Large... *) - assign_var_spec renv' - (nbfix-i, lazy (Subterm(Strict,recargs))) in - let decrArg = recindxs.(i) in - let theBody = bodies.(i) in - let nbOfAbst = decrArg+1 in - let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in - (* pushing the fix parameters *) - let stack' = push_stack_closures renv l stack in - let renv'' = push_ctxt_renv renv' sign in - let renv'' = - if List.length stack' < nbOfAbst then renv'' - else - let decrArg = List.nth stack' decrArg in - let arg_spec = stack_element_specif decrArg in - assign_var_spec renv'' (1, arg_spec) in - subterm_specif renv'' [] strippedBody) - - | Lambda (x,a,b) -> - assert (l=[]); - let spec,stack' = extract_stack renv a stack in - subterm_specif (push_var renv (x,a,spec)) stack' b + assign_var_spec renv' + (nbfix-i, lazy (Subterm(Strict,recargs))) in + let decrArg = recindxs.(i) in + let theBody = bodies.(i) in + let nbOfAbst = decrArg+1 in + let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in + (* pushing the fix parameters *) + let stack' = push_stack_closures renv l stack in + let renv'' = push_ctxt_renv renv' sign in + let renv'' = + if List.length stack' < nbOfAbst then renv'' + else + let decrArg = List.nth stack' decrArg in + let arg_spec = stack_element_specif decrArg in + assign_var_spec renv'' (1, arg_spec) in + subterm_specif renv'' [] strippedBody) + + | Lambda (x,a,b) -> + let () = assert (List.is_empty l) in + let spec,stack' = extract_stack renv a stack in + subterm_specif (push_var renv (x,a,spec)) stack' b (* Metas and evars are considered OK *) - | (Meta _|Evar _) -> Dead_code + | (Meta _|Evar _) -> Dead_code + + | Proj (p, c) -> + let subt = subterm_specif renv stack c in + (match subt with + | Subterm (s, wf) -> Subterm (Strict, wf) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm) (* Other terms are not subterms *) - | _ -> Not_subterm + | _ -> Not_subterm and lazy_subterm_specif renv stack t = lazy (subterm_specif renv stack t) @@ -606,13 +823,14 @@ and stack_element_specif = function |SArg x -> x and extract_stack renv a = function - | [] -> Lazy.lazy_from_val Not_subterm , [] - | h::t -> stack_element_specif h, t + | [] -> Lazy.lazy_from_val Not_subterm , [] + | h::t -> stack_element_specif h, t (* Check term c can be applied to one of the mutual fixpoints. *) -let check_is_subterm x = +let check_is_subterm x tree = match Lazy.force x with - Subterm (Strict,_) | Dead_code -> true + | Subterm (Strict,tree') -> incl_wf_paths tree tree' + | Dead_code -> true | _ -> false (************************************************************************) @@ -635,25 +853,53 @@ let error_illegal_rec_call renv fx (arg_renv,arg) = let error_partial_apply renv fx = raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx)) +let filter_stack_domain env ci p stack = + let absctx, ar = dest_lam_assum env p in + (* Optimization: if the predicate is not dependent, no restriction is needed + and we avoid building the recargs tree. *) + 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 + match stack, kind_of_term t with + | elt :: stack', Prod (n,a,c0) -> + let d = (n,None,a) in + let ty, args = decompose_app (whd_betadeltaiota env a) in + let elt = match kind_of_term ty with + | Ind ind -> + let spec' = stack_element_specif elt in + (match (Lazy.force spec') with + | Not_subterm | Dead_code -> elt + | Subterm(s,path) -> + let recargs = get_recargs_approx env path ind args in + let path = inter_wf_paths path recargs in + SArg (lazy (Subterm(s,path)))) + | _ -> (SArg (lazy Not_subterm)) + in + elt :: filter_stack (push_rel d env) c0 stack' + | _,_ -> List.fold_right (fun _ l -> SArg (lazy Not_subterm) :: l) stack [] + in + filter_stack env ar stack + (* Check if [def] is a guarded fixpoint body with decreasing arg. given [recpos], the decreasing arguments of each mutually defined fixpoint. *) -let check_one_fix renv recpos def = +let check_one_fix renv recpos trees def = let nfi = Array.length recpos in (* Checks if [t] only make valid recursive calls [stack] is the list of constructor's argument specification and - arguments than will be applied after reduction. + arguments that will be applied after reduction. example u in t where we have (match .. with |.. => t end) u *) let rec check_rec_call renv stack t = (* if [t] does not make recursive calls, it is guarded: *) if noccur_with_meta renv.rel_min nfi t then () else - let (f,l) = decompose_app (whd_betaiotazeta t) in + let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in match kind_of_term f with | Rel p -> (* Test if [p] is a fixpoint (recursive call) *) - if renv.rel_min <= p & p < renv.rel_min+nfi then + if renv.rel_min <= p && p < renv.rel_min+nfi then begin List.iter (check_rec_call renv []) l; (* the position of the invoked fixpoint: *) @@ -663,9 +909,10 @@ let check_one_fix renv recpos def = let stack' = push_stack_closures renv l stack in if List.length stack' <= np then error_partial_apply renv glob else + (* Retrieve the expected tree for the argument *) (* Check the decreasing arg is smaller *) let z = List.nth stack' np in - if not (check_is_subterm (stack_element_specif z)) then + if not (check_is_subterm (stack_element_specif z) trees.(glob)) then begin match z with |SClosure (z,z') -> error_illegal_rec_call renv glob (z,z') |SArg _ -> error_partial_apply renv glob @@ -689,6 +936,7 @@ let check_one_fix renv recpos def = let case_spec = branches_specif renv (lazy_subterm_specif renv [] c_0) ci in let stack' = push_stack_closures renv l stack in + let stack' = filter_stack_domain renv.env ci p stack' in Array.iteri (fun k br' -> let stack_br = push_stack_args case_spec.(k) stack' in check_rec_call renv stack_br br') lrest @@ -713,29 +961,29 @@ let check_one_fix renv recpos def = let stack' = push_stack_closures renv l stack in Array.iteri (fun j body -> - if i=j && (List.length stack' > decrArg) then + if Int.equal i j && (List.length stack' > decrArg) then let recArg = List.nth stack' decrArg in let arg_sp = stack_element_specif recArg in check_nested_fix_body renv' (decrArg+1) arg_sp body else check_rec_call renv' [] body) bodies - | Const kn -> + | Const (kn,u as cu) -> if evaluable_constant kn renv.env then try List.iter (check_rec_call renv []) l with (FixGuardError _ ) -> - let value = (applist(constant_value renv.env kn, l)) in + let value = (applist(constant_value_in renv.env cu, l)) in check_rec_call renv stack value else List.iter (check_rec_call renv []) l | Lambda (x,a,b) -> - assert (l = []); + let () = assert (List.is_empty l) in check_rec_call renv [] a ; let spec, stack' = extract_stack renv a stack in check_rec_call (push_var renv (x,a,spec)) stack' b | Prod (x,a,b) -> - assert (l = [] && stack = []); + let () = assert (List.is_empty l && List.is_empty stack) in check_rec_call renv [] a; check_rec_call (push_var_renv renv (x,a)) [] b @@ -759,15 +1007,18 @@ let check_one_fix renv recpos def = check_rec_call renv stack (applist(c,l)) end - | Sort _ -> assert (l = []) + | Sort _ -> + assert (List.is_empty l) (* l is not checked because it is considered as the meta's context *) | (Evar _ | Meta _) -> () | (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 + if Int.equal decr 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body else match kind_of_term body with @@ -775,23 +1026,23 @@ let check_one_fix renv recpos def = check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in check_nested_fix_body renv' (decr-1) recArgsDecrArg b - | _ -> anomaly "Not enough abstractions in fix body" + | _ -> anomaly (Pp.str "Not enough abstractions in fix body") in check_rec_call renv [] def let judgment_of_fixpoint (_, types, bodies) = - array_map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies + Array.map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = let nbfix = Array.length bodies in - if nbfix = 0 - or Array.length nvect <> nbfix - or Array.length types <> nbfix - or Array.length names <> nbfix - or bodynum < 0 - or bodynum >= nbfix - then anomaly "Ill-formed fix term"; + if Int.equal nbfix 0 + || not (Int.equal (Array.length nvect) nbfix) + || not (Int.equal (Array.length types) nbfix) + || not (Int.equal (Array.length names) nbfix) + || bodynum < 0 + || bodynum >= nbfix + then anomaly (Pp.str "Ill-formed fix term"); let fixenv = push_rec_types recdef env in let vdefj = judgment_of_fixpoint recdef in let raise_err env i err = @@ -805,7 +1056,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then let env' = push_rel (x, None, a) env in - if n = k+1 then + if Int.equal n (k + 1) then (* get the inductive type of the fixpoint *) let (mind, _) = try find_inductive env a @@ -813,20 +1064,25 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = raise_err env i (RecursionNotOnInductiveType a) in (mind, (env', b)) else check_occur env' (n+1) b - else anomaly "check_one_fix: Bad occurrence of recursive call" + else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call") | _ -> raise_err env i NotEnoughAbstractionInFixBody in check_occur fixenv 1 def in (* Do it on every fixpoint *) - let rv = array_map2_i find_ind nvect bodies in + let rv = Array.map2_i find_ind nvect bodies in (Array.map fst rv, Array.map snd rv) let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = let (minds, rdef) = inductive_of_mutfix env fix in + let get_tree (kn,i) = + let mib = Environ.lookup_mind kn env in + mib.mind_packets.(i).mind_recargs + in + let trees = Array.map (fun (mind,_) -> get_tree mind) minds in for i = 0 to Array.length bodies - 1 do let (fenv,body) = rdef.(i) in - let renv = make_renv fenv nvect.(i) minds.(i) in - try check_one_fix renv nvect body + let renv = make_renv fenv nvect.(i) trees.(i) in + try check_one_fix renv nvect trees body with FixGuardError (fixenv,err) -> error_ill_formed_rec_body fixenv err names i (push_rec_types recdef env) (judgment_of_fixpoint recdef) @@ -843,7 +1099,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; exception CoFixGuardError of env * guard_error let anomaly_ill_typed () = - anomaly "check_one_cofix: too many arguments applied to constructor" + 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 @@ -856,7 +1112,7 @@ let rec codomain_is_coind env c = raise (CoFixGuardError (env, CodomainNotInductiveType b))) let check_one_cofix env nbfix def deftype = - let rec check_rec_call env alreadygrd n vlra t = + 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 match kind_of_term c with @@ -867,69 +1123,76 @@ let check_one_cofix env nbfix def deftype = raise (CoFixGuardError (env,UnguardedRecursiveCall t)) else if not(List.for_all (noccur_with_meta n nbfix) args) then raise (CoFixGuardError (env,NestedRecursiveOccurrences)) - - | Construct (_,i as cstr_kn) -> + | Construct ((_,i as cstr_kn),u) -> let lra = vlra.(i-1) in let mI = inductive_of_constructor cstr_kn in let (mib,mip) = lookup_mind_specif env mI in - let realargs = list_skipn mib.mind_nparams args in + let realargs = List.skipn mib.mind_nparams args in let rec process_args_of_constr = function | (t::lr), (rar::lrar) -> - if rar = mk_norec then + if eq_wf_paths rar mk_norec then if noccur_with_meta n nbfix t then process_args_of_constr (lr, lrar) else raise (CoFixGuardError (env,RecCallInNonRecArgOfConstructor t)) - else - let spec = dest_subterms rar in - check_rec_call env true n spec t; - process_args_of_constr (lr, lrar) + else begin + check_rec_call env true n rar (dest_subterms rar) t; + process_args_of_constr (lr, lrar) + end | [],_ -> () | _ -> anomaly_ill_typed () in process_args_of_constr (realargs, lra) | Lambda (x,a,b) -> - assert (args = []); + let () = assert (List.is_empty args) in if noccur_with_meta n nbfix a then let env' = push_rel (x, None, a) env in - check_rec_call env' alreadygrd (n+1) vlra b + check_rec_call env' alreadygrd (n+1) tree vlra b else raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) | CoFix (j,(_,varit,vdefs as recdef)) -> if List.for_all (noccur_with_meta n nbfix) args then - if array_for_all (noccur_with_meta n nbfix) varit then + if Array.for_all (noccur_with_meta n nbfix) varit then let nbfix = Array.length vdefs in let env' = push_rec_types recdef env in - (Array.iter (check_rec_call env' alreadygrd (n+nbfix) vlra) vdefs; - List.iter (check_rec_call env alreadygrd n vlra) args) + (Array.iter (check_rec_call env' alreadygrd (n+nbfix) tree vlra) vdefs; + List.iter (check_rec_call env alreadygrd n tree vlra) args) else raise (CoFixGuardError (env,RecCallInTypeOfDef c)) else raise (CoFixGuardError (env,UnguardedRecursiveCall c)) | Case (_,p,tm,vrest) -> - if (noccur_with_meta n nbfix p) then - if (noccur_with_meta n nbfix tm) then - if (List.for_all (noccur_with_meta n nbfix) args) then - Array.iter (check_rec_call env alreadygrd n vlra) vrest - else - raise (CoFixGuardError (env,RecCallInCaseFun c)) - else - raise (CoFixGuardError (env,RecCallInCaseArg c)) - else - raise (CoFixGuardError (env,RecCallInCasePred c)) + begin + let tree = match restrict_spec env (Subterm (Strict, tree)) p with + | Dead_code -> assert false + | Subterm (_, tree') -> tree' + | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c)) + in + if (noccur_with_meta n nbfix p) then + if (noccur_with_meta n nbfix tm) then + if (List.for_all (noccur_with_meta n nbfix) args) then + let vlra = dest_subterms tree in + Array.iter (check_rec_call env alreadygrd n tree vlra) vrest + else + raise (CoFixGuardError (env,RecCallInCaseFun c)) + else + raise (CoFixGuardError (env,RecCallInCaseArg c)) + else + raise (CoFixGuardError (env,RecCallInCasePred c)) + end | Meta _ -> () | Evar _ -> - List.iter (check_rec_call env alreadygrd n vlra) args + List.iter (check_rec_call env alreadygrd n tree vlra) args | _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in - let (mind, _) = codomain_is_coind env deftype in + let ((mind, _),_) = codomain_is_coind env deftype in let vlra = lookup_subterms env mind in - check_rec_call env false 1 (dest_subterms vlra) def + check_rec_call env false 1 vlra (dest_subterms vlra) def (* The function which checks that the whole block of definitions satisfies the guarded condition *) -- cgit v1.2.3