Quoting + erasure of primitive objects

[zoep]

It would be very useful to add support for primitive ints + floats in MetaCoq (so we can then realize such primitives in CertiCoq's backend). Are there any plans to do so?

[mattam82]

We have not looked at it deeply but it should mostly be a straightforward adaptation of Coq's handling of them. Note that we will need to have a way to translate the axiomatized definitions on the primitive types to something in CertiCoq. If you're eager to try we can certainly guide you a little :)

[zoep]

Hi Matthieu,

For CertiCoq, I'm working on adding support for extracting terms to specific C definitions (à la Extract Constant) and I think the same code can be used to handle compilation of primitive objects.

For MetaCoq, I don't think I'll get the time to try that soon. I might at some point if no one else wants to.

[mattam82]

Ok, we discussed this a bit today during a CUDW2020 working group, and we think ideally we'd like to support primitive types using their primitive representation in template-coq, but modify the translation to PCUIC to uses their models, to ensure correctness of axiomatisation (without introducing axioms in PCUIC). In the meantime, we can certainly hack some unsafe translation that keeps primitive objects untouched until LambdaBox. I'll give a try to this tomorrow.

[intoverflow]

@mattam82 Is this still open? I have time to work on this.

[mattam82]

Hi @intoverflow, it's only somewhat open. We've added treatment of primitive objects to template-coq/pcuic/erasure already, so in erased terms you now get prim_model (https://github.com/MetaCoq/metacoq/blob/coq-8.11/pcuic/theories/PCUICPrimitive.v) values for primitive ints and floats. I think CertiCoq does not translate those yet.
They can be translated back to primitive values using:

Definition uint63_from_model (i : uint63_model) : Int63.int :=
  Int63.of_Z (proj1_sig i).

Definition float64_from_model (f : float64_model) : PrimFloat.float :=
  FloatOps.SF2Prim (proj1_sig f).