Add head reduction flags (`lazy head beta` etc) #17503

SkySkimmer · 2023-04-18T14:02:37Z

NB: the cbv code doesn't seem to have a weak mode (I guess it would
just mean not reducing under binders).

Overlays:

Adapt to coq/coq#17503 (raw/glob_red_expr moved) ejgallego/coq-serapi#360

SkySkimmer · 2023-04-18T14:03:33Z

@coqbot run full ci

jfehrle

Some suggestions. Would be good to add the index entries.

doc/tools/docgram/orderedGrammar

doc/sphinx/proofs/writing-proofs/equality.rst

JasonGross

This is great, thank you!

I would also be quite interested in modifiers that meant "don't go underneath lambdas". Should I open a separate issue for that?

JasonGross · 2023-04-18T19:55:51Z

test-suite/output/reduction.v

@@ -11,3 +11,6 @@ Eval simpl in (fix plus (n m : nat) {struct n} : nat :=

 Eval hnf in match (plus (S n) O) with S n => n | _ => O end.

+Eval weak simpl in 2 + 2.


Please also test 2 + (2 + 2) (behavior on terms with non-normal arguments) and hold (fun x => 1 + x)forAxiom hold : forall {T}, T.` (when the arguments to the whnf have lambdas)

SkySkimmer · 2023-04-18T20:02:20Z

If we want to add modifiers we should probably not go with this syntax and instead put the modifiers among the flags (beta etc)
The situation for simpl with flags is kinda strange btw, it ignores the flags unless simpliscbn AFAICT

JasonGross · 2023-04-18T23:55:56Z

If we want to add modifiers we should probably not go with this syntax and instead put the modifiers among the flags (beta etc)

I'd be fine with weak meaning the thing in this PR for lazy, cbn, and simpl, and meaning "don't go under binders" for cbv, vm_compute and native_compute.

jfehrle · 2023-04-19T00:02:36Z

I'd be fine with weak meaning the thing in this PR for lazy, cbn, and simpl, and meaning "don't go under binders" for cbv, vm_compute and native_compute.

Only if we document the behavior/differences!

SkySkimmer · 2023-04-19T11:22:27Z

I'd be fine with weak meaning the thing in this PR for lazy, cbn, and simpl, and meaning "don't go under binders" for cbv, vm_compute and native_compute.

But "go in subterms but not under binders" is also meaningful for cbn & co.

JasonGross · 2023-04-19T23:52:29Z

I'd be fine with weak meaning the thing in this PR for lazy, cbn, and simpl, and meaning "don't go under binders" for cbv, vm_compute and native_compute.

But "go in subterms but not under binders" is also meaningful for cbn & co.

That's true. But it's also the natural meaning of "weak" for cbv ("stop once you're guaranteed that there can be no more redexs in the head position"). But in any case, I care more about having the functionality at all than about what the syntax is. And I support merging this PR with the current syntax. (Though I do think it'd be cleaner overall to have two flags instead of prefixes, one for "stop when there are guaranteed to be no redexs in the head position", and another for "do not traverse into the bodies of lambdas/Pis".)

ppedrot · 2023-04-24T16:07:18Z

Related to the flag discussion, I'm not a huge fan of adding non-identifiers in the list of reductions, since this easily causes mayhem with parsing (think about future parsing extensions). If not a flag, this should rather be called weak_cbn or something similar as a single ident.

SkySkimmer · 2023-04-27T14:32:26Z

weak was the wrong term, it should have been head. Now changed.
Also changed to use the regular postfix flag system instead of a special prefix.

herbelin · 2023-10-22T20:30:45Z

OK if you insist. Then how to proceed? You fix the ll of contextualize and update the serapi orverlay, then I merge?

herbelin

OK to me.

Note that the following will later have to be done:

weak cbv (but Support for weak cbv #18190 will do)
support for the head flag at the syntax level in Ltac2

Regarding terminology: head looks good because more intuitive than weak-head (e.g. using the word whd would have looked a bit jargon).

herbelin · 2023-10-22T20:48:15Z

Also: will it be "acceptable practice" that the weak cbv PR modifies the change log of this PR?

Added: I guess so.

SkySkimmer · 2023-10-24T12:19:25Z

@coqbot ci minimize ci-analysis

coqbot-app · 2023-10-24T12:19:30Z

I am now running minimization at commit 6bbecf5 on requested target ci-analysis. I'll come back to you with the results once it's done.

JasonGross · 2023-10-24T23:32:11Z

I expect the minimization will not go anywhere without help; the file takes 10s to run and is 3700loc...

SkySkimmer · 2023-10-25T12:14:11Z

Looks like it was a temporary problem anyway, probably some incompatible mathcomp change.

SkySkimmer · 2023-10-25T12:14:38Z

@herbelin this should be ready to merge

herbelin · 2023-10-25T17:16:28Z

@coqbot: merge now (finally!)

coqbot-app · 2023-10-25T17:16:31Z

@herbelin: Please take care of the following overlays:

17503-SkySkimmer-redexpr.sh

Adapt to coq/coq#17503 (raw/glob_red_expr moved)

SkySkimmer requested review from a team as code owners April 18, 2023 14:02

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Apr 18, 2023

SkySkimmer mentioned this pull request Apr 18, 2023

Feature Request: variant of hnf that runs on reduction engines other than simpl #13881

Closed

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Apr 18, 2023

jfehrle mentioned this pull request Apr 18, 2023

Support multiple :name:s with multiple signatures for .. tacn:: #17507

Closed

jfehrle reviewed Apr 18, 2023

View reviewed changes

doc/tools/docgram/orderedGrammar Outdated Show resolved Hide resolved

doc/sphinx/proofs/writing-proofs/equality.rst Outdated Show resolved Hide resolved

JasonGross approved these changes Apr 18, 2023

View reviewed changes

JasonGross reviewed Apr 18, 2023

View reviewed changes

SkySkimmer added needs: progress Work in progress: awaiting action from the author. needs: test-suite update Test case should be added to / updated in the test-suite. labels Apr 19, 2023

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Apr 25, 2023

SkySkimmer force-pushed the redexpr branch from 6d317ab to b411b87 Compare April 27, 2023 14:30

coqbot-app bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Apr 27, 2023

SkySkimmer changed the title ~~Add weak reductions: weak lazy weak cbn weak simpl~~ Add head reduction flags (lazy head beta etc) Apr 27, 2023

SkySkimmer removed needs: progress Work in progress: awaiting action from the author. needs: test-suite update Test case should be added to / updated in the test-suite. labels Apr 27, 2023

herbelin approved these changes Oct 22, 2023

View reviewed changes

herbelin self-assigned this Oct 22, 2023

SkySkimmer added 4 commits October 24, 2023 10:05

Move raw and glob red expr type definitions to genredexpr

c3f33ee

Remove legacy let head_style = false in redexpr

3ec3124

Add head reduction flags (lazy head beta etc)

be092c0

Overlays for head reduction flag PR

6bbecf5

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 24, 2023

SkySkimmer force-pushed the redexpr branch from adaa829 to 6bbecf5 Compare October 24, 2023 08:07

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 24, 2023

SkySkimmer added the needs: fixing The proposed code change is broken. label Oct 24, 2023

This comment was marked as outdated.

Sign in to view

SkySkimmer removed the needs: fixing The proposed code change is broken. label Oct 25, 2023

coqbot-app bot merged commit f2e9235 into coq:master Oct 25, 2023
9 of 11 checks passed

herbelin added the part: reduction strategies The Strategy command for defining reduction straegies. label Oct 25, 2023

SkySkimmer mentioned this pull request Oct 25, 2023

Ltac2 should support weak reduction flag #18209

Closed

ejgallego added a commit to ejgallego/coq-serapi that referenced this pull request Oct 25, 2023

Merge pull request #360 from SkySkimmer/redexpr

3673c01

Adapt to coq/coq#17503 (raw/glob_red_expr moved)

SkySkimmer deleted the redexpr branch October 26, 2023 11:23

herbelin mentioned this pull request Feb 25, 2024

cbv performs a strong reduction #1992

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add head reduction flags (`lazy head beta` etc) #17503

Add head reduction flags (`lazy head beta` etc) #17503

SkySkimmer commented Apr 18, 2023 •

edited

SkySkimmer commented Apr 18, 2023

jfehrle left a comment

JasonGross left a comment

JasonGross Apr 18, 2023

SkySkimmer commented Apr 18, 2023

JasonGross commented Apr 18, 2023

jfehrle commented Apr 19, 2023

SkySkimmer commented Apr 19, 2023

JasonGross commented Apr 19, 2023

ppedrot commented Apr 24, 2023

SkySkimmer commented Apr 27, 2023

herbelin commented Oct 22, 2023

herbelin left a comment •

edited

herbelin commented Oct 22, 2023 •

edited

SkySkimmer commented Oct 24, 2023

coqbot-app bot commented Oct 24, 2023

This comment was marked as outdated.

This comment was marked as outdated.

JasonGross commented Oct 24, 2023

This comment was marked as outdated.

This comment was marked as outdated.

SkySkimmer commented Oct 25, 2023

SkySkimmer commented Oct 25, 2023

herbelin commented Oct 25, 2023

coqbot-app bot commented Oct 25, 2023

		@@ -11,3 +11,6 @@ Eval simpl in (fix plus (n m : nat) {struct n} : nat :=

		Eval hnf in match (plus (S n) O) with S n => n \| _ => O end.

		Eval weak simpl in 2 + 2.

Add head reduction flags (lazy head beta etc) #17503

Add head reduction flags (lazy head beta etc) #17503

Conversation

SkySkimmer commented Apr 18, 2023 • edited

SkySkimmer commented Apr 18, 2023

jfehrle left a comment

Choose a reason for hiding this comment

JasonGross left a comment

Choose a reason for hiding this comment

JasonGross Apr 18, 2023

Choose a reason for hiding this comment

SkySkimmer commented Apr 18, 2023

JasonGross commented Apr 18, 2023

jfehrle commented Apr 19, 2023

SkySkimmer commented Apr 19, 2023

JasonGross commented Apr 19, 2023

ppedrot commented Apr 24, 2023

SkySkimmer commented Apr 27, 2023

herbelin commented Oct 22, 2023

herbelin left a comment • edited

Choose a reason for hiding this comment

herbelin commented Oct 22, 2023 • edited

SkySkimmer commented Oct 24, 2023

coqbot-app bot commented Oct 24, 2023

This comment was marked as outdated.

This comment was marked as outdated.

JasonGross commented Oct 24, 2023

This comment was marked as outdated.

This comment was marked as outdated.

SkySkimmer commented Oct 25, 2023

SkySkimmer commented Oct 25, 2023

herbelin commented Oct 25, 2023

coqbot-app bot commented Oct 25, 2023

Add head reduction flags (`lazy head beta` etc) #17503

Add head reduction flags (`lazy head beta` etc) #17503

SkySkimmer commented Apr 18, 2023 •

edited

herbelin left a comment •

edited

herbelin commented Oct 22, 2023 •

edited