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.)
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: Dec 05 2023 at 12:01 UTC