The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

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?
* 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?
* 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.

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.
* 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.

Any advice?

Thanks!
Clément.