Apparently discriminate calls
hnf to expose (different constructors) on both sides, but recent changes in
ret.v made this reduction overly expensive.
lazy for example is fast, but
hnf horrible. IIRC @Maxime Dénès did inverstigate hnf before. Is it using the refolding thingy? It is using the call-by-name?
hnf is cbn and refolds, yes
it's a weird special case of (weak-head) simpl essentially
I have the impression that there is no gain in calling
hnf if the user explicitly calls
discriminate (instead of
injection in which case one may want arguments to stay "nice")
indeed, for discriminate we shouldn't care about the shape of the arguments
Do you agree?
you don't even need the arguments actually, just knowing the head is different should be enough
(btw most of the uses of hnf live in ssr, I would recommend seriously reconsidering these uses)
If we bind
whd_all as a reduction strategy, then I'm all for it.
You mean Reductionops.clos_whd_flags?
I was talking about the OCaml implementation of ssr
Oh, let me see (it was used from before the refolding business anyway...)
I mean the kernel one, lazy, not the call-by-name one
clos_whd_flags is the kernel reduction
(Eval lazy recurses on arguments)
you have to be careful that sometimes refolding makes sense
Last updated: Jan 29 2023 at 19:02 UTC