Stream: Coq users

Topic: Extraction to Records

view this post on Zulip Josh Cohen (Mar 14 2024 at 17:25):

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

view this post on Zulip Gaëtan Gilbert (Mar 14 2024 at 17:30):

bool * bool * bool in coq is (bool * bool) * bool, but in ocaml this is not true

view this post on Zulip Gaëtan Gilbert (Mar 14 2024 at 17:33):

Maybe something like

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

would work

view this post on Zulip Josh Cohen (Mar 14 2024 at 17:36):

This works, thanks!

Last updated: Jun 23 2024 at 03:02 UTC