This PR adds generic support for extracted plugins taking Coq's AST as input, and is used in the CertiCoq project to provide an efficient reification staying entirely in ML.
The way this is done is by functorizing the reifier and allowing different quotations types. Two instances are provided, the usual Constr.t quoter which produces a Coq value in the Template.Ast type, and another that quotes into the extracted version of that Ast in ML. The reification code is reused to ensure consistency.
For the ML reifier, we slightly tweak extraction to extract strings to char list, improving memory usage and performance significantly. Any extracted plugin wanting to plug to this reifier will have to do the same.
mattam82
commented
7 years ago
This PR adds generic support for extracted plugins taking Coq's AST as input, and is used in the CertiCoq project to provide an efficient reification staying entirely in ML.
The way this is done is by functorizing the reifier and allowing different quotations types. Two instances are provided, the usual Constr.t quoter which produces a Coq value in the Template.Ast type, and another that quotes into the extracted version of that Ast in ML. The reification code is reused to ensure consistency.
For the ML reifier, we slightly tweak extraction to extract strings to char list, improving memory usage and performance significantly. Any extracted plugin wanting to plug to this reifier will have to do the same.