From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- checker/inductive.ml | 352 +++++++++++++++++++++++++-------------------------- 1 file changed, 174 insertions(+), 178 deletions(-) (limited to 'checker/inductive.ml') diff --git a/checker/inductive.ml b/checker/inductive.ml index b9964fe6..7a04cbfa 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] then fail(); substl subs ty -let instantiate_partial_params = instantiate_params false - let full_inductive_instantiate mib params sign = let dummy = Prop Null in let t = mkArity (sign,dummy) in @@ -100,10 +96,6 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) = (* Functions to build standard types related to inductive *) - -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: @@ -346,14 +338,14 @@ let type_case_branches env (ind,largs) (p,pj) c = (************************************************************************) -(* Checking the case annotation is relevent *) +(* Checking the case annotation is relevant *) let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if not (eq_ind indsp ci.ci_ind) or (mib.mind_nparams <> ci.ci_npar) or - (mip.mind_consnrealdecls <> ci.ci_cstr_nargs) + (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) (************************************************************************) @@ -404,8 +396,10 @@ type subterm_spec = | Dead_code | Not_subterm -let spec_of_tree t = - if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t) +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 subterm_spec_glb = let glb2 s1 s2 = @@ -440,7 +434,7 @@ let make_renv env minds recarg (kn,tyi) = rel_min = recarg+2; inds = minds; recvec = mind_recvec; - genv = [Lazy.lazy_from_val (Subterm(Large,mind_recvec.(tyi)))] } + genv = [Lazy.lazy_from_val(Subterm(Large,mind_recvec.(tyi)))] } let push_var renv (x,ty,spec) = { renv with @@ -459,10 +453,6 @@ let subterm_var p renv = try Lazy.force (List.nth renv.genv (p-1)) with Failure _ | Invalid_argument _ -> Not_subterm -(* Add a variable and mark it as strictly smaller with information [spec]. *) -let add_subterm renv (x,a,spec) = - push_var renv (x,a,lazy (spec_of_tree (Lazy.force spec))) - let push_ctxt_renv renv ctxt = let n = rel_context_length ctxt in { renv with @@ -478,6 +468,15 @@ let push_fix_renv renv (_,v,_ as recdef) = genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv } +(* Definition and manipulation of the stack *) +type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t + +let push_stack_closures renv l stack = + List.fold_right (fun h b -> (SClosure (renv,h))::b) l stack + +let push_stack_args l stack = + List.fold_right (fun h b -> (SArg h)::b) l stack + (******************************) (* Computing the recursive subterms of a term (propagation of size information through Cases). *) @@ -497,60 +496,38 @@ let lookup_subterms env ind = let (_,mip) = lookup_mind_specif env ind in mip.mind_recargs -(*********************************) - -let match_trees t1 t2 = - let v1 = dest_subterms t1 in - let v2 = dest_subterms t2 in - array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) v1 v2 +let match_inductive ind ra = + match ra with + | (Mrec i | Imbr i) -> eq_ind ind i + | Norec -> false -(* In {match c as z in ind y_s return P with |C_i x_s => t end} - [branches_specif renv c_spec ind] returns an array of x_s specs given - c_spec the spec of c. *) -let branches_specif renv c_spec ind = - let (_,mip) = lookup_mind_specif renv.env ind in +(* In {match c as z in ci y_s return P with |C_i x_s => t end} + [branches_specif renv c_spec ci] returns an array of x_s specs knowing + c_spec. *) +let branches_specif renv c_spec ci = let car = (* We fetch the regular tree associated to the inductive of the match. This is just to get the number of constructors (and constructor arities) that fit the match branches without forcing c_spec. Note that c_spec might be more precise than [v] below, because of nested inductive types. *) + let (_,mip) = lookup_mind_specif renv.env ci.ci_ind in let v = dest_subterms mip.mind_recargs in Array.map List.length v in Array.mapi (fun i nca -> (* i+1-th cstructor has arity nca *) let lvra = lazy (match Lazy.force c_spec with - Subterm (_,t) when match_trees mip.mind_recargs t -> + 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 spec_of_tree 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) - car - -(* Propagation of size information through Cases: if the matched - object is a recursive subterm then compute the information - 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 vlrec = branches_specif renv c_spec ind in - let rec push_branch_args renv lrec c = - match lrec with - ra::lr -> - let c' = whd_betadeltaiota renv.env c in - (match c' with - Lambda(x,a,b) -> - let renv' = push_var renv (x,a,ra) in - push_branch_args renv' lr b - | _ -> (* branch not in eta-long form: cannot perform rec. calls *) - (renv,c')) - | [] -> (renv, c) in - assert (Array.length vlrec = Array.length lbr); - array_map2 (push_branch_args renv) vlrec lbr - + car (* [subterm_specif renv t] computes the recursive structure of [t] and compare its size with the size of the initial recursive argument of @@ -558,78 +535,88 @@ let case_branches_specif renv c_spec ind lbr = about variables. *) -let rec subterm_specif renv t = + +let rec subterm_specif renv stack t = (* maybe reduction is not always necessary! *) let f,l = decompose_app (whd_betadeltaiota renv.env t) in - match f with - | Rel k -> subterm_var k renv - - | Case (ci,_,c,lbr) -> - 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 - 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' = - (* Why Strict here ? To be general, it could also be - Large... *) - assign_var_spec renv' - (nbfix-i, Lazy.lazy_from_val (Subterm(Strict,recargs))) in - let decrArg = recindxs.(i) in - let theBody = bodies.(i) in - let nbOfAbst = decrArg+1 in - let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in - (* pushing the fix parameters *) - let renv'' = push_ctxt_renv renv' sign in - let renv'' = - if List.length l < nbOfAbst then renv'' - else - let theDecrArg = List.nth l decrArg in - let arg_spec = lazy_subterm_specif renv theDecrArg in - assign_var_spec renv'' (1, arg_spec) in - subterm_specif renv'' strippedBody) - - | Lambda (x,a,b) -> - assert (l=[]); - subterm_specif (push_var_renv renv (x,a)) b - - (* Metas and evars are considered OK *) - | (Meta _|Evar _) -> Dead_code - - (* Other terms are not subterms *) - | _ -> Not_subterm - -and lazy_subterm_specif renv t = - lazy (subterm_specif renv t) - -and case_subterm_specif renv ci c lbr = - if Array.length lbr = 0 then [||] - else - let c_spec = lazy_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 = - match subterm_specif renv c with + 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' = + (* Why Strict here ? To be general, it could also be + Large... *) + assign_var_spec renv' + (nbfix-i, lazy (Subterm(Strict,recargs))) in + let decrArg = recindxs.(i) in + let theBody = bodies.(i) in + let nbOfAbst = decrArg+1 in + let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in + (* pushing the fix parameters *) + let stack' = push_stack_closures renv l stack in + let renv'' = push_ctxt_renv renv' sign in + let renv'' = + if List.length stack' < nbOfAbst then renv'' + else + let decrArg = List.nth stack' decrArg in + let arg_spec = stack_element_specif decrArg in + assign_var_spec renv'' (1, arg_spec) in + subterm_specif renv'' [] strippedBody) + + | Lambda (x,a,b) -> + assert (l=[]); + let spec,stack' = extract_stack renv a stack in + subterm_specif (push_var renv (x,a,spec)) stack' b + + (* Metas and evars are considered OK *) + | (Meta _|Evar _) -> Dead_code + + (* Other terms are not subterms *) + | _ -> Not_subterm + +and lazy_subterm_specif renv stack t = + lazy (subterm_specif renv stack t) + +and stack_element_specif = function + |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h + |SArg x -> x + +and extract_stack renv a = function + | [] -> Lazy.lazy_from_val Not_subterm , [] + | h::t -> stack_element_specif h, t + + +(* Check size x is a correct size for recursive calls. *) +let check_is_subterm x = + match Lazy.force x with Subterm (Strict,_) | Dead_code -> true | _ -> false @@ -637,7 +624,7 @@ let check_is_subterm renv c = exception FixGuardError of env * guard_error -let error_illegal_rec_call renv fx arg = +let error_illegal_rec_call renv fx (arg_renv,arg) = let (_,le_vars,lt_vars) = List.fold_left (fun (i,le,lt) sbt -> @@ -647,7 +634,8 @@ let error_illegal_rec_call renv fx arg = | _ -> (i+1, le ,lt)) (1,[],[]) renv.genv in raise (FixGuardError (renv.env, - RecursionOnIllegalTerm(fx,arg,le_vars,lt_vars))) + RecursionOnIllegalTerm(fx,(arg_renv.env, arg), + le_vars,lt_vars))) let error_partial_apply renv fx = raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx)) @@ -659,48 +647,57 @@ let check_one_fix renv recpos def = 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 stack t = (* if [t] does not make recursive calls, it is guarded: *) if noccur_with_meta renv.rel_min nfi t then () else - let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in + let (f,l) = decompose_app (whd_betaiotazeta t) in match f with | 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; + List.iter (check_rec_call renv []) l; (* 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 - if List.length l <= np then error_partial_apply renv glob + let stack' = push_stack_closures renv l stack in + if List.length stack' <= np then error_partial_apply renv glob else (* Check the decreasing arg is smaller *) - let z = List.nth l np in - if not (check_is_subterm renv z) then - error_illegal_rec_call renv glob z + let z = List.nth stack' np in + if not (check_is_subterm (stack_element_specif z)) then + begin match z with + |SClosure (z,z') -> error_illegal_rec_call renv glob (z,z') + |SArg _ -> error_partial_apply renv glob + end end else begin match pi2 (lookup_rel p renv.env) with | None -> - List.iter (check_rec_call renv) l + List.iter (check_rec_call renv []) l | Some c -> - try List.iter (check_rec_call renv) l - with FixGuardError _ -> check_rec_call renv (applist(c,l)) + try List.iter (check_rec_call renv []) l + with FixGuardError _ -> + check_rec_call renv stack (applist(lift p c,l)) end - + | Case (ci,p,c_0,lrest) -> - List.iter (check_rec_call renv) (c_0::p::l); + List.iter (check_rec_call renv []) (c_0::p::l); (* compute the recarg information for the arguments of each branch *) - let lbr = case_subterm_specif renv ci c_0 lrest in - Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr + let case_spec = branches_specif renv + (lazy_subterm_specif renv [] c_0) ci in + let stack' = push_stack_closures renv l 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 (* Enables to traverse Fixpoint definitions in a more intelligent way, ie, the rule : - if - g = Fix g/p := [y1:T1]...[yp:Tp]e & + 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 @@ -710,81 +707,80 @@ let check_one_fix renv recpos def = 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; + 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 - if (List.length l < (decrArg+1)) then - Array.iter (check_rec_call renv') bodies - else + let stack' = push_stack_closures renv l stack in Array.iteri (fun j body -> - if i=j then - let theDecrArg = List.nth l decrArg in - let arg_spec = lazy_subterm_specif renv theDecrArg in - check_nested_fix_body renv' (decrArg+1) arg_spec body - else check_rec_call renv' body) + if i=j && (List.length stack' > decrArg) then + let recArg = List.nth stack' decrArg in + let arg_sp = stack_element_specif recArg in + check_nested_fix_body renv' (decrArg+1) arg_sp body + else check_rec_call renv' [] body) bodies | Const kn -> if evaluable_constant kn renv.env then - try List.iter (check_rec_call renv) l + try List.iter (check_rec_call renv []) l with (FixGuardError _ ) -> - check_rec_call renv(applist(constant_value renv.env kn, l)) - else List.iter (check_rec_call renv) l - - (* The cases below simply check recursively the condition on the - subterms *) - | Cast (a,_, b) -> - List.iter (check_rec_call renv) (a::b::l) + let value = (applist(constant_value renv.env kn, l)) in + check_rec_call renv stack value + else List.iter (check_rec_call renv []) l | Lambda (x,a,b) -> - List.iter (check_rec_call renv) (a::l); - check_rec_call (push_var_renv renv (x,a)) b + assert (l = []); + check_rec_call renv [] a ; + let spec, stack' = extract_stack renv a stack in + check_rec_call (push_var renv (x,a,spec)) stack' b | Prod (x,a,b) -> - List.iter (check_rec_call renv) (a::l); - check_rec_call (push_var_renv renv (x,a)) b + assert (l = [] && stack = []); + check_rec_call renv [] a; + check_rec_call (push_var_renv renv (x,a)) [] b | CoFix (i,(_,typarray,bodies as recdef)) -> - List.iter (check_rec_call renv) l; - Array.iter (check_rec_call renv) typarray; + List.iter (check_rec_call renv []) l; + Array.iter (check_rec_call renv []) typarray; let renv' = push_fix_renv renv recdef in - Array.iter (check_rec_call renv') bodies + Array.iter (check_rec_call renv' []) bodies - | (Ind _ | Construct _ | Sort _) -> - List.iter (check_rec_call renv) l + | (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 + List.iter (check_rec_call renv []) l | Some c -> - try List.iter (check_rec_call renv) l - with (FixGuardError _) -> check_rec_call renv (applist(c,l)) + try List.iter (check_rec_call renv []) l + with (FixGuardError _) -> + check_rec_call renv stack (applist(c,l)) end + | Sort _ -> assert (l = []) + (* l is not checked because it is considered as the meta's context *) | (Evar _ | Meta _) -> () - | (App _|LetIn _) -> assert false (* beta zeta reduction *) + | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then - check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) body + check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body else match body with | Lambda (x,a,b) -> - check_rec_call renv a; + check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in - check_nested_fix_body renv' (decr-1) recArgsDecrArg b + check_nested_fix_body renv' (decr-1) recArgsDecrArg b | _ -> anomaly "Not enough abstractions in fix body" - + in - check_rec_call renv def + check_rec_call renv [] def let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = -- cgit v1.2.3