Stream: Coq devs & plugin devs

Topic: Detecting stuckness in CClosure reduction


view this post on Zulip Janno (Jul 10 2020 at 12:49):

What's the best way to check if a term has been reduced by CClosure reduction (whd_stack in my specific case)? I am using Constr.equal now and that seems to work for the one example I have. Is it a good solution in general?

view this post on Zulip Gaëtan Gilbert (Jul 10 2020 at 12:55):

What do you mean "using constr.equal"? like

let is_reduced env c =
  let c' = Reduction.whd_all env c in
  Constr.equal c c'

? although that's whd_all not _stack

view this post on Zulip Janno (Jul 10 2020 at 13:04):

Okay, that's exactly what I do. Thanks!

view this post on Zulip Janno (Jul 10 2020 at 13:05):

Oh, wait, you are not quoting an existing function, are you?

view this post on Zulip Gaëtan Gilbert (Jul 10 2020 at 13:09):

Janno said:

Oh, wait, you are not quoting an existing function, are you?

correct

view this post on Zulip Janno (Jul 10 2020 at 13:19):

But is it a good idea to do it this way? :)

view this post on Zulip Gaëtan Gilbert (Jul 10 2020 at 13:28):

If the term is unreduced it will do arbitrary amounts of work only to throw it away so it's not great

view this post on Zulip Janno (Jul 10 2020 at 13:32):

Well, in my case I do the check after a call to reduction that is required either way. I am more worried about the use of Constr.equal since I don't know what could go wrong there.

view this post on Zulip Gaëtan Gilbert (Jul 10 2020 at 13:35):

If you have a call to reduction why do you need the check?

view this post on Zulip Janno (Jul 10 2020 at 14:28):

Because the result of reduction is given to a recursive call that will end up in the same place. I suppose one could rewrite the whole thing to do it differently (and previous versions did do it differently) but this has been the most maintainable version of the code so far. I could probably add a flag that says "previously reduced, don't reduce again". That might work..

view this post on Zulip Gaëtan Gilbert (Jul 10 2020 at 15:21):

If you're testing to know if you need to reduce, you should probably just reduce

view this post on Zulip Janno (Jul 10 2020 at 15:34):

Ah, no, I am testing to see if I am stuck to avoid endlessly (not) reducing the same term.


Last updated: Oct 16 2021 at 02:03 UTC