Enrico Tassi (Oct 20 2021 at 09:40): Enrico Tassi (Oct 20 2021 at 09:40):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?
Pierre-Marie Pédrot (Oct 20 2021 at 09:41):hnf is cbn and refolds, yes
Pierre-Marie Pédrot (Oct 20 2021 at 09:41):it's a weird special case of (weak-head) simpl essentially
Enrico Tassi (Oct 20 2021 at 09:42):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")
Pierre-Marie Pédrot (Oct 20 2021 at 09:42):indeed, for discriminate we shouldn't care about the shape of the arguments
Enrico Tassi (Oct 20 2021 at 09:42):Do you agree?
Pierre-Marie Pédrot (Oct 20 2021 at 09:43):you don't even need the arguments actually, just knowing the head is different should be enough
Pierre-Marie Pédrot (Oct 20 2021 at 09:47):(btw most of the uses of hnf live in ssr, I would recommend seriously reconsidering these uses)
Enrico Tassi (Oct 20 2021 at 10:01):If we bind whd_all as a reduction strategy, then I'm all for it.
Pierre-Marie Pédrot (Oct 20 2021 at 10:02):You mean Reductionops.clos_whd_flags?
Pierre-Marie Pédrot (Oct 20 2021 at 10:02):I was talking about the OCaml implementation of ssr
Enrico Tassi (Oct 20 2021 at 10:07):Oh, let me see (it was used from before the refolding business anyway...)
Enrico Tassi (Oct 20 2021 at 10:08):I mean the kernel one, lazy, not the call-by-name one
Pierre-Marie Pédrot (Oct 20 2021 at 10:08):clos_whd_flags is the kernel reduction
Enrico Tassi (Oct 20 2021 at 10:08):(Eval lazy recurses on arguments)
Enrico Tassi (Oct 20 2021 at 10:08):ok then
Pierre-Marie Pédrot (Oct 20 2021 at 10:09):you have to be careful that sometimes refolding makes sense
Last updated: Oct 13 2024 at 01:02 UTC