Extract Format.string_of_atom to OCaml

[liyishuai]

Uncommenting any line breaks the compilation:

(* From Coq Require Import ExtrOcamlNatInt. *)
(* From Coq Require Import ExtrOcamlString. *)
(* From Coq Require Import ExtrOcamlZInt. *)
From Ceres Require Import Format.
Extraction TestCompile string_of_atom.

[liyishuai]

Blame coq/coq#7017 for all of these.

[Lysxia]

Does adding custom extraction rules for int and whatnot fix this?

On 10/17/19 12:27 AM, Yishuai Li wrote:

Blame coq/coq#7017 for all of these.

[liyishuai]

Maybe not. You can avoid int but not bool, unless with https://github.com/coq/coq/issues/7017#issuecomment-543023388 for OCaml 4.08+.

[Lysxia]

For builtins pre 4.08 one more trick is to have a standalone raw OCaml module to give a qualifiable name to those types.

[liyishuai]

Do you have a fix in hand? My tests in DeepWeb are blocked by extractions. I could write another version without Ceres, but might not escape this bug.

[Lysxia]

Does it not work to fix extraction like

Extract Inductive bool => "Bool.t" [ "false" "true" ].

?

[liyishuai]

Not really:

From Coq Require Import ExtrOcamlString.
From Ceres Require Import CeresFormat.
Extract Inductive bool => "Bool.t" ["false" "true"].
Extraction TestCompile string_of_atom.

File "/tmp/testextractione95d6a.ml", line 428, characters 5-9:
428 |    | Left -> '\\'::('t'::escaped_s')
           ^^^^
Error: This variant pattern is expected to have type bool
       The constructor Left does not belong to type bool

[Lysxia]

That's a different bug though. Import ExtrOcamlBasic.

[Lysxia]

Here's a dirty hack for the int bug, by extracting Decimal.int to uint + uint. You have to make sure sum is extracted (e.g., adding it at the end of the Extraction command), and that also relies on the fact that sum gets extracted before Decimal.int.

(* Test.v *)
Require Import Extraction.
From Coq Require Import Decimal.

Extract Inductive Decimal.int => "((uint, uint) sum)" ["Inl" "Inr"].

From Coq Require Import ExtrOcamlBasic.
From Coq Require Import ExtrOcamlString.
From Coq Require Import ExtrOcamlNatInt.
From Coq Require Import ExtrOcamlZInt.

From Ceres Require Import CeresFormat.
Extraction "test.ml" string_of_atom sum.

$ coqc Test.v
$ ocamlc test.mli test.ml

# No errors.

[liyishuai]

Not so dirty compared to QuickChick/QuickChick@dadabe5 🤦🏻‍♂️

[Lysxia]

Another version that avoids depending on the order in which things are extracted, is to put sum in an external module, and use qualified names to refer to it:

(* Test.v *)
Require Import Extraction.
From Coq Require Import Decimal.

Extract Inductive Decimal.int => "((uint, uint) M.sum)" ["M.Inl" "M.Inr"].

From Coq Require Import ExtrOcamlBasic.
From Coq Require Import ExtrOcamlString.
From Coq Require Import ExtrOcamlNatInt.
From Coq Require Import ExtrOcamlZInt.

From Ceres Require Import CeresFormat.
Extraction "test.ml" string_of_atom.

(* m.ml *)
type ('a, 'b) sum = Inl of 'a | Inr of 'b

$ coqc Test.v
$ ocamlc m.ml test.mli test.ml