From b13e6d67084f7e35595513ffa1045ba6bdccd482 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 19 Feb 2019 14:55:01 +0100 Subject: [kernel] termination checking backtracks on stuck case The strategy is to backtrack when a constant is in head position: we first try to see if the arguments are guarded, if not we unfold. Since `Case` is represented as a head (rather than as a context as the reduction machine does) we did not backtrack there and reduce (including delta) the scrutinized in order to fire the iota redex. This commit adds a choice point in that specific case, and reduces eagerly (not step by step) the scrutinized in case of failure. --- kernel/inductive.ml | 34 ++++++++++++++++++++++++---------- 1 file changed, 24 insertions(+), 10 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 848ae65c51..cbdb393bd7 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -921,16 +921,30 @@ let check_one_fix renv recpos trees def = end | Case (ci,p,c_0,lrest) -> - List.iter (check_rec_call renv []) (c_0::p::l); - (* compute the recarg information for the arguments of - each branch *) - 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 - Array.iteri (fun k br' -> - let stack_br = push_stack_args case_spec.(k) stack' in - check_rec_call renv stack_br br') lrest + begin try + List.iter (check_rec_call renv []) (c_0::p::l); + (* compute the recarg info for the arguments of each branch *) + 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 + lrest |> Array.iteri (fun k br' -> + let stack_br = push_stack_args case_spec.(k) stack' in + check_rec_call renv stack_br br') + with (FixGuardError _ as exn) -> + let exn = CErrors.push exn in + (* we try hard to reduce the match away by looking for a + constructor in c_0 (we unfold definitions too) *) + let c_0 = whd_all renv.env c_0 in + let hd, _ = decompose_app c_0 in + match kind hd with + | Construct _ -> + (* the call to whd_betaiotazeta will reduce the + apparent iota redex away *) + check_rec_call renv [] + (Term.applist (mkCase (ci,p,c_0,lrest), l)) + | _ -> Exninfo.iraise exn + end (* Enables to traverse Fixpoint definitions in a more intelligent way, ie, the rule : -- cgit v1.2.3 From 8785269bb1b514f11bef7a56baeaef0cf3eaa452 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 22 Feb 2019 14:09:30 +0100 Subject: [kernel] termination checking backtracks on stuck fix --- kernel/inductive.ml | 38 ++++++++++++++++++++++++++------------ 1 file changed, 26 insertions(+), 12 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index cbdb393bd7..c0f41d2bc9 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -959,19 +959,33 @@ let check_one_fix renv recpos trees def = 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 stack' = push_stack_closures renv l stack in - Array.iteri - (fun j body -> - if Int.equal 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 + begin try + List.iter (check_rec_call renv []) l; + Array.iter (check_rec_call renv []) typarray; + let renv' = push_fix_renv renv recdef in + let stack' = push_stack_closures renv l stack in + bodies |> Array.iteri (fun j body -> + if Int.equal 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) + with (FixGuardError _ as exn) -> + let exn = CErrors.push exn in + (* we try hard to reduce the fix away by looking for a + constructor in l[decrArg] (we unfold definitions too) *) + if List.length l <= decrArg then Exninfo.iraise exn; + let recArg = List.nth l decrArg in + let recArg = whd_all renv.env recArg in + let hd, _ = decompose_app recArg in + match kind hd with + | Construct _ -> + let before, after = CList.(firstn decrArg l, skipn (decrArg+1) l) in + check_rec_call renv [] + (Term.applist (mkFix ((recindxs,i),recdef), (before @ recArg :: after))) + | _ -> Exninfo.iraise exn + end | Const (kn,_u as cu) -> if evaluable_constant kn renv.env then -- cgit v1.2.3 From 8cad12e0e48eae83773667c2fab7d2570ed43ed2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 22 Feb 2019 14:10:06 +0100 Subject: [kernel] termination checking backtracks on stuck primitive projection --- kernel/inductive.ml | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index c0f41d2bc9..48856c5c0d 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1015,9 +1015,22 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l - | Proj (_p, c) -> - List.iter (check_rec_call renv []) l; - check_rec_call renv [] c + | Proj (p, c) -> + begin try + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + with (FixGuardError _ as exn) -> + let exn = CErrors.push exn in + (* we try hard to reduce the proj away by looking for a + constructor in c (we unfold definitions too) *) + let c = whd_all renv.env c in + let hd, _ = decompose_app c in + match kind hd with + | Construct _ -> + check_rec_call renv [] + (Term.applist (mkProj(Projection.unfold p,c), l)) + | _ -> Exninfo.iraise exn + end | Var id -> begin -- cgit v1.2.3