Stream: Elpi users & devs

Topic: Quotation for `constructor`

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 10:14):

Looking at the tutorial code in (https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_HOAS.html#quotations-and-antiquotations)

Elpi Query lp:{{
  coq.locate "S" S,
  coq.say {{ 1 + lp:{{ app[global S, {{ 0 }} ]  }}   }}
% elpi....  coq..     elpi...........  coq  elpi  coq

}}

I wonder if there is a direct way to quote the constructor S, that is without using coq.locate. The double angle bracket quotation used during printing leads to a parser anomaly when used on input. Also lib: mentioned later in the same section does not work for me. II find this especially inconvenient in the matching/head part of rules.

This rule is an example for the work around I use. I guess this is not very efficient, if I have several rules with different S.

  vst-extract-local-symbols (app [global (indc S), VN, _VT]) I O :- coq.locate "Etempvar" (indc S), coq.say "Etempvar" VN.

view this post on Zulip Enzo Crance (Oct 27 2022 at 10:19):

You can match input terms with the quoting syntax as well, like the following:

p {{ S lp:X }} :- % ...

It is translated as

p (app [global (indc «S»), X]) :- % ...

with «S» being the gref value for the constructor S (you don't have to call coq.locate).

What is more surprising in your example line is S being applied to several terms (the _VT after VN). This looks like an ill-formed term.

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 10:20):

Please note that in the lower example Sis an elpi variable, not a constructor. The constructor bound to it is Etempvar which takes 2 arguments.

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 10:21):

Thanks for the hint on the correct quoting!

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 10:30):

Sorry, but I can't make this work:

Elpi Accumulate lp:{{
  pred p i:term.
  p {{ S lp:X }} :- coq.say X.
}}.

results in

File "(stdin)", line 3, column 20, character 36:: The reference X
was not found in the current environment.

view this post on Zulip Enrico Tassi (Oct 27 2022 at 11:22):

This works here:

From elpi Require Import elpi.
Elpi Command foo.
Elpi Accumulate lp:{{
  pred p i:term.
  p {{ S lp:X }} :- coq.say X.
}}.

It may be that some other code of yours makes lp: not a quotation anymore?

view this post on Zulip Enrico Tassi (Oct 27 2022 at 11:24):

You code should be:

st-extract-local-symbols {{ S lp:VN _ }} I O :- ...

if it does not even parse then it is definitely some bad interaction with another package.
Can I reproduce it, somehow?

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 11:27):

The code vst-extract-local-symbols {{ S lp:VN _ }} I O :- ... parses, but the variable VN is undefined then - same error message as above. Let me find a short example ...

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 11:39):

@Enrico Tassi : the problem appears with your above code if I steps back over the Elpi import and forward over it again (in VsCoq, CoqIDE seems to be fine). A similar problem has been reported for Ltac2 a longer time back - not sure if it is fixed. You might want to ask PMP about it.

view this post on Zulip Enrico Tassi (Oct 27 2022 at 11:41):

Hum, ok thanks. CC @Pierre-Marie Pédrot , do you recall what it was?

view this post on Zulip Enrico Tassi (Oct 27 2022 at 11:41):

(I think CoqIDE don't show the problem because retracting the first line restarts Coq)

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 11:44):

Indeed CoqIDE shows the same error when I put an arbitrary line in front (I use Require Import ZArith) and don't step back over it.

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 11:46):

Anyway - nice that the quotation works now as expected - this resulted in quite a few question marks on my side.

view this post on Zulip Paolo Giarrusso (Oct 27 2022 at 23:11):

The vscoq bug you see is probably one of the n-thousands bugs with async mode, which should be due for replacement soon (the vscoq roadmap claims this year!)

view this post on Zulip Michael Soegtrop (Oct 28 2022 at 07:38):

@Paolo Giarrusso : as mentioned it doesn't work in CoqIDE either. Afair it was something that going forward and backward over a Require does not leave the Coq parser in the state it was before the Require, but only in a few special cases.

view this post on Zulip Enrico Tassi (Oct 28 2022 at 08:29):

I guess the plugin adds twice the same grammar rule, and for some reason that bricks the parser...

view this post on Zulip Michael Soegtrop (Oct 28 2022 at 08:51):

I don't know much about the Coq parsing machinery, but I guess something like this.

Last updated: Apr 18 2024 at 12:01 UTC