Stream: Elpi users & devs

Topic: Possible bug related to implicit arguments


view this post on Zulip Rodolphe Lepigre (Oct 07 2022 at 14:38):

I submitted a bug report about a change of behaviour on the definition of an Elpi Command, and I'm actually thinking this might have been on purpose somehow. Basically, if you run

From elpi Require Import elpi.
Class I := {}.
Class L (i : I) := {}.

Succeed Definition xxx `{L} : Prop := True.

Elpi Command hello.
Elpi Accumulate lp:{{
  main Arguments :- coq.say Arguments.
}}.
Elpi Typecheck.

Elpi hello Definition D `{l : L} : Prop := True.

the [const-decl ...] that is fed as argument to main does not have a "parameter" thingy for the implicit i (the omitted parameter to L), whereas it used to be the case with earlier versions of elpi / coq-elpi.

Is there something I missed, or is this indeed a bug?

view this post on Zulip Enrico Tassi (Oct 07 2022 at 15:11):

It may be related to https://github.com/LPCIC/coq-elpi/#terms-as-arguments , Quick try #[arguments(raw)] Elpi Command hello.

view this post on Zulip Enrico Tassi (Oct 07 2022 at 15:11):

It is a bug I guess, but I don't have time now to really look into it.

view this post on Zulip Rodolphe Lepigre (Oct 07 2022 at 15:28):

That seems to fix my problem! Thanks Enrico!
Do you know what is happening here?

view this post on Zulip Enrico Tassi (Oct 07 2022 at 18:55):

I still need to check the code, but my feeling is that:

I've the feeling that this code
https://github.com/LPCIC/coq-elpi/blob/96b3a3d72f8b6d93ec6d7611c1575a056e13688e/src/coq_elpi_arg_HOAS.ml#L353
and this other code
https://github.com/LPCIC/coq-elpi/blob/96b3a3d72f8b6d93ec6d7611c1575a056e13688e/src/coq_elpi_arg_HOAS.ml#L314
chained with
https://github.com/LPCIC/coq-elpi/blob/96b3a3d72f8b6d93ec6d7611c1575a056e13688e/src/coq_elpi_arg_HOAS.ml#L799
give different parameters.
Indeed the name of the latter suggest I did not try hard enough ;-)

view this post on Zulip Enrico Tassi (Oct 07 2022 at 18:57):

It is probably this line which needs "refinement": https://github.com/LPCIC/coq-elpi/blob/96b3a3d72f8b6d93ec6d7611c1575a056e13688e/src/coq_elpi_arg_HOAS.ml#L664, the i parameters is flagged as what?

view this post on Zulip Rodolphe Lepigre (Oct 07 2022 at 21:00):

Cool, thanks for this. I might take a crack at solving this if I can find a moment.


Last updated: Mar 29 2024 at 11:01 UTC