Stream: Coq users

Topic: Extraction to Abstract Type

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

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

Josh Cohen (Feb 20 2024 at 18:35):

I see, thanks for the info

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

Matthieu Sozeau (Feb 21 2024 at 08:24):

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

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: Oct 13 2024 at 01:02 UTC