The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Did you open Stdarg?

Gaëtan Gilbert

On 30/01/2020 21:18, Zoe Paraskevopoulou 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