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?
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
Okay, that's exactly what I do. Thanks!
Oh, wait, you are not quoting an existing function, are you?
Janno said:
Oh, wait, you are not quoting an existing function, are you?
correct
But is it a good idea to do it this way? :)
If the term is unreduced it will do arbitrary amounts of work only to throw it away so it's not great
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.
If you have a call to reduction why do you need the check?
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..
If you're testing to know if you need to reduce, you should probably just reduce
Ah, no, I am testing to see if I am stuck to avoid endlessly (not) reducing the same term.
Last updated: Dec 05 2023 at 04:01 UTC