Quentin VERMANDE (Nov 15 2023 at 10:23): Quentin VERMANDE (Nov 15 2023 at 10:23):Hi. In elpi/coq-lib.elpi, coq.term->gref has a last clause that calls fatal-error-w-data, which breaks what I am currently trying to do since I want to do different things depending on whether my term has a gref head or not. I temporarily added a copy of coq.term->gref that fails silently to proceed with my work, but I am curious to know why this design was chosen (if this is not already documented somewhere) and if there is a standard workaround that does not involve changing coq-elpi's code.
Enrico Tassi (Nov 15 2023 at 10:43):I think both predicates have a place, the one asserting and the one checking (hence failing).
Usually a->b are conversions which do not fail (unless the programmer misuses them).
I'm pretty sure we have term-is-gref? in HB or maybe in TC. The addition to coq-lib would be welcome.
Quentin VERMANDE (Nov 15 2023 at 11:48):Oh, I see, it is in HB, thanks. I guess the whole content of HB/common/stdpp.elpi is meant to be ported back to coq-elpi, does it not?
Cyril Cohen (Nov 15 2023 at 12:02):@Quentin VERMANDE see https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users-.26-devs/topic/.E2.9C.94.20Grafting.20in.20an.20implication/near/397540505
Cyril Cohen (Nov 15 2023 at 12:03):You can add
pred do-not-fail.
:before "term->gref:fail"
coq.term->gref _ _ :- do-not-fail, !, false.
and then call do-not-fail => coq.term->gref X Y.
Enrico Tassi (Nov 15 2023 at 12:44):This also work, but is for black belts ;-)
Yes, the stdpp code should be merged back at some point.
Quentin VERMANDE (Nov 15 2023 at 13:33):Oh, excellent, thanks. If you think I can, I may try to do something about the merging.
Last updated: Oct 13 2024 at 01:02 UTC