Stream: Coq users

Topic: Extraction to Abstract Type


view this post on Zulip Josh Cohen (Feb 20 2024 at 17:54):

Is there any way to extract to OCaml so that a particular type is completely abstract in the resulting .mli file?
Or is there a way to structure Coq developments (preferably without modules) so that this occurs?

For example, say we have the following .v file:

Inductive foo = | A | B.
    Definition isA (f: foo) : bool :=
    match f with
    | A => true
    | B => false
    end.

From which we want to produce the following .mli file:

type foo
val isA : foo -> bool

view this post on Zulip Karl Palmskog (Feb 20 2024 at 18:27):

to my knowledge, there is no way to control the design of the .mli file except by hacking the extraction plugin (not recommended). It can also turn out that .mli file is essentially wrong/invalid and won't compile, due to impedance mismatches between the Coq and OCaml typesystems. Probably our best hope for the future is https://github.com/yforster/coq-malfunction rather than an overhaul of the existing direct-to-OCaml extraction

view this post on Zulip Josh Cohen (Feb 20 2024 at 18:35):

I see, thanks for the info

view this post on Zulip Karl Palmskog (Feb 20 2024 at 18:36):

what people do in practice is that they post-process the .mli file, typically, e.g., with sed

view this post on Zulip Matthieu Sozeau (Feb 21 2024 at 08:24):

Yep, post process is the way to go, in any case.

view this post on Zulip Karl Palmskog (Feb 21 2024 at 08:47):

and in the coq-malfunction workflow, one would typically write an .mli from scratch, right?


Last updated: Jun 22 2024 at 15:01 UTC