From 871484af30e0a515c07c81bb59b8f8cb3c93c92d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 10 Jan 2024 14:51:29 +0100 Subject: [PATCH] Revert "Followup of #17993, fixes #18239: anomaly on triggering conditions for simpl." This reverts commit b789f40f7616e3a159b43356cb314ff53e329fc9. --- pretyping/tacred.ml | 45 ++++++++++------------- test-suite/success/simpl.v | 75 -------------------------------------- 2 files changed, 19 insertions(+), 101 deletions(-) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 76ddeb5d1729..e3907762a5ff 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -233,7 +233,7 @@ let compute_fix_reversibility sigma labs args fix = labs; typed_reversible_args, nlam, nargs -let check_fix_reversibility env sigma ref u labs args minarg refs ((lv,i),_ as fix) = +let check_fix_reversibility env sigma ref u labs args refs ((lv,i),_ as fix) = let li, nlam, nargs = compute_fix_reversibility sigma labs args (mkFix fix) in let k = lv.(i) in let refolding_data = { @@ -247,13 +247,13 @@ let check_fix_reversibility env sigma ref u labs args minarg refs ((lv,i),_ as f EliminationFix (n-p+1,(li,n)) *) EliminationFix { - trigger_min_args = max minarg nlam; + trigger_min_args = nlam; refolding_target = ref; refolding_data; } else EliminationFix { - trigger_min_args = max minarg (nlam - nargs + k + 1); + trigger_min_args = nlam - nargs + k + 1; refolding_target = ref; refolding_data; } @@ -305,49 +305,42 @@ let deactivate_delta allowed_reds = (* Act both on Delta and transparent state as not all reduction functions work the same *) RedFlags.(red_add_transparent (red_sub allowed_reds fDELTA) TransparentState.empty) -(* [compute_consteval] stepwise expands an arbitrary long sequence of - reversible constants, eventually refolding to the initial constant - for unary fixpoints and to the last constant encapsulating the Fix - for mutual fixpoints *) +(* [compute_consteval] expands and refolds an arbitrary long sequence + of reversible constants for unary fixpoints but consider the last + constant before revealing a Fix if the latter is mutually defined *) let compute_consteval allowed_reds env sigma ref u = let allowed_reds_no_delta = deactivate_delta allowed_reds in - let rec srec env all_abs lastref lastu onlyproj c = - let c', args = whd_stack_gen allowed_reds_no_delta env sigma c in - (* We now know that the initial [ref] evaluates to [fun all_abs => c' args] *) - (* and that the last visited name in the evaluation is [lastref] *) + let rec srec env n labs lastref lastu onlyproj c = + let c',l = whd_stack_gen allowed_reds_no_delta env sigma c in match EConstr.kind sigma c' with - | Lambda (id,t,g) when not onlyproj -> - assert (List.is_empty args); + | Lambda (id,t,g) when List.is_empty l && not onlyproj -> let open Context.Rel.Declaration in - srec (push_rel (LocalAssum (id,t)) env) (t::all_abs) lastref lastu onlyproj g + srec (push_rel (LocalAssum (id,t)) env) (n+1) (t::labs) lastref lastu onlyproj g | Fix ((lv,i),(names,_,_) as fix) when not onlyproj -> - let n_all_abs = List.length all_abs in let nbfix = Array.length lv in (if nbfix = 1 then - (* Try to refold to [ref] *) let names = [|Some (ref,u)|] in - try check_fix_reversibility env sigma ref u all_abs args n_all_abs names fix + try check_fix_reversibility env sigma ref u labs l names fix with Elimconst -> NotAnElimination else - (* Try to refold to [lastref] *) - let last_labs, last_args, names = invert_names allowed_reds env sigma lastref lastu names i in - try check_fix_reversibility env sigma lastref lastu last_labs last_args n_all_abs names fix + let labs, l, names = invert_names allowed_reds env sigma lastref lastu names i in + try check_fix_reversibility env sigma lastref lastu labs l names fix with Elimconst -> NotAnElimination) - | Case (_,_,_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases (List.length all_abs) - | Case (_,_,_,_,_,d,_) -> srec env all_abs lastref lastu true d - | Proj (p, _, d) when isRel sigma d -> EliminationProj (List.length all_abs) + | Case (_,_,_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n + | Case (_,_,_,_,_,d,_) -> srec env n labs lastref lastu true d + | Proj (p, _, d) when isRel sigma d -> EliminationProj n | _ when isTransparentEvalRef env sigma (RedFlags.red_transparent allowed_reds) c' -> - (* Continue stepwise unfolding from [c' args] *) + (* Forget all \'s and args and do as if we had started with c' *) let ref, u = destEvalRefU sigma c' in (match reference_opt_value env sigma ref u with | None -> NotAnElimination (* e.g. if a rel *) - | Some c -> srec env all_abs ref u onlyproj (applist (c, args))) + | Some c -> srec env n labs ref u onlyproj (applist (c,l))) | _ -> NotAnElimination in match reference_opt_value env sigma ref u with | None -> NotAnElimination - | Some c -> srec env [] ref u false c + | Some c -> srec env 0 [] ref u false c let reference_eval allowed_reds env sigma ref u = match ref with diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v index 03f46046cc48..6faf3f026970 100644 --- a/test-suite/success/simpl.v +++ b/test-suite/success/simpl.v @@ -189,78 +189,3 @@ match goal with [ |- g a c n = g a c n ] => idtac end. Abort. End WithLetMutual. - -Module IotaTrigger1. - -Definition a x := match x with true => tt | false => tt end. -Definition b x (y : unit) := a x. -Definition c x := b x tt. -Goal a true = tt. simpl. match goal with [ |- tt = tt ] => idtac end. Abort. -Goal b true = fun _ => tt. simpl. match goal with [ |- b true = _ ] => idtac end. Abort. -Goal c true = tt. simpl. match goal with [ |- tt = tt ] => idtac end. Abort. - -End IotaTrigger1. - -Module IotaTrigger2. - -Definition a x := match x with true => fun _ => tt | false => fun _ => tt end tt. -Definition b x (y : unit) := a x. -Definition c x := b x tt. -Goal a true = tt. simpl. match goal with [ |- tt = tt ] => idtac end. Abort. -Goal b true = fun _ => tt. simpl. match goal with [ |- b true = _ ] => idtac end. Abort. -Goal c true = tt. simpl. match goal with [ |- tt = tt ] => idtac end. Abort. - -End IotaTrigger2. - -Module IotaTrigger3. - -Fixpoint f_fix_fun n := match n with 0 => fun _ : unit => true | S n => f_fix_fun n end. -Definition test_fix_fun n := f_fix_fun n. -Goal test_fix_fun 2 = fun _ => true. simpl. match goal with [ |- (fun _ => true) = _ ] => idtac end. Abort. -Goal forall x, test_fix_fun (S x) = fun _ => true. intro. simpl. match goal with [ |- test_fix_fun x = _ ] => idtac end. Abort. -(* REDUCED *) - -Definition test_fix_fun_partial n (x:unit) := f_fix_fun n. -Goal test_fix_fun_partial 2 = fun _ _ => true. simpl. match goal with [ |- test_fix_fun_partial 2 = _ ] => idtac end. Abort. -Goal forall x, test_fix_fun_partial (S x) = fun _ _ => true. intro. simpl. match goal with [ |- test_fix_fun_partial (S x) = _ ] => idtac end. Abort. -(* NOT REDUCED: design choice that it is not enough fully applied to trigger the reduction *) -(* remark: the presence of an inner "fun" does not matter *) - -Fixpoint f_fix n := match n with 0 => fun _ : unit => true | S n => f_fix n end. -Definition test_fix n := f_fix n tt. -Goal test_fix 2 = true. simpl. match goal with [ |- test_fix 2 = _ ] => idtac end. Abort. -Goal forall x, test_fix (S x) = true. intro. simpl. match goal with [ |- test_fix (S x) = _ ] => idtac end. Abort. -(* NOT REDUCED: design choice that we couldn't refold to test_fix after reduction *) - -Fixpoint f_mutual_fix n := match n with 0 => true | S n => g n end -with g n := match n with 0 => true | S n => f_mutual_fix n end. -Definition test_mutual_fix n := f_mutual_fix n. -Goal test_mutual_fix 2 = true. simpl. match goal with [ |- true = _ ] => idtac end. Abort. -Goal forall x, test_mutual_fix (S x) = true. intro. simpl. match goal with [ |- g x = _ ] => idtac end. Abort. -(* REDUCED: design choice that mutual fixpoints refold to last encapsulating name *) - -Definition test_mutual_fix_partial n (x:unit) := f_mutual_fix n. -Goal test_mutual_fix_partial 2 = fun _ => true. simpl. match goal with [ |- test_mutual_fix_partial 2 = _ ] => idtac end. Abort. -Goal forall x, test_mutual_fix_partial (S x) = fun _ => true. intro. simpl. match goal with [ |- test_mutual_fix_partial (S x) = _ ] => idtac end. Abort. -(* NOT REDUCED: design choice that it is not enough fully applied to trigger the reduction *) -(* Moreover, was failing between #17993 and #18243 (see #18239) *) - -Fixpoint f_mutual_fix_cut n := match n with 0 => fun _ : unit => true | S n => g_cut n end -with g_cut n := match n with 0 => fun _ : unit => true | S n => f_mutual_fix_cut n end. -Definition test_mutual_fix_cut n := f_mutual_fix_cut n tt. -Goal test_mutual_fix_cut 2 = true. simpl. match goal with [ |- true = _ ] => idtac end. Abort. -Goal forall x, test_mutual_fix_cut (S x) = true. intro. simpl. match goal with [ |- g_cut x tt = _ ] => idtac end. Abort. -(* REDUCED: by consistency with test_mutual_fix, which itself already differs from the case of a unary fix (new behavior from #18243) *) - -Definition test_mutual_fix_cut_partial n (x:unit) := f_mutual_fix_cut n x. -Goal test_mutual_fix_cut_partial 2 = fun _ => true. simpl. match goal with [ |- test_mutual_fix_cut_partial 2 = _ ] => idtac end. Abort. -Goal forall x, test_mutual_fix_cut_partial (S x) = fun _ => true. intro. simpl. match goal with [ |- test_mutual_fix_cut_partial (S x) = _ ] => idtac end. Abort. -(* NOT REDUCED: by consistency with test_fix_fun_partial and test_mutual_fix_cut_partial *) -(* Moreover was failing before #18243 (see #18239) *) - -Definition f_case n := match n with 0 => fun _ : unit => true | S n => fun _ => true end. -Definition test_case n := f_case n tt. -Goal test_case 2 = true. simpl. match goal with [ |- true = _ ] => idtac end. Abort. -(* REDUCED *) - -End IotaTrigger3.