coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] OCaml API documentation

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] OCaml API documentation
Date: Mon, 24 Apr 2017 10:06:06 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f177.google.com
Ironport-phdr: 9a23:zUQHfx2AZMB6NUqUsmDT+DRfVm0co7zxezQtwd8ZseISL/ad9pjvdHbS+e9qxAeQG96Kt7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXbAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLniikHOT43/m/Ul8J+kr5UrQm7qBBj2YPZep2ZOOZ8c67bYNgURXBBXsFUVyFZHo6zdIsPD+saPeZYsYb9pEYFoAe4BQa2AuPg1yJDi3js0qIh0+QhEBrG3Aw+ENINqnjbttP1O70UUe+o1qXIzDTDb+9Z2Trm54jIdwouofCIXb5qbcXRzkwvGhrDg16Np4LlODaV2f4Ms2id9+dvSeWvi3Qhqw5vpjivwt0ghZfUiYII0lzE+iR5wJo1Jd2lU0F3e8KrEJxVty2CK4R2QtktQ2VtuCkk0L0GooS3fDMUx5kh2hXRaOSHfpCW7h7/UOudOzR1iXJ/dL6hmRq+7VKsxvD+W8S21ltBszBLncPWtn8X0hze8siHReV5/kemwTuP0hrc6uBAIUwtjKrbKIItzqc+lpYOs0nOHDX6mErxjK+ReUUk/van5/77bbXho5+QL450igfgPaQygsGzH/g0PwwUU2WY+emwzqPv8VPlTLlQk/E7kKvUvIjfJcsBp665BwFV0pwk6xa6Fzqpys8XnXkGLFJeeBKIkYvpN0vUL/D+F/i/hUmjnC1qx/DHIr3hDY7ALnfGkLj7fLZ971RQxxY0zdBa/55UEK0OIOrvWk/ts9zVFgM2Mwutw+r+FNp90p4eVnmUD6+CMKLStEeI6fg1L+mNYo8Vojf9JOI/6/7gl39q0WMaKKKuxN4cbG2yVqBtJFzcan7xiP8AF30Lt0wwVrq5pkeFVGt6bXazRKIx5XkSDougAc+XT4qtgaeB0ST9F5tfYGwAC1GQHl/ncoyFX7EHbyfEcZwpqSANSbX0E9xp7hqprgKvk7c=

Based on template-coq, a plugin that implements reification/reflection, I have a monad that may allow you to write some plugins, especially those implementing transformations of Gallina programs, in Gallina:

https://github.com/aa755/template-coq/blob/574c895cceac2e8b0047a312ac4038db09baf6fa/theories/Ast.v#L107

There are some example invocations near the end of this file:

https://github.com/aa755/template-coq/blob/coq-8.5/test-suite/demo.v

Currently limitations:

1) as in template-coq, universes other than Set/Prop are not properly reified/reflected.

2) the monad is currently very experimental.

If I understand the following correctly, having something like it for Coq would be great:

http://www.cse.chalmers.se/~nad/listings/equality/Agda.Builtin.Reflection.html

Regards,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sun, Apr 23, 2017 at 8:03 AM, Dan Frumin <dfrumin AT cs.ru.nl> wrote:

Dear all,

Is there an up to date documentation on the Coq’s OCaml’s interface somewhere?
I would like to write a plugin, but I didn’t find anything on the website or in the refman. I suppose the only way would be to just
dig into the source code?

Best,
Dan

[Coq-Club] OCaml API documentation, Dan Frumin, 04/23/2017
- Re: [Coq-Club] OCaml API documentation, Emilio Jesús Gallego Arias, 04/24/2017
- Re: [Coq-Club] OCaml API documentation, Abhishek Anand, 04/24/2017