The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Maybe a silly question, but does it work if you use { } instead of [ ]? I don't know if you just copied over the code incorrectly. The error messages for .mlg files are always bewildering. Apologies if it's not that. I haven't used VERNAC ARGUMENT EXTEND before.

Whenever you do figure this out, I'd like to add an example to one of the plugin tutorials in the Coq repo. Please let me know if you are willing to share a minimal example for that.

Talia

On Thu, Jan 30, 2020, 11:38 PM Zoe Paraskevopoulou <zoe.paraskevopoulou AT princeton.edu> wrote:

Hi Coq Club,

I’ve been trying to write a vernacular command that parses some optional arguments, but I’m facing some issue and I’d appreciate some help.

The result I’m trying to achieve is: 

CertiCoq Compile [options] <global_identifier>

where [options] is zero or more compilation flags like -debug.

For this I wrote the following code: 

type command_args =

 | ANF

 | TIME

 | OPT of int

 | DEBUG

 | ARGS of int

VERNAC ARGUMENT EXTEND cargs 

| [ "-anf" ] -> [ ANF ]

| [ "-time" ] -> [ TIME ]

| [ "-o1" ] -> [ OPT(1) ]

| [ "-debug" ] -> [ DEBUG ]

| [ "-args" int(n) ] -> [ ARGS(n) ]

END.

However, when I compile I get the following error: 

File "g_certicoq.ml4", line 1, characters 0-0:
Error: This _expression_ has type int -> Pp.t
       but an _expression_ was expected of type
         'a Extend.entry = 'a Grammar.GMake(CLexer).Entry.e

This happens whenever I try to parse a non-terminal symbols (e.g. string()) in VERNAC ARGUMENT EXTEND, not just with int().

If I drop the last case of cargs and parse this option at the VERNAC COMMAND instead, everything works:

VERNAC COMMAND EXTEND CertiCoq_Compile CLASSIFIED AS QUERY

| [ "CertiCoq" "Compile" cargs_list(l) “-args” int(x) global(gr) ] -> [ ... do stuff ...  ]

END

Any idea about what is going on? I’m suspecting that I’m missing an import because I’ve seen this type of parsing in VERNAC ARGUMENT EXTEND before. For example here: https://github.com/coq/coq/blob/master/plugins/ltac/g_ltac.mlg. I tried to use the same imports but that didn’t help.

I am using Coq 8.9.1 and OCaml 4.07.0.

Cheers,

Zoe