From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- kernel/inductive.ml | 241 +++++++++++++++++++++++++--------------------------- 1 file changed, 115 insertions(+), 126 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 99ec1650..5bcba626 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductive.ml 11647 2008-12-02 10:40:11Z barras $ *) +(* $Id$ *) open Util open Names @@ -55,7 +55,7 @@ let inductive_params (mib,_) = mib.mind_nparams (* inductives *) let ind_subst mind mib = let ntypes = mib.mind_ntypes in - let make_Ik k = mkInd (mind,ntypes-k-1) in + let make_Ik k = mkInd (mind,ntypes-k-1) in list_tabulate make_Ik ntypes (* Instantiate inductives in constructor type *) @@ -64,7 +64,7 @@ let constructor_instantiate mind mib c = substl s c let instantiate_params full t args sign = - let fail () = + let fail () = anomaly "instantiate_params: type, ctxt and args mismatch" in let (rem_args, subs, ty) = Sign.fold_rel_context @@ -75,7 +75,7 @@ let instantiate_params full t args sign = | (_,[],_) -> if full then fail() else ([], subs, ty) | _ -> fail ()) sign - ~init:(args,[],t) + ~init:(args,[],t) in if rem_args <> [] then fail(); substl subs ty @@ -101,11 +101,11 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) = let number_of_inductives mib = Array.length mib.mind_packets let number_of_constructors mip = Array.length mip.mind_consnames -(* +(* Computing the actual sort of an applied or partially applied inductive type: I_i: forall uniformparams:utyps, forall otherparams:otyps, Type(a) -uniformargs : utyps +uniformargs : utyps otherargs : otyps I_1:forall ...,s_1;...I_n:forall ...,s_n |- sort(C_kj(uniformargs)) = s_kj s'_k = max(..s_kj..) @@ -221,11 +221,11 @@ let type_of_constructor cstr (mib,mip) = if i > nconstr then error "Not enough constructors in the type."; constructor_instantiate (fst ind) mib specif.(i-1) -let arities_of_specif kn (mib,mip) = +let arities_of_specif kn (mib,mip) = let specif = mip.mind_nf_lc in Array.map (constructor_instantiate kn mib) specif -let arities_of_constructors ind specif = +let arities_of_constructors ind specif = arities_of_specif (fst ind) specif let type_of_constructors ind (mib,mip) = @@ -250,7 +250,7 @@ let local_rels ctxt = None -> (mkRel n :: rels, n+1) | Some _ -> (rels, n+1)) ~init:([],1) - ctxt + ctxt in rels @@ -258,7 +258,7 @@ let local_rels ctxt = let inductive_sort_family mip = match mip.mind_arity with - | Monomorphic s -> family_of_sort s.mind_sort + | Monomorphic s -> family_of_sort s.mind_sort | Polymorphic _ -> InType let mind_arity mip = @@ -270,26 +270,30 @@ let get_instantiated_arity (mib,mip) params = let elim_sorts (_,mip) = mip.mind_kelim -let rel_list n m = - let rec reln l p = - if p>m then l else reln (mkRel(n+p)::l) (p+1) - in - reln [] 1 +let extended_rel_list n hyps = + let rec reln l p = function + | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps + | (_,Some _,_) :: hyps -> reln l (p+1) hyps + | [] -> l + in + reln [] 1 hyps let build_dependent_inductive ind (_,mip) params = - let nrealargs = mip.mind_nrealargs in - applist - (mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs)) + let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + applist + (mkInd ind, + List.map (lift mip.mind_nrealargs_ctxt) 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 + if not (List.exists ((=) ksort) (elim_sorts specif)) then let s = inductive_sort_family (snd specif) in raise (LocalArity (Some(ksort,s,error_elim_expln ksort s))) -let is_correct_arity env c pj ind specif params = +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 pt' = whd_betadeltaiota env pt in @@ -301,20 +305,19 @@ let is_correct_arity env c pj ind specif params = srec (push_rel (na1,None,a1) env) t ar' (Constraint.union u univ) | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *) let ksort = match kind_of_term (whd_betadeltaiota env a2) with - | Sort s -> family_of_sort s + | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in - let dep_ind = build_dependent_inductive ind specif params in + let dep_ind = build_dependent_inductive ind specif params in let univ = try conv env a1 dep_ind with NotConvertible -> raise (LocalArity None) in check_allowed_sort ksort specif; - (true, Constraint.union u univ) - | Sort s', [] -> - check_allowed_sort (family_of_sort s') specif; - (false, u) + Constraint.union u univ + | _, (_,Some _,_ as d)::ar' -> + srec (push_rel d env) (lift 1 pt') ar' u | _ -> raise (LocalArity None) - in + in try srec env pj.uj_type (List.rev arsign) Constraint.empty with LocalArity kinds -> error_elim_arity env ind (elim_sorts specif) c pj kinds @@ -325,7 +328,7 @@ 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 dep p = +let build_branches_type ind (_,mip as specif) params p = let build_one_branch i cty = let typi = full_constructor_instantiate (ind,specif,params) cty in let (args,ccl) = decompose_prod_assum typi in @@ -333,50 +336,36 @@ let build_branches_type ind (_,mip as specif) params dep p = let (_,allargs) = decompose_app ccl 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 (mkConstruct cstr,lparams@(local_rels args)) in - vargs @ [dep_cstr] - else - vargs in + let cstr = ith_constructor_of_inductive ind (i+1) in + let dep_cstr = applist (mkConstruct cstr,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 Array.mapi build_one_branch mip.mind_nf_lc (* [p] is the predicate, [c] is the match object, [realargs] is the list of real args of the inductive type *) -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 build_case_type n p c realargs = + whd_betaiota (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 specif = lookup_mind_specif env ind in let nparams = inductive_params specif in let (params,realargs) = list_chop nparams largs in let p = pj.uj_val in - let (dep,univ) = is_correct_arity env c pj ind specif params in - let lc = build_branches_type ind specif params dep p in - let ty = build_case_type dep p c realargs 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) (************************************************************************) (* Checking the case annotation is relevent *) -let rec inductive_kn_equiv env kn1 kn2 = - match (lookup_mind kn1 env).mind_equiv with - | Some kn1' -> inductive_kn_equiv env kn2 kn1' - | None -> match (lookup_mind kn2 env).mind_equiv with - | Some kn2' -> inductive_kn_equiv env kn2' kn1 - | None -> false - -let inductive_equiv env (kn1,i1) (kn2,i2) = - i1=i2 & inductive_kn_equiv env kn1 kn2 - let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if - not (Closure.mind_equiv env indsp ci.ci_ind) or + not (eq_ind indsp ci.ci_ind) or (mib.mind_nparams <> ci.ci_npar) or (mip.mind_consnrealdecls <> ci.ci_cstr_nargs) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) @@ -386,7 +375,7 @@ let check_case_info env indsp ci = (* Guard conditions for fix and cofix-points *) -(* Check if t is a subterm of Rel n, and gives its specification, +(* Check if t is a subterm of Rel n, and gives its specification, assuming lst already gives index of subterms with corresponding specifications of recursive arguments *) @@ -431,7 +420,7 @@ type subterm_spec = let spec_of_tree t = if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t) - + let subterm_spec_glb = let glb2 s1 s2 = match s1,s2 with @@ -444,7 +433,7 @@ let subterm_spec_glb = (* branches do not return objects with same spec *) else Not_subterm in Array.fold_left glb2 Dead_code - + type guard_env = { env : env; (* dB of last fixpoint *) @@ -468,7 +457,7 @@ let make_renv env minds recarg (kn,tyi) = genv = [Subterm(Large,mind_recvec.(tyi))] } let push_var renv (x,ty,spec) = - { renv with + { renv with env = push_rel (x,None,ty) renv.env; rel_min = renv.rel_min+1; genv = spec:: renv.genv } @@ -480,7 +469,7 @@ let push_var_renv renv (x,ty) = push_var renv (x,ty,Not_subterm) (* Fetch recursive information about a variable p *) -let subterm_var p renv = +let subterm_var p renv = try List.nth renv.genv (p-1) with Failure _ | Invalid_argument _ -> Not_subterm @@ -490,7 +479,7 @@ let add_subterm renv (x,a,spec) = let push_ctxt_renv renv ctxt = let n = rel_context_length ctxt in - { renv with + { renv with env = push_rel_context ctxt renv.env; rel_min = renv.rel_min+n; genv = iterate (fun ge -> Not_subterm::ge) n renv.genv } @@ -529,8 +518,8 @@ let lookup_subterms env ind = associated to its own subterms. Rq: if branch is not eta-long, then the recursive information is not propagated to the missing abstractions *) -let case_branches_specif renv c_spec ind lbr = - let rec push_branch_args renv lrec c = +let case_branches_specif renv c_spec ind lbr = + let rec push_branch_args renv lrec c = match lrec with ra::lr -> let c' = whd_betadeltaiota renv.env c in @@ -546,7 +535,7 @@ let case_branches_specif renv c_spec ind lbr = let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in assert (Array.length sub_spec = Array.length lbr); array_map2 (push_branch_args renv) sub_spec lbr - | Dead_code -> + | Dead_code -> let t = dest_subterms (lookup_subterms renv.env ind) in let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in assert (Array.length sub_spec = Array.length lbr); @@ -559,22 +548,19 @@ let case_branches_specif renv c_spec ind lbr = about variables. *) -let rec subterm_specif renv t = +let rec subterm_specif renv t = (* maybe reduction is not always necessary! *) let f,l = decompose_app (whd_betadeltaiota renv.env t) in - match kind_of_term f with + match kind_of_term f with | Rel k -> subterm_var k renv | Case (ci,_,c,lbr) -> - if Array.length lbr = 0 then Dead_code - else - let c_spec = subterm_specif renv c in - let lbr_spec = case_branches_specif renv c_spec ci.ci_ind lbr in - let stl = - Array.map (fun (renv',br') -> subterm_specif renv' br') - lbr_spec in - subterm_spec_glb stl - + let lbr_spec = case_subterm_specif renv ci c lbr in + let stl = + Array.map (fun (renv',br') -> subterm_specif renv' br') + lbr_spec 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 @@ -597,7 +583,7 @@ let rec subterm_specif renv t = (* Why Strict here ? To be general, it could also be Large... *) assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in - let decrArg = recindxs.(i) 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 @@ -611,7 +597,7 @@ let rec subterm_specif renv t = assign_var_spec renv'' (1, arg_spec) in subterm_specif renv'' strippedBody) - | Lambda (x,a,b) -> + | Lambda (x,a,b) -> assert (l=[]); subterm_specif (push_var_renv renv (x,a)) b @@ -621,9 +607,14 @@ let rec subterm_specif renv t = (* Other terms are not subterms *) | _ -> Not_subterm - +and case_subterm_specif renv ci c lbr = + if Array.length lbr = 0 then [||] + else + let c_spec = subterm_specif renv c in + case_branches_specif renv c_spec ci.ci_ind lbr + (* Check term c can be applied to one of the mutual fixpoints. *) -let check_is_subterm renv c = +let check_is_subterm renv c = match subterm_specif renv c with Subterm (Strict,_) | Dead_code -> true | _ -> false @@ -651,21 +642,21 @@ let error_partial_apply renv fx = given [recpos], the decreasing arguments of each mutually defined fixpoint. *) let check_one_fix renv recpos def = - let nfi = Array.length recpos in + let nfi = Array.length recpos in (* Checks if [t] only make valid recursive calls *) - let rec check_rec_call renv t = + let rec check_rec_call renv 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 match kind_of_term f with - | Rel p -> - (* Test if [p] is a fixpoint (recursive call) *) + | Rel p -> + (* Test if [p] is a fixpoint (recursive call) *) 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: *) + (* the position of the invoked fixpoint: *) let glob = renv.rel_min+nfi-1-p in (* the decreasing arg of the rec call: *) let np = recpos.(glob) in @@ -691,31 +682,29 @@ let check_one_fix renv recpos def = List.iter (check_rec_call renv) (c_0::p::l); (* compute the recarg information for the arguments of each branch *) - let c_spec = subterm_specif renv c_0 in - let lbr = case_branches_specif renv c_spec ci.ci_ind lrest in + let lbr = case_subterm_specif renv ci c_0 lrest in Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr (* Enables to traverse Fixpoint definitions in a more intelligent way, ie, the rule : - if - g = Fix g/p := [y1:T1]...[yp:Tp]e & - - f is guarded with respect to the set of pattern variables S + if - g = fix g (y1:T1)...(yp:Tp) {struct yp} := e & + - f is guarded with respect to the set of pattern variables S in a1 ... am & - - f is guarded with respect to the set of pattern variables S + - f is guarded with respect to the set of pattern variables S in T1 ... Tp & - ap is a sub-term of the formal argument of f & - f is guarded with respect to the set of pattern variables S+{yp} in e then f is guarded with respect to S in (g a1 ... am). Eduardo 7/9/98 *) - | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> List.iter (check_rec_call renv) l; Array.iter (check_rec_call renv) typarray; let decrArg = recindxs.(i) in - let renv' = push_fix_renv renv recdef in + let renv' = push_fix_renv renv recdef in if (List.length l < (decrArg+1)) then Array.iter (check_rec_call renv') bodies - else + else Array.iteri (fun j body -> if i=j then @@ -725,8 +714,8 @@ let check_one_fix renv recpos def = else check_rec_call renv' body) bodies - | Const kn -> - if evaluable_constant kn renv.env then + | Const kn -> + if evaluable_constant kn renv.env then try List.iter (check_rec_call renv) l with (FixGuardError _ ) -> check_rec_call renv(applist(constant_value renv.env kn, l)) @@ -734,14 +723,14 @@ let check_one_fix renv recpos def = (* The cases below simply check recursively the condition on the subterms *) - | Cast (a,_, b) -> + | Cast (a,_, b) -> List.iter (check_rec_call renv) (a::b::l) | Lambda (x,a,b) -> List.iter (check_rec_call renv) (a::l); check_rec_call (push_var_renv renv (x,a)) b - | Prod (x,a,b) -> + | Prod (x,a,b) -> List.iter (check_rec_call renv) (a::l); check_rec_call (push_var_renv renv (x,a)) b @@ -787,9 +776,9 @@ let judgment_of_fixpoint (_, 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 + let nbfix = Array.length bodies in if nbfix = 0 - or Array.length nvect <> nbfix + or Array.length nvect <> nbfix or Array.length types <> nbfix or Array.length names <> nbfix or bodynum < 0 @@ -800,18 +789,18 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = let raise_err env i err = error_ill_formed_rec_body env err names i fixenv vdefj in (* Check the i-th definition with recarg k *) - let find_ind i k def = - (* check fi does not appear in the k+1 first abstractions, + let find_ind i k def = + (* check fi does not appear in the k+1 first abstractions, gives the type of the k+1-eme abstraction (must be an inductive) *) - let rec check_occur env n def = + let rec check_occur env n def = match kind_of_term (whd_betadeltaiota env def) with - | Lambda (x,a,b) -> + | 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 (* get the inductive type of the fixpoint *) - let (mind, _) = - try find_inductive env a + let (mind, _) = + try find_inductive env a with Not_found -> raise_err env i (RecursionNotOnInductiveType a) in (mind, (env', b)) @@ -831,7 +820,7 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = let renv = make_renv fenv minds nvect.(i) minds.(i) in try check_one_fix renv nvect body with FixGuardError (fixenv,err) -> - error_ill_formed_rec_body fixenv err names i + error_ill_formed_rec_body fixenv err names i (push_rec_types recdef env) (judgment_of_fixpoint recdef) done @@ -852,17 +841,17 @@ let rec codomain_is_coind env c = let b = whd_betadeltaiota env c in match kind_of_term b with | Prod (x,a,b) -> - codomain_is_coind (push_rel (x, None, a) env) b - | _ -> + codomain_is_coind (push_rel (x, None, a) env) b + | _ -> (try find_coinductive env b with Not_found -> raise (CoFixGuardError (env, CodomainNotInductiveType b))) -let check_one_cofix env nbfix def deftype = +let check_one_cofix env nbfix def deftype = let rec check_rec_call env alreadygrd n 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 + match kind_of_term c with | Rel p when n <= p && p < n+nbfix -> (* recursive call: must be guarded and no nested recursive call allowed *) @@ -870,14 +859,14 @@ 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) -> - let lra = vlra.(i-1) in + 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 rec process_args_of_constr = function - | (t::lr), (rar::lrar) -> + | (t::lr), (rar::lrar) -> if rar = mk_norec then if noccur_with_meta n nbfix t then process_args_of_constr (lr, lrar) @@ -888,26 +877,26 @@ let check_one_cofix env nbfix def deftype = check_rec_call env true n spec t; process_args_of_constr (lr, lrar) | [],_ -> () - | _ -> anomaly_ill_typed () + | _ -> anomaly_ill_typed () in process_args_of_constr (realargs, lra) - + | Lambda (x,a,b) -> 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 - else + else raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) - + | CoFix (j,(_,varit,vdefs as recdef)) -> if (List.for_all (noccur_with_meta n nbfix) args) - then + then let nbfix = Array.length vdefs in if (array_for_all (noccur_with_meta n nbfix) varit) then let env' = push_rec_types recdef env in (Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs; List.iter (check_rec_call env alreadygrd n vlra) args) - else + else raise (CoFixGuardError (env,RecCallInTypeOfDef c)) else raise (CoFixGuardError (env,UnguardedRecursiveCall c)) @@ -917,32 +906,32 @@ let check_one_cofix env nbfix def deftype = 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 + else raise (CoFixGuardError (env,RecCallInCaseFun c)) - else + else raise (CoFixGuardError (env,RecCallInCaseArg c)) - else + else raise (CoFixGuardError (env,RecCallInCasePred c)) - + | Meta _ -> () | Evar _ -> List.iter (check_rec_call env alreadygrd n vlra) args - - | _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in + + | _ -> 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 -(* The function which checks that the whole block of definitions +(* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env (bodynum,(names,types,bodies as recdef)) = - let nbfix = Array.length bodies in +let check_cofix env (bodynum,(names,types,bodies as recdef)) = + let nbfix = Array.length bodies in for i = 0 to nbfix-1 do let fixenv = push_rec_types recdef env in try check_one_cofix fixenv nbfix bodies.(i) types.(i) - with CoFixGuardError (errenv,err) -> - error_ill_formed_rec_body errenv err names i + with CoFixGuardError (errenv,err) -> + error_ill_formed_rec_body errenv err names i fixenv (judgment_of_fixpoint recdef) done -- cgit v1.2.3