Probably too broad a question, but is there a way to sort of 'extract' (not sure if that is the term for languages other than ml and haskell) to a language different from those that coq supports by default?
I'm just looking for very simple stuff (to start with at least. But if it won't scale well, at least to satisfy curiosity).
Specifically what I had in mind was converting a simple inductive type in coq to an enum type in python (is that even possible?).
Like using this type
Inductive Fruit := apple | orange | mango.
to produce its Python version:
class Fruit(enum.Enum): apple = enum.auto() orange = enum.auto() mango = enum.auto()
By doing simple textual placement of things like
Is it by writing a coq plugin?
some people are content with just deeply embedding a language in Coq and writing various pretty-printers. But sure, if you want the
Extraction commands, you need to write a plugin.
How would we make pretty printer? Do we have to ocaml for that? Or can it be done within coq itself? I have no idea about this and thought extraction was the only way to have something like this.
A pretty-printer is a function Expr -> String, so it can can be written in Coq (EDIT: in Gallina, even!)
"deeply embedding a language" to some extent means defining an inductive type for its abstract syntax tree.
however, looking at
Fruit and obtaining, say,
[“apple”, “orange”, “mango”] isn’t doable in Gallina itself… for this step you might need something like Ltac2 (wouldn’t know how to do it in Ltac1).
it's doable with MetaCoq I believe.
recent paper / code doing pretty-printing and some plugin tooling towards the end for a few functional languages: https://twitter.com/BasspittersBs/status/1444753617282605062
Extracting functional programs from Coq, in @CoqLang. http://arxiv.org/abs/2108.02995 57pp overview of our work in ConCert converting Coq programs to ML-family programs (@rustlang, @elmlang, ...) Extracted rust smart contracts running on @ConcordiumNet http://github.com/AU-COBRA/ConCert- Bas Spitters (@BasspittersBs)
Does pretty printing mean a sort of mapping from coq notations to some strings?
Last updated: Jan 31 2023 at 12:01 UTC