The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi Clément,

> Le 30 oct. 2019 à 15:13, Clément Pit-Claudel 
> <cpitclaudel AT gmail.com>
>  a écrit :
> 
> 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?

We do something like this in the MetaCoq project: using `Separate Extraction` 
or `Extraction Library` to extract module B, knowing that I have an mlpack 
implementing A on which B depends, and then calling `ocamlc -open Myplugin.A 
-I …/user-contrib/myplugin B.ml` to compile the « extension » code. With 
`Separate Extraction`, it’s a matter of removing all the generated code for 
`A` and its dependencies that is produced by extraction. With `Extraction 
Library` the user has to be careful that he extracts all the libraries he 
needs but doesn’t need . No unsafe type casts are inserted this way.

Best,
— Matthieu