Stream: Coq users

Topic: 'Extraction' to a different language

Julin S (Nov 27 2021 at 06:05):

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 = enum.auto().

Is it by writing a coq plugin?

Karl Palmskog (Nov 27 2021 at 11:31):

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.

Julin S (Nov 27 2021 at 15:06):

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.

Paolo Giarrusso (Nov 27 2021 at 15:40):

A pretty-printer is a function Expr -> String, so it can can be written in Coq (EDIT: in Gallina, even!)

Paolo Giarrusso (Nov 27 2021 at 15:42):

"deeply embedding a language" to some extent means defining an inductive type for its abstract syntax tree.

Paolo Giarrusso (Nov 27 2021 at 15:44):

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).

Karl Palmskog (Nov 27 2021 at 15:45):

it's doable with MetaCoq I believe.

Karl Palmskog (Nov 27 2021 at 15:47):

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)

Julin S (Dec 03 2021 at 16:32):

Does pretty printing mean a sort of mapping from coq notations to some strings?

Last updated: Apr 18 2024 at 17:02 UTC