Stream: MetaCoq

Topic: Primitive types in MetaCoq


view this post on Zulip Danil Annenkov (Oct 01 2020 at 09:37):

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?

view this post on Zulip Yannick Forster (Oct 01 2020 at 09:51):

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?

view this post on Zulip Danil Annenkov (Oct 01 2020 at 10:24):

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.

view this post on Zulip Matthieu Sozeau (Oct 01 2020 at 12:04):

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.

view this post on Zulip Matthieu Sozeau (Oct 01 2020 at 12:05):

On the translations side I suppose all of metacoq will simply cary around the primitive objects without intervening

view this post on Zulip Matthieu Sozeau (Dec 07 2020 at 21:44):

@Jakob Botsch Nielsen , @Yannick Forster, @Danil Annenkov and anyone interested do you have some time tomorrow morning to talk about this?

view this post on Zulip Yannick Forster (Dec 07 2020 at 21:45):

Sure, I'm free all day tomorrow

view this post on Zulip Jakob Botsch Nielsen (Dec 07 2020 at 21:54):

Yeah, I'm free tomorrow as well

view this post on Zulip Matthieu Sozeau (Dec 08 2020 at 09:59):

Let's chat here: https://rdv4.rendez-vous.renater.fr/metacoq

view this post on Zulip Yannick Forster (Dec 08 2020 at 09:59):

Now?

view this post on Zulip Matthieu Sozeau (Dec 08 2020 at 09:59):

If that's ok with you yes ?

view this post on Zulip Jakob Botsch Nielsen (Dec 08 2020 at 10:00):

Yep, just a sec

view this post on Zulip Yannick Forster (Dec 08 2020 at 11:50):

Any conclusions? :)

view this post on Zulip Matthieu Sozeau (Dec 08 2020 at 12:16):

view this post on Zulip Matthieu Sozeau (Dec 08 2020 at 12:18):

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.

view this post on Zulip Matthieu Sozeau (Dec 08 2020 at 13:04):

(Correct me if I'm wrong :)


Last updated: Aug 11 2022 at 02:03 UTC