diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 33 |
1 files changed, 10 insertions, 23 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index bce56d6170..8962fa9a92 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -763,6 +763,7 @@ let get_codomain_spec env p = let env' = push_rel_context pctx env in if is_arity env' pr then let specs = Array.map (family_codomain_spec env) lbr in + (* What if the specs correspond to different inductive families? *) Array.fold_left family_spec_glb (None, Dead_code) specs else None, Not_subterm | _ -> None, Not_subterm @@ -882,50 +883,36 @@ let error_illegal_rec_call renv fx (arg_renv,arg) = let error_partial_apply renv fx = raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx)) -let rec filter_stack_domain env p stack = - let reset_stack stack = - (* TODO: is it correct to empty the stack instead? *) - List.fold_right (fun _ l -> (None, SArg (lazy Not_subterm)) :: l) stack [] - in +let filter_stack_domain env ci p stack = let absctx, ar = dest_lam_assum env p in let env = push_rel_context absctx env in let rec filter_stack env ar stack = let t = whd_betadeltaiota env ar in match stack, kind_of_term t with - | (oind,elt) :: stack', Prod (n,a,c0) -> + | elt :: stack', Prod (n,a,c0) -> let d = (n,None,a) in let ty, args = decompose_app a in (* TODO: reduce a? *) let elt = match kind_of_term ty with - | Ind ind when oind = None || Option.equal eq_ind (Some ind) oind -> + | Ind ind -> let spec' = stack_element_specif elt in (* TODO: this is recomputed each time*) (match (Lazy.force spec') with (* TODO: are we forcing too much? *) - | Not_subterm -> (Some ind, elt) + | Not_subterm -> elt | Subterm(s,path) -> let recargs = get_recargs_approx env ind args in let path = inter_wf_paths path recargs in - (Some ind, SArg (lazy (Subterm(s,path))))) + SArg (lazy (Subterm(s,path)))) (* TODO: not really an SArg *) (* TODO: what if Dead_code above? *) - | _ -> (None, SArg (lazy Not_subterm)) (* We could accept match here too *) + | _ -> (SArg (lazy Not_subterm)) in elt :: filter_stack (push_rel d env) c0 stack' - | _, Case (ci,p,c,lbr) -> - let pctx, pr = dest_lam_assum env p in - let env' = push_rel_context pctx env in - if is_arity env' pr then - Array.fold_left (fun stack ar -> filter_stack_domain env ar stack) stack lbr - (* What if the specs correspond to different inductive families? *) - else reset_stack stack | [], _ -> [] (* TODO: remove after debugging *) - | _,_ -> reset_stack stack + | _,_ -> List.fold_right (fun _ l -> SArg (lazy Not_subterm) :: l) stack [] + (* TODO: is it correct to empty the stack instead? *) in filter_stack env ar stack -let filter_stack_domain env p stack = - let stack = List.map (fun spec -> (None, spec)) stack in - List.map snd (filter_stack_domain env p stack) - (* Check if [def] is a guarded fixpoint body with decreasing arg. given [recpos], the decreasing arguments of each mutually defined fixpoint. *) @@ -981,7 +968,7 @@ let check_one_fix renv recpos trees 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 p 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 |