Jasper Haag (Jan 25 2022 at 20:40): 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?
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).
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.
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.
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.
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.
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:
collect-goals on the term-with-hole rather than on the hole itselfI’ll follow up once tomorrow after experimenting some more :~)
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.
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.
Enrico Tassi (Jan 25 2022 at 21:23):https://github.com/LPCIC/coq-elpi/pull/333
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).
Enrico Tassi (Jan 26 2022 at 06:33):FYI coq.sigma.print displays this mapping.
Notification Bot (Jan 26 2022 at 13:51):Jasper Haag has marked this topic as resolved.
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).
Notification Bot (Jan 26 2022 at 13:52):Jasper Haag has marked this topic as unresolved.
Notification Bot (Jan 26 2022 at 21:55):Jasper Haag has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC