Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Question about writing plugins/vercular commands extension

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about writing plugins/vercular commands extension


Chronological Thread 
  • From: Zoe Paraskevopoulou <zoe.paraskevopoulou AT princeton.edu>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] Question about writing plugins/vercular commands extension
  • Date: Thu, 30 Jan 2020 20:18:06 +0000
  • Accept-language: en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=princeton.edu; dmarc=pass action=none header.from=princeton.edu; dkim=pass header.d=princeton.edu; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=HGeD19qHuf7vQjJxbbhSsPPRqZYaaY7zS+Lql61KXFI=; b=F2rUGCZkeO/2lU0WDLWJrkvILxjyyzDD5LTfaWFCSKY2mFT8bmT+bMXxHnKB0i1VTG3Nq5LK7SG9m29h3evTtlP8lFhJ5AikHLHko/QxMyVxt15CWQbI3LKfY3CblOXuYLMy2yVeNfSxoFjDH7sxhWsdVaHNej+YxVJn4Q9hpH0jJACGUpt+uHbOXWqXOHRdpJfT+gGZVJhzeautxReqAXaXQJrSUdEFVMJNmty+7e3OUp6nhvnLFqaFhxjUWO/ZskgkYmxhh/L+FxsoCB0EIyQFkridRkCZquAr5ho9UcrTUvGDuZv09Sa6Gs4OjyNO4rfbd+pHtuL5W+y4jwT2VQ==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=furBUk0wBnDjMve6h5zqVv87WB2Juo8OzTPbQ9BaKfl03KTyjY217RqGejmpyrUVCHfgYjmNjCnl460KMTMg/K99xyyJi1HJLz+ng/iewN4l3WSwxPRHc8/kzYgKJUFcQm0nbB69h5EBII4MxBUMWuI9mWN8Ai/N0Um9jWNpkYDvsxoJWgiLeAxUxgZwvsK4ho+IHK9no3HG41VmI7O8abVuddKd2T32XgVhSVvYJJ68MXEHEVH6nFIk6ychdXMCYjul+Gkjq03UmoLyC2aT4fZyu2b10W+aI4FIqkbFmlBjdlc7ShHQth4nzQFoZgyV7vn9qXwHZe17dzTAz+xcrQ==
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=zoe.paraskevopoulou AT princeton.edu; spf=Pass smtp.mailfrom=zoe.paraskevopoulou AT princeton.edu; spf=Pass smtp.helo=postmaster AT Princeton.EDU
  • Ironport-phdr: 9a23:qZrtwRybha9ek/DXCy+O+j09IxM/srCxBDY+r6Qd2u8fIJqq85mqBkHD//Il1AaPAdyHrakUwLON6eigATVGvc/a9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMucQam4VvJ6U+xhfUrHZEZfldyWd0KV6OhRrx6dq88ZB5/yhMp/4t8tNLXLnncag/UbFWFiktPXov5M3suxnDTA+P6WUZX24LjBdGABXL4Q/jUJvpvST0quRy2C+BPc3rVr80Qiit771qSBDzligKMSMy/XzNhcxxiKJbpw+hpwB6zoXJboyZKOZyc6XAdt4cWGFPXNteVzZZD428cYUBEvYBM+hboYn8u1QBogCzChOwCOPq0DJEmmP60K883u88EQ/GxgsgH9cWvXvXq9X6KroZX/qvw6nS1zrDdPBW1inj6IjPahAhpuyMXbZ3ccrM1EIiEALEjlKOpoD/JzOazP4NvHKA7+pjS+2vlWknqxl2ojiywscsjZTJi5kNylDe9CV5xpo6KsOkSE58Z96oCoVfuDyHN4ZvRM4pXm9muCE/yrIcuJ67ejAHyJsmxx7Da/yHbpOH7gj/W+aWJDd1gm9udrGnhxuq7ESs1O7xWtOp3FpXsCZJiMTAum4O2hDJ9MSLV/tw8l+81TuAywzf8PxILEMomabBNZIszaI8moANvUnNESL6gEv2g7GVe0k4/+Wl7uvqbanmq5KcMoJ5ihzxPb8tl8G6A+k4PAsDUHae9Oum17Ds5030TbNXhfMsiKbZqorVJcEDq665HQBV1oEj5g6lATe80dQYm2UII0xZeBKAiYjlIV7ALv72AvunglSslilkx+zeM7H8HJnALWLPnKr8cbpj8UJQ1RQ/wNNF655KF70MIOr/Wkrru9zZCh85PRa0w+HiCNhl14IeXnyADrWBMKzIq1+H/PkvI+qSa48Lvzb9M/8l5+PqjX8+hF8QZrGp3YEWaHC+AvtpPVmZYX3qgtsbD2gFoxc+QPTwiFKeST5Te2qyX6Uk6z4nD4KmFJ7PSZypgLycxyi2BYZWZ2BDClCUC3jkbYSEW/EWaCKTOMBtiDIEVaLyA7MmgFulsxa/wL56JMLV/DcZvNTtzpI9s+bUjFQ58SF+J8WbyWCECW9uyDAmXTgziZJ4rARFw02Kyqt1nftAEsFX4O4BBhU9ONjExvZzENP/RAXZecqNT0uOWs+nBzo8UtU3hdICfhAuSJ2Zkhnf0n/yUPcunLuRCclsq/+O7z3KP894jk3++uwhgl0hG5YdDXengKVy6w/VQaPlrhfAzvf4ReEnxCfIsVy74y+LtUBcXhR3VPyYD2gFZ03doMj+4AXPQ6L8UO17YDsE8taLL+5xUvOslU9PHaqxIM7fZWm8h2C2QxuE2+HUYQ==
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

Archive powered by MHonArc 2.6.18.

Top of Page