Skip to content

Commit

Permalink
Revert "Followup of coq#17993, fixes coq#18239: anomaly on triggering…
Browse files Browse the repository at this point in the history 
… conditions for simpl."

This reverts commit b789f40.
  • Loading branch information
@SkySkimmer
SkySkimmer committed Jan 10, 2024
1 parent db93e18 commit 871484a
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 101 deletions.
45 changes: 19 additions & 26 deletions pretyping/tacred.ml
View file
Expand Up @@ -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 = {
Expand All @@ -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;
}
Expand Down Expand Up @@ -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
Expand Down
75 changes: 0 additions & 75 deletions test-suite/success/simpl.v
View file
Expand Up @@ -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.

0 comments on commit 871484a

Please sign in to comment.