The Coq mailing list

[Jasper Hugunin <jasperh AT cs.washington.edu>]

Hello,

That you need different brackets for each quotation is indeed annoying; I've struggled with it myself.

Making "x := y" a level 0 command fixed the second question you have in that file, along with adding the invisible antiquotation you mention.

I found this by trying replacing [x custom string at level 4] with [x ident], and then Coq told me that notations starting with an atomic _expression_ must be at level 0.

Those changes also let the final question get further (past the ; case), but it now fails in the "if" case on "then", apparently thinking b is an aexp and then looking for a <= or =. Playing around with making the level of "a = a2" and "a <= a2" zero, and adding invisible antiquotations for global bexps makes different things succeed and fail, so there may be something possible there. This feels like a similar problem to the second question, in a slightly different guise.

Making the inside of the quotations look for things of level 10 or so rather than 0 may help avoid weird things, since you are writing [ x + y ] rather than [ ( x + y ) ].

Best of luck,

- Jasper Hugunin

On Tue, Sep 24, 2019 at 3:06 PM Jim Fehrle <jim.fehrle AT gmail.com> wrote:

I don't know too much about notations, but perhaps this is not completely useless:

It appears that com doesn't have a constructor to represent calling or referencing another com such as subtract_slowly_body.  And presumably that would need its own notation.

You can reproduce the problem with the following simpler example:

Definition foo : com :=

  [[subtract_slowly_body]].

I suppose defining a notation like "'call' x" might be a way to get around parsing limitations.

--Jim

On Tue, Sep 24, 2019 at 4:05 AM Benjamin C. Pierce <bcpierce AT cis.upenn.edu> wrote:

Any suggestions from the community on how to make custom entries work better here would be greatly appreciated.  We would like to use the new features in the next release of Software Foundations (for which the timeline is rather tight), but right now we are blocked on several things that appear to be either inconveniently rigid in the design or not working as documented.  :-(

Thanks!

    - Benjamin

> On Sep 22, 2019, at 1:33 PM, Konstantinos Kallas <kallas AT seas.upenn.edu> wrote:
>
> Hi all,
>
> We are trying to define the syntax of a simple imperative language using the Custom entries feature but we are encountering some problems. Some of the problems might not be related to custom entries per se, but might be caused by some misuse of the notation feature (due to my lack of understanding of parsing in Coq).
>
> I have attached a file that contains the definitions, some examples that work as expected, and some examples where the parser gets confused (that are annotated with "Question:" comments).
>
> It would be great if someone could give us some hints about what could be the problem or how should we go about solving it.
>
> Thanks,
> Konstantinos