walker (Aug 04 2022 at 22:07): 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?
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.
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
walker (Aug 05 2022 at 07:31):wow I didn't notice that hidden documentation
walker (Aug 05 2022 at 07:31):I will give it another try
Gaëtan Gilbert (Aug 05 2022 at 07:31):in what sense is that hidden?
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
walker (Aug 05 2022 at 07:33):one last question.
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
walker (Aug 05 2022 at 07:33):how can I embed a coq expression in ocaml in utop
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
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)")))
not sure it works though
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: Oct 13 2024 at 01:02 UTC