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(-) 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 a9bc1ac0dc96ca2bf5f33707b2e5b6bdc843b625 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Feb 2019 11:48:23 +0100 Subject: overlay for Equations --- .../user-overlays/09602-gares-more-delta-in-termination-checking.sh | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh diff --git a/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh b/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh new file mode 100644 index 0000000000..18a295cdbb --- /dev/null +++ b/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9602" ] || [ "$CI_BRANCH" = "more-delta-in-termination-checking" ]; then + + equations_CI_REF=more-delta-in-termination-checking + equations_CI_GITURL=https://github.com/gares/Coq-Equations + +fi -- cgit v1.2.3 From f3cb208d3172d0726e18f45a03d0a18dee2b4743 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Feb 2019 13:00:00 +0100 Subject: update CHANGES --- CHANGES.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index c309002beb..e02de0224e 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -48,6 +48,13 @@ Kernel - Added primitive integers +- Unfolding heuristic in termination checking made more complete. + In particular Coq is now more aggressive in unfolding constants + when it looks for a iota redex. Performance regression may occur + in Fixpoint declarations without an explicit {struct} annotation, + since guessing the decreasing argument can now be more expensive. + (PR #9602) + Notations - New command `Declare Scope` to explicitly declare a scope name -- cgit v1.2.3 From abdb6692d8be2250685e4d78cdd84711f4d493d6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Feb 2019 17:47:25 +0100 Subject: add test case for "match" --- test-suite/bugs/closed/bug_9598.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/bug_9598.v diff --git a/test-suite/bugs/closed/bug_9598.v b/test-suite/bugs/closed/bug_9598.v new file mode 100644 index 0000000000..917bf92a87 --- /dev/null +++ b/test-suite/bugs/closed/bug_9598.v @@ -0,0 +1,11 @@ +Module case. + + Inductive pair := K (n1 : nat) (n2 : nat). + Definition fst (p : pair) : nat := match p with K n _ => n end. + + Definition alias_K a b := K a b. + + Fixpoint rec (x : nat) : nat := fst (K 0 (rec x)). + Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)). + +End case. -- 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(-) 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 5ee6581330ac77596d31dddc1bf4fc09e585b1f6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 22 Feb 2019 14:09:43 +0100 Subject: add testcase for fix --- test-suite/bugs/closed/bug_9598.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/test-suite/bugs/closed/bug_9598.v b/test-suite/bugs/closed/bug_9598.v index 917bf92a87..daf4d3f847 100644 --- a/test-suite/bugs/closed/bug_9598.v +++ b/test-suite/bugs/closed/bug_9598.v @@ -9,3 +9,15 @@ Module case. Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)). End case. + +Module fixpoint. + + Inductive pair := K (n1 : nat) (n2 : nat). + Fixpoint fst (p : pair) : nat := match p with K n _ => n end. + + Definition alias_K a b := K a b. + + Fixpoint rec (x : nat) : nat := fst (K 0 (rec x)). + Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)). + +End fixpoint. -- 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(-) 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 From 565cefdb051339a601b9977e163ee4ffbba75274 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 22 Feb 2019 14:10:18 +0100 Subject: add testcase for primitive projection --- test-suite/bugs/closed/bug_9598.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/test-suite/bugs/closed/bug_9598.v b/test-suite/bugs/closed/bug_9598.v index daf4d3f847..00bbfcf5d9 100644 --- a/test-suite/bugs/closed/bug_9598.v +++ b/test-suite/bugs/closed/bug_9598.v @@ -21,3 +21,16 @@ Module fixpoint. Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)). End fixpoint. + +Module primproj. + + Set Primitive Projections. + + Inductive pair := K { fst : nat; snd : nat }. + + Definition alias_K a b := K a b. + + Fixpoint rec (x : nat) : nat := fst (K 0 (rec x)). + Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)). + +End primproj. -- cgit v1.2.3