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.)
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