Stream: Coq devs & plugin devs

Topic: Documentation for Miniml.ml ?


view this post on Zulip walker (Aug 04 2022 at 22:07):

I am writing coq extraction plugin and I am using the vast majority of the extraction code. I see the AST representation in the file miniml.ml

But I am struggling with understanding few things:

I am having hard time mapping Coq code to miniml structure.

For instance, I have no idea what is SEmodule or SEmodtype?

If there is a documentation, I it will be nice, also if there is a way to convert coq code to miniML and display it, it will also be nice since it will help with interactive development.

Also, I am trying to follow existing implementations but I don't understand some functions like is_inline_custom what is meant by custom?

view this post on Zulip Jason Gross (Aug 05 2022 at 07:22):

I expect SEmodule is about Module foo. ... End foo. and SEmodtype is about Module Type foo. ... End foo. (see https://coq.inria.fr/refman/language/core/modules.html). Not sure about your other questions.

view this post on Zulip Gaëtan Gilbert (Aug 05 2022 at 07:30):

a way to convert coq code to miniML

the functions in extraction.mli?

and display it

I don't think there's a printer defined for miniml (unless you count the extraction backends)

Also, I am trying to follow existing implementations but I don't understand some functions like is_inline_custom what is meant by custom?

stuff like https://coq.github.io/doc/master/refman/addendum/extraction.html#coq:cmd.Extraction-Inline https://coq.github.io/doc/master/refman/addendum/extraction.html#coq:cmd.Extract-Constant

view this post on Zulip walker (Aug 05 2022 at 07:31):

wow I didn't notice that hidden documentation

view this post on Zulip walker (Aug 05 2022 at 07:31):

I will give it another try

view this post on Zulip Gaëtan Gilbert (Aug 05 2022 at 07:31):

in what sense is that hidden?

view this post on Zulip walker (Aug 05 2022 at 07:32):

I couldn't find it by looking in the source code :sweat_smile: I thought docs would be in mli files, but never thought that this maps 1-1 to user interface

view this post on Zulip walker (Aug 05 2022 at 07:33):

one last question.

view this post on Zulip Gaëtan Gilbert (Aug 05 2022 at 07:33):

~oh actually there's some printer stuff in extract_env (follow the Show Extraction implem)~
nevermind it's just running the extraction

view this post on Zulip walker (Aug 05 2022 at 07:33):

how can I embed a coq expression in ocaml in utop

view this post on Zulip walker (Aug 05 2022 at 07:34):

so to observe how it gets converted to miniml, I need to use utop like interactive test space where I just write quick expression and see how it maps to miniml

view this post on Zulip Gaëtan Gilbert (Aug 05 2022 at 07:39):

I think you need to go through the parser
something like

Constrintern.interp_constr env sigma (Pcoq.Entry.parse Pcoq.Constr.constr_eoi
  (Pcoq.Parsable.make (Gramlib.Stream.of_string "(fun a b => a + b)")))

view this post on Zulip Gaëtan Gilbert (Aug 05 2022 at 07:41):

not sure it works though

view this post on Zulip walker (Aug 05 2022 at 07:52):

thanks for the pointers, I will either get it working or come up with something creative to get it to work.


Last updated: Feb 01 2023 at 15:04 UTC