diff options
author | 2015-01-25 14:42:51 +0100 | |
---|---|---|
committer | 2015-01-25 14:42:51 +0100 | |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /checker/inductive.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'checker/inductive.ml')
-rw-r--r-- | checker/inductive.ml | 666 |
1 files changed, 472 insertions, 194 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index 1e12f610..59d1a645 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -1,19 +1,21 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names -open Univ +open Cic open Term open Reduction open Type_errors open Declarations open Environ +open Univ let inductive_of_constructor = fst let index_of_constructor = snd @@ -37,42 +39,60 @@ let find_rectype env c = let find_inductive env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in match t with - | Ind ind - when (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l) + | 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 match t with - | Ind ind - when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l) + | Ind (ind,_) + when (fst (lookup_mind_specif env ind)).mind_finite == CoFinite -> (ind, l) | _ -> raise Not_found let inductive_params (mib,_) = mib.mind_nparams +(** Polymorphic inductives *) + +let inductive_instance mib = + if mib.mind_polymorphic then + 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 *) (* inductives *) -let ind_subst mind mib = +let ind_subst mind mib u = let ntypes = mib.mind_ntypes in - let make_Ik k = Ind (mind,ntypes-k-1) in - list_tabulate make_Ik ntypes + let make_Ik k = Ind ((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 instantiate_params full t u 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) = fold_rel_context (fun (_,copt,_) (largs,subs,ty) -> match (copt, largs, ty) with | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) - | (Some b,_,LetIn(_,_,_,t)) -> (largs, (substl subs b)::subs, t) + | (Some b,_,LetIn(_,_,_,t)) -> + (largs, (substl subs (subst_instance_constr u b))::subs, t) | (_,[],_) -> if full then fail() else ([], subs, ty) | _ -> fail ()) sign @@ -81,15 +101,15 @@ let instantiate_params full t args sign = if rem_args <> [] then fail(); substl subs ty -let full_inductive_instantiate mib params sign = +let full_inductive_instantiate mib u params sign = let dummy = Prop Null in let t = mkArity (sign,dummy) in - fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) + fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) -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) + instantiate_params true (inst_ind t) u params mib.mind_params_ctxt) (************************************************************************) (************************************************************************) @@ -119,12 +139,11 @@ Remark: Set (predicative) is encoded as Type(0) let sort_as_univ = function | Type u -> u -| Prop Null -> type0m_univ -| Prop Pos -> type0_univ +| Prop Null -> Univ.type0m_univ +| Prop Pos -> Univ.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 + Univ.LMap.add u su subst let actualize_decl_level env lev t = let sign,s = dest_arity env t in @@ -157,65 +176,112 @@ 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, - if is_type0m_univ level then Prop Null - else if is_type0_univ level then Prop Pos - else Type level - -let type_of_inductive_knowing_parameters 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 Univ.is_type0m_univ level then Prop Null + (* Non singleton type not containing types are interpretable in Set *) + else if Univ.is_type0_univ level then Prop Pos + (* This is a Type with constraints *) + else Type level + in + (ctx, ty) + +(* 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 = 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 -> + if not mib.mind_polymorphic then a.mind_user_arity + else 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 (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) + +let type_of_inductive_knowing_parameters env mip args = + type_of_inductive_gen env mip args + (* Type of a (non applied) inductive type *) -let type_of_inductive env (_,mip) = +let type_of_inductive env mip = type_of_inductive_knowing_parameters env mip [||] (* 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 -> Univ.sup Univ.type0_univ u + | Type u' -> Univ.sup u u' let max_inductive_sort = - Array.fold_left cumulate_constructor_univ type0m_univ + Array.fold_left cumulate_constructor_univ Univ.type0m_univ (************************************************************************) (* Type of a constructor *) -let type_of_constructor cstr (mib,mip) = +let type_of_constructor_subst 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) + if i > nconstr then error "Not enough constructors in the type."; + constructor_instantiate (fst ind) u mib specif.(i-1) -let arities_of_specif kn (mib,mip) = +let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = + type_of_constructor_subst cstr u 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 mib) specif + Array.map (constructor_instantiate kn u mib) specif @@ -233,15 +299,15 @@ let error_elim_expln kp ki = 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 @@ -254,10 +320,10 @@ 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 (Ind ind, - List.map (lift mip.mind_nrealargs_ctxt) params + List.map (lift mip.mind_nrealdecls) params @ extended_rel_list 0 realargs) (* This exception is local *) @@ -269,7 +335,7 @@ let check_allowed_sort ksort specif = raise (LocalArity (Some(ksort,s,error_elim_expln ksort s))) let is_correct_arity env c (p,pj) ind specif params = - let arsign,_ = get_instantiated_arity specif params in + let arsign,_ = get_instantiated_arity ind specif params in let rec srec env pt ar = let pt' = whd_betadeltaiota env pt in match pt', ar with @@ -305,18 +371,18 @@ let is_correct_arity env c (p,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 dep p = +let build_branches_type (ind,u) (_,mip as specif) params dep 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 = if dep then let cstr = ith_constructor_of_inductive ind (i+1) in let dep_cstr = - applist (Construct cstr,lparams@extended_rel_list 0 args) in + applist (Construct (cstr,u),lparams@extended_rel_list 0 args) in vargs @ [dep_cstr] else vargs in @@ -330,12 +396,12 @@ let build_case_type dep p c realargs = let args = if dep then realargs@[c] else realargs in beta_appvect p (Array.of_list args) -let type_case_branches env (ind,largs) (p,pj) c = - let specif = lookup_mind_specif env ind in +let type_case_branches env (pind,largs) (p,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 dep = is_correct_arity env c (p,pj) ind specif params in - let lc = build_branches_type ind specif params dep p in + let (params,realargs) = List.chop nparams largs in + let dep = is_correct_arity env c (p,pj) pind specif params in + let lc = build_branches_type pind specif params dep p in let ty = build_case_type dep p c realargs in (lc, ty) @@ -346,9 +412,10 @@ let type_case_branches env (ind,largs) (p,pj) c = let check_case_info env indsp ci = let (mib,mip) = 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) + not (eq_ind indsp ci.ci_ind) || + (mib.mind_nparams <> ci.ci_npar) || + (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) || + (mip.mind_consnrealargs <> ci.ci_cstr_nargs) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) (************************************************************************) @@ -399,54 +466,70 @@ 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_recarg r1 r2 = match r1, r2 with +| Norec, Norec -> true +| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 +| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 +| _ -> false + +let eq_wf_paths = Rtree.equal 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 eq_recarg inter_recarg Norec + +let incl_wf_paths = Rtree.incl 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 - _, Dead_code -> s1 - | Dead_code, _ -> 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; (* dB of last fixpoint *) rel_min : int; - (* inductive of recarg of each fixpoint *) - inds : inductive array; - (* the recarg information of inductive family *) - recvec : wf_paths array; (* dB of variables denoting subterms *) genv : subterm_spec Lazy.t list; } -let make_renv env minds recarg (kn,tyi) = - let mib = 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; - inds = minds; - recvec = mind_recvec; - 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) = - { renv with - env = push_rel (x,None,ty) renv.env; + { env = push_rel (x,None,ty) renv.env; rel_min = renv.rel_min+1; 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.lazy_from_val Not_subterm) @@ -458,15 +541,13 @@ let subterm_var p renv = let push_ctxt_renv renv ctxt = let n = rel_context_length ctxt in - { renv with - env = push_rel_context ctxt renv.env; + { env = push_rel_context ctxt renv.env; rel_min = renv.rel_min+n; genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv } let push_fix_renv renv (_,v,_ as recdef) = let n = Array.length v in - { renv with - env = push_rec_types recdef renv.env; + { env = push_rec_types recdef renv.env; rel_min = renv.rel_min+n; genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv } @@ -524,14 +605,171 @@ let branches_specif renv c_spec ci = 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) + 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 + match i with Ind _ -> true | _ -> false + +(* 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 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 = Sort (Type (Universe.make level)) in + let lambda_implicit a = Lambda (Anonymous, implicit_sort, a) in + iterate lambda_implicit n (lift n a) + +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 (Rel (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 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 + match 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 infered 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 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 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 @@ -545,36 +783,40 @@ let rec subterm_specif renv stack t = match 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' = + | 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' @@ -618,9 +860,10 @@ and extract_stack renv a = function (* Check size x is a correct size for recursive calls. *) -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 (************************************************************************) @@ -643,10 +886,38 @@ 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, 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 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 *) @@ -658,7 +929,7 @@ let check_one_fix renv recpos def = match 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: *) @@ -668,9 +939,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 @@ -694,6 +966,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 @@ -725,11 +998,11 @@ let check_one_fix renv recpos def = else check_rec_call renv' [] body) bodies - | Const kn -> + | Const (kn,u) -> 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 renv.env (kn,u), l)) in check_rec_call renv stack value else List.iter (check_rec_call renv []) l @@ -753,16 +1026,7 @@ let check_one_fix renv recpos def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l - | Var id -> - begin - match pi2 (lookup_named id renv.env) with - | None -> - List.iter (check_rec_call renv []) l - | Some c -> - try List.iter (check_rec_call renv []) l - with (FixGuardError _) -> - check_rec_call renv stack (applist(c,l)) - end + | Var _ -> anomaly (Pp.str "Section variable in Coqchk !") | Sort _ -> assert (l = []) @@ -771,6 +1035,8 @@ let check_one_fix renv recpos 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 @@ -780,7 +1046,7 @@ 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 @@ -789,12 +1055,12 @@ let check_one_fix renv recpos def = 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"; + || Array.length nvect <> nbfix + || Array.length types <> nbfix + || 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 raise_err env i err = error_ill_formed_rec_body env err names i in @@ -815,20 +1081,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 get_tree minds in for i = 0 to Array.length bodies - 1 do let (fenv,body) = rdef.(i) in - let renv = make_renv fenv minds 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 done @@ -844,7 +1115,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 @@ -857,7 +1128,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 c with @@ -868,12 +1139,11 @@ 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 @@ -881,10 +1151,10 @@ let check_one_cofix env nbfix def deftype = 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) @@ -893,44 +1163,52 @@ let check_one_cofix env nbfix def deftype = assert (args = []); 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 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 *) |