Stream: MetaCoq

Topic: Primitive types in MetaCoq

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?

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?

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.

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.

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

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?

Yannick Forster (Dec 07 2020 at 21:45):

Sure, I'm free all day tomorrow

Jakob Botsch Nielsen (Dec 07 2020 at 21:54):

Yeah, I'm free tomorrow as well

Matthieu Sozeau (Dec 08 2020 at 09:59):

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

Yannick Forster (Dec 08 2020 at 09:59):

Now?

Matthieu Sozeau (Dec 08 2020 at 09:59):

If that's ok with you yes ?

Jakob Botsch Nielsen (Dec 08 2020 at 10:00):

Yep, just a sec

Yannick Forster (Dec 08 2020 at 11:50):

Any conclusions? :)

Matthieu Sozeau (Dec 08 2020 at 12:16):

• It would be better to wrap tInt/tFloat in PCUIC into a single tPrim (t : prim_tag) (e : prim_model t) constructor to avoid duplication.
• We need to support reifying "primitive" constants in MetaCoq to make at least the reification work.
  I'll try to push these two things in the prim-int-float branch this week.
  I'm going to stay with the Z/Float models for now, leaving the switch to encoding Int63.t to the right Z constructor representation for later.

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.

Matthieu Sozeau (Dec 08 2020 at 13:04):

(Correct me if I'm wrong :)

Last updated: Apr 19 2024 at 05:01 UTC