Hello, I would like to extract a single-argument Inductive type to a Record. Since the record constructor is not available in OCaml, I tried to write a wrapper function around the constructor and extract the record constructor to this constructor. However, it seems that the Coq extraction automatically transforms the function type (taking in a tuple rather than multiple arguments) but does not parenthesize the arguments appropriately.

The following example shows this:

```
Require Import Coq.Bool.Bool.
(*Type in Coq*)
Record aty1 := mk_a1 {a1: bool; a2 : bool; a3 : bool}.
(*Type we want to extract to in OCaml*)
Record aty2 := mk_a2 {a11: bool; a12 : bool; a13 : bool}.
(*The function to translate mk_a1 to during extraction*)
Definition mk_ab (x: bool * bool * bool) : aty2 :=
{| a11 := fst (fst x); a12 := snd (fst x); a13 := (snd x) |}.
(*Test*)
Definition foo (x y z: bool) : aty1 :=
mk_a1 x y z.
From Coq Require Extraction.
Require Import Coq.extraction.ExtrOcamlBasic.
Extract Inductive aty1 => "aty2" ["mk_ab"].
Extract Inlined Constant Datatypes.fst => "fst".
Extract Inlined Constant Datatypes.snd => "snd".
Separate Extraction mk_ab foo.
```

This results in the ml file:

```
type aty2 = { a11 : bool; a12 : bool; a13 : bool }
(** val mk_ab : ((bool * bool) * bool) -> aty2 **)
let mk_ab x =
{ a11 = (fst (fst x)); a12 = (snd (fst x)); a13 = (snd x) }
(** val foo : bool -> bool -> bool -> aty2 **)
let foo x y z =
mk_ab' (x, y, z) (*not parenthesized correctly*)
```

Which gives the error message (for the argument to `mk_ab`

in foo): ```
This expression has type 'a * 'b * 'c
but an expression was expected of type (bool * bool) * bool
```

. The fix is to correctly parenthesize as `((x, y), z)`

. Is there a way to extract a single constructor Inductive/Record to a Record and somehow map the constructor appropriately? Thanks.

`bool * bool * bool`

in coq is `(bool * bool) * bool`

, but in ocaml this is not true

Maybe something like

```
Extract Inductive aty1 => "aty2" ["(fun (a,b,c) => mk_ab ((a,b),c))"].
```

would work

This works, thanks!

Last updated: Jun 23 2024 at 03:02 UTC