Stream: Coq devs & plugin devs

Topic: `Reduction.whd_all`


view this post on Zulip Jason Gross (Apr 07 2023 at 07:29):

Does Reduction.whd_all do fixpoint refolding? And is there a variant of Reduction.whd_all that does not do fixpoint refolding and will also fully reduce fixpoints in the head position? That is, I want List.map f (x :: y :: z :: []) to become f x :: f y :: f z :: [], not f x :: <unfolded fixpoint of List.map> f (y :: z :: []). (I ask because MetaCoq uses Reduction.whd_all on every step of the TemplateMonad, and I suspect it's responsible for some performance bottlenecks, though I haven't managed to profile the code.)

view this post on Zulip Hugo Herbelin (Apr 07 2023 at 08:57):

Does Reduction.whd_all do fixpoint refolding?

Not to my knowledge (though it would be nice at some time that globally named fixpoints are kernel-wise refolded, I would say).

And is there a variant of Reduction.whd_all that [..] will also fully reduce fixpoints in the head position?

Do you really mean in the head position or, as in your example, recursively on subterms of the form ... :: ...?

In head position, whd_all should continue to reduce, and, otherwise, there is Reductionops.nf_all (using call-by-need reduction).


Last updated: Oct 13 2024 at 01:02 UTC