Stream: math-comp users

Topic: hnf & discriminate


view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 09:41):

hnf is cbn and refolds, yes

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 09:41):

it's a weird special case of (weak-head) simpl essentially

view this post on Zulip 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")

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 09:42):

indeed, for discriminate we shouldn't care about the shape of the arguments

view this post on Zulip Enrico Tassi (Oct 20 2021 at 09:42):

Do you agree?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Oct 20 2021 at 10:01):

If we bind whd_all as a reduction strategy, then I'm all for it.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 10:02):

You mean Reductionops.clos_whd_flags?

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 10:02):

I was talking about the OCaml implementation of ssr

view this post on Zulip Enrico Tassi (Oct 20 2021 at 10:07):

Oh, let me see (it was used from before the refolding business anyway...)

view this post on Zulip Enrico Tassi (Oct 20 2021 at 10:08):

I mean the kernel one, lazy, not the call-by-name one

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 10:08):

clos_whd_flags is the kernel reduction

view this post on Zulip Enrico Tassi (Oct 20 2021 at 10:08):

(Eval lazy recurses on arguments)

view this post on Zulip Enrico Tassi (Oct 20 2021 at 10:08):

ok then

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 10:09):

you have to be careful that sometimes refolding makes sense


Last updated: Jan 29 2023 at 19:02 UTC