Stream: Elpi users & devs

Topic: ✔ Generating terms via ltac in an [Elpi Command]


view this post on Zulip Jasper Haag (Jan 25 2022 at 20:40):

I'm building an Elpi Command which is intended to construct a module containing definitions/lemmas/instances, and I'm running into some issues with building the body of the EqDecision instance. In particular, the following:

...
std.assert-ok! (coq.elaborate-skeleton {{ EqDecision lp:CarrierTerm }} _ ElaboratedEqDecisionTy) "whoops",
Term = {{ ltac:(solve_decision) : lp:ElaboratedEqDecisionTy }}

fails with the following error:

Error: Not Yet Implemented: (glob)HOAS for GHole

My next thought was to construct a (sealed-)goal of the appropriate form so that I can coq.ltac.call "solve_decision" [] in order to generate the term that I want. However, I can't seem to construct the appropriate goal on-the-fly within the context of an Elpi Command; using coq.ltac.call ... within the solve clause of an Elpi Tactic indeed works, so I suspect that I'm just not generating the appropriate goal (or the appropriate connection between Coq/Elpi states).

Am I on the right track w.r.t generating an EqDecision term in an Elpi Command via the (ltac1) solve_decision tactic? If so, how can I construct a valid goal? If not, what should I be doing instead?

view this post on Zulip Enrico Tassi (Jan 25 2022 at 20:46):

I think you need this commit https://github.com/LPCIC/coq-elpi/pull/319/commits/9f82e6ea1da82f8796eb4711161b7f5b5812e17c (from https://github.com/LPCIC/coq-elpi/pull/319), and then do like so: https://github.com/LPCIC/coq-elpi/blob/d58d0f0d54f296d2c90dc691084638f770357b70/apps/derive/elpi/eqbcorrect.elpi#L158-L160 (run solved is up in the same file and calls some ltac code).

view this post on Zulip Enrico Tassi (Jan 25 2022 at 20:48):

In order to build a goal you need to typecheck a term, then its holes can be turned into goals. In that example the term is lp:B : some type and B is a hole.

view this post on Zulip Enrico Tassi (Jan 25 2022 at 20:49):

I can push the commit to master tomorrow, I'm confident about that one. The rest of the PR is very wip, but calling ltac to build a term as part of a Command worked reliably.

view this post on Zulip Enrico Tassi (Jan 25 2022 at 20:50):

Bottom line, building a sealed-goal by hand is too hard, coq.ltac.collect-goals is a builtin for that.

view this post on Zulip Enrico Tassi (Jan 25 2022 at 20:54):

FTR: the error message is cryptic, GHole is the Coq AST node which can contain a tactic call... It is not supported.

view this post on Zulip Jasper Haag (Jan 25 2022 at 21:07):

Thank you for the response and for offering to push those changes to master! I will not be able to test things out until tomorrow, but your explanation makes sense (and the linked example indeed seems to support my use-case).

I agree that manually creating sealed goals is difficult, and I had tried to use coq.ltac.collect-goals, but this failed due to a combination of:

I’ll follow up once tomorrow after experimenting some more :~)

view this post on Zulip Enrico Tassi (Jan 25 2022 at 21:21):

Hum, if the hole/term is type checked before, then collect-goals on the whole term should work.

view this post on Zulip Enrico Tassi (Jan 25 2022 at 21:22):

About type checking, the "idea" is that a hole in elpi is just a hole, when you type check the term (pass it to Coq) then the hole becomes (also) and evar, and there is a link between the hole and the evar. An evar is also a goal, and can be collected. A hole, well it is just a hole, it does not have a (Coq) type for example.

view this post on Zulip Enrico Tassi (Jan 25 2022 at 21:23):

https://github.com/LPCIC/coq-elpi/pull/333

view this post on Zulip Jasper Haag (Jan 25 2022 at 22:51):

Aha, I was wondering where the elpi<->Coq-evar mapping was being introduced. Thank you for explaining this in more detail (and linking the PR).

view this post on Zulip Enrico Tassi (Jan 26 2022 at 06:33):

FYI coq.sigma.print displays this mapping.

view this post on Zulip Notification Bot (Jan 26 2022 at 13:51):

Jasper Haag has marked this topic as resolved.

view this post on Zulip Jasper Haag (Jan 26 2022 at 13:52):

Right. I was looking into the mapping and noticed that when I tried to manually setup my goal - or coq.ltac.collect-goals - I was not seeing any evar mappings (which I now realize was caused by my aforementioned missteps w.r.t typechecking my skeleton).

view this post on Zulip Notification Bot (Jan 26 2022 at 13:52):

Jasper Haag has marked this topic as unresolved.

view this post on Zulip Notification Bot (Jan 26 2022 at 21:55):

Jasper Haag has marked this topic as resolved.


Last updated: Mar 28 2024 at 18:02 UTC