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
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.
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
wow I didn't notice that hidden documentation
I will give it another try
in what sense is that hidden?
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
one last question.
~oh actually there's some printer stuff in extract_env (follow the Show Extraction implem)~
nevermind it's just running the extraction
how can I embed a coq expression in ocaml in utop
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
I think you need to go through the parser
Constrintern.interp_constr env sigma (Pcoq.Entry.parse Pcoq.Constr.constr_eoi (Pcoq.Parsable.make (Gramlib.Stream.of_string "(fun a b => a + b)")))
not sure it works though
thanks for the pointers, I will either get it working or come up with something creative to get it to work.
Last updated: Dec 01 2023 at 06:01 UTC