summaryrefslogtreecommitdiff
path: root/checker/inductive.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/inductive.ml')
-rw-r--r--checker/inductive.ml666
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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 23:12:08 +0000