The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Wed, Oct 30, 2019 at 3:15 PM Clément Pit-Claudel <cpitclaudel AT gmail.com> wrote:

Hi all.

I'm running out of ideas regarding a tricky Coq extraction question.

I have a compiler from Foo to Bar written in Coq, then a compiler from Bar to Baz written in OCaml.  Foo and Bar are ASTs defined as `Inductive`s in Coq; Baz is an AST defined in OCaml.

I don't write programs directly in Foo; instead I use Gallina as a metaprogramming language to generate Foo ASTs.  Then I extract these ASTs to OCaml and use the BarBaz compiler written in OCaml to generate Baz ASTs and write these to disk.

Currently, the FooBar compiler is bundled with all my example Foo programs and extracted as one FooBar.ml file, and then the BarBaz compiler depends on FooBar.ml and compiles all the example Foo programs.

I'm looking for a way to extract example programs separately from the compiler itself.  This would allow me to distribute an OPAM package FooBarBaz including the whole compilation pipeline, and then users could write their program in Coq, like this:

```
Definition prog : foo_ast := ….

Module FooBarBaz.
  Axiom baz_ast: Type.
  Extract Constant baz_ast => "FooBarBaz.BarBaz.baz_ast".

  Axiom compile : forall (prog: foo_ast): baz_ast.
  Extract Constant compile => "FooBarBaz.compile_foo".

  Axiom write_to_disk : forall (compiled_prog: baz_ast): unit.
  Extract Constant compile => "FooBarBaz.write_to_disk".
End FooBarBaz.

Definition main : unit := FooBarBaz.write_to_disk (FooBarBaz.compile_foo prog) "prog.baz".
Extraction "prog.ml" main.
```

The generated prog.ml would be linked against the OPAM FooBarBaz package, and running prog.ml would produce "prog.baz".

Unfortunately, this doesn't work: prog.ml has its own copy of the Foo and Bar ASTs, and these are not nominally the same types as those in the FooBarBaz package, so the call to FooBarBaz.compile_foo doesn't typecheck ("This _expression_ has type foo_ast but an _expression_ was expected of type FooBarBaz.FooBar.foo_ast)

Is there an easy way around this issue?  I guess I'd need to either:

* Convince OCaml to accept to unify two structurally equal types; is this possible without an unsafe cast?

Structurally equal types are equal.  What you mean is "two inductive types that have the same constructors with the same argument types", and the answer is no, it is not possible.

* Tell Coq to extract only the definitions not provided by `FooBarBaz.FooBar`, and to add `open FooBarBaz.FooBar` at the top of `prog.ml`; is there a way to do that? Some form of incremental extraction?

Not exactly what you describe, but "Extract Constant" and "Extract Inductive" could help.  Consider:

Inductive t := A | B (n: nat) | C (b: bool).

Fixpoint f(x : t) := match x with A => ... | ... end.

If you extract as is, it will produce a definition for type t, with constructors A, B, C, and a definition for function f that will use those constructors.

Now, add the following before extraction:

Extract Inductive t => "Lib.t" [ "Lib.A" "Lib.B" "Lib.C" ].

Then, t will be defined as an abbreviation for Lib.t, and the code for f will use constructors prefixed with Lib.  That might do what you want.

* Add unsafe casts and hope for the best, which I think should work fine, but won't detect issues like version mismatches between the FooBarBaz library used on the OCaml and the FooBar library used on the Coq side.

Hmph.  What's the point of proving code if you're adding unsafe casts in the end?

I've also considered the following:

* Serializing Bar ASTs on the Coq side and reparsing them on the OCaml side, but they contain functions, so that's not trivial.
* Marshalling the ASTs, but that's just as unsafe as Obj.magic, as far as I understand
* Using library extraction and delete all modules already included in FooBar.ml, then prefixing all references to these modules in the remaining code with FooBarBaz.FooBar.

That might work too.

* Recompiling a fresh copy of the whole FooBarBaz library every time I need to compile a Foo program, but that's inconvenient and heavy-handed.

Indeed.

Any advice?

Don't use unsafe casts :-)

- Xavier Leroy

Thanks!
Clément.