So far, MetaCoq does not support primitive integers, floats and arrays recently introduced in Coq. https://github.com/MetaCoq/metacoq/blob/613bfd9d70699986eb78463b03f6860b0ce98853/template-coq/src/quoter.ml#L267-L269
Are there any plans to add support for these?
Not as far as I'm aware, but also I don't think there are crucial hurdles in supporting them at least on the Template-Coq level. I'm not so sure how easy it is to also include them in the type system, PCUIC, the type checker, erasure and so on, but maybe that is orthogonal. How far on the different subprojects of MetaCoq would you need the support to go in order to be useful for you?
One of the reasons is adding the support for primitives to CertiCoq: https://github.com/PrincetonUniversity/certicoq/issues/24 to allow for efficient compilation of arithmetic. So, I believe, the primitives should be supported all the way until erasure.
I don't think it will be terribly complicated but it might be quite a bit of plumbing and some careful thinking about how to formulate/stage the typing rules and reduction rules.
On the translations side I suppose all of metacoq will simply cary around the primitive objects without intervening
@Jakob Botsch Nielsen , @Yannick Forster, @Danil Annenkov and anyone interested do you have some time tomorrow morning to talk about this?
Sure, I'm free all day tomorrow
Yeah, I'm free tomorrow as well
Let's chat here: https://rdv4.rendez-vous.renater.fr/metacoq
If that's ok with you yes ?
Yep, just a sec
Any conclusions? :)
tPrim (t : prim_tag) (e : prim_model t)constructor to avoid duplication.
Ultimately, we would have
tPrim (t : prim_tag) (e : term) I guess, and typing will ensure that
e is a correct model of
t, and that should be preserved by reduction.
(Correct me if I'm wrong :)
Last updated: Aug 11 2022 at 02:03 UTC