Janno (Jul 10 2020 at 12:49): 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?
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
Janno (Jul 10 2020 at 13:04):Okay, that's exactly what I do. Thanks!
Janno (Jul 10 2020 at 13:05):Oh, wait, you are not quoting an existing function, are you?
Gaëtan Gilbert (Jul 10 2020 at 13:09):Janno said:
Oh, wait, you are not quoting an existing function, are you?
correct
Janno (Jul 10 2020 at 13:19):But is it a good idea to do it this way? :)
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
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.
Gaëtan Gilbert (Jul 10 2020 at 13:35):If you have a call to reduction why do you need the check?
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..
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
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: Apr 19 2024 at 20:01 UTC