Stream: Elpi users & devs

Topic: Possible bug related to implicit arguments

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?

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.

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.

Rodolphe Lepigre (Oct 07 2022 at 15:28):

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

Enrico Tassi (Oct 07 2022 at 18:55):

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

• if it is elpi that processes the arity (raw mode) the extra parameter i is somehow kept
• if it is Coq, then elpi tries to "rediscover" the parameter and fails, maybe it's because the name is L instead of I... the code I wrote is brittle, here:

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 ;-)

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?

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: Oct 13 2024 at 01:02 UTC