Gordon Stewart (Jan 25 2022 at 15:36): Gordon Stewart (Jan 25 2022 at 15:36):Though now I see above that you're reluctant to add functors :-) https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users.20.26.20devs/topic/Opaque.20bodies/near/263258676. It seems like they'd be useful to support certain patterns in large developments (I can expand on that if desired). I'm interested to better understand the reasons not to add them.
Enrico Tassi (Jan 25 2022 at 17:56):I will look at the code in the other thread tomorrow, but I can clarify why I'm reluctant. I think I've been quite inaccurate in my discussion with @Jason Gross so this is the occasion to explain the problems I see. Implementing functors means two things for me:
Enrico Tassi (Jan 25 2022 at 17:58):I've nothing against the former, hence I'll look at your code and help you.
Enrico Tassi (Jan 25 2022 at 18:08):Putting code inside a functor can happen in two ways, either by defining a command/tactic inside the functor (I see no real use case for this) or by running some code inside the functor (code which uses the API coq.elpi.accumulate). Imagine the functor defines an inductive and you Elpi derive stuff on it, elpi would put in one database a piece of elpi code which relates the type with, say, the equality test. At functor instantiation time one would need to apply a coq-term-substitution to some elpi code. This is not implemented yes, and not super trivial either. One reason, which is fixable with some work, is that elpi (not coq-elpi) does not have an API to manipulate "compilation units", see https://github.com/LPCIC/elpi/blob/ad3a854c4f137e4bb132e3d967eb3ea5dd95e280/src/API.mli#L175 . The other is that I'm not so sure that doing the obvious substitution would result in code which still works as the programmer expects (since functor parameters are just constants, like usual constants.. .maybe an API to distinguish them is enough to let the programmer make is code robust in face of substitution... I don't really have enough experience here, so maybe I'm overcautious).
Last updated: Oct 13 2024 at 01:02 UTC