Coq provides an interface for primitives (currently used for machine integers, floating points and arrays), which is currently limited in how it can be extended. As part of my work on https://github.com/coq/coq/pull/17839, I was able to easily lift some limitations (basically, making it possible for primitives to have more complicated types), but I'm hitting another issue that (I believe) requires some larger refactoring (I initially mentioned it here).
Basically, I need to define a new value constructor
Blocked for a primitive type that I want to add. So far, values of primitive types have been added to the
Constr.kind_of_term type, but that is a bit annoying. Morally, I need to add a
Blocked of 'types * 'constr to the
Constr.kind_of_term type, but that sounds a bit too invasive. A better option would be to instead have a new type in
kernel/cPrimitives.ml for "primitive type constructors", which would also encompass primitive integers, floats and arrays. So, something like:
type ('constr, 'types, 'sort, 'univs) prim_const = | Int of Uint63.t | Float of Float64.t | Array of 'univs * 'constr array * 'constr * 'types | Block of 'types * 'constr
And then, we would modify the type Constr.kind_of_term in the following way:
- | Int of Uint63.t - | Float of Float64.t - | Array of 'univs * 'constr array * 'constr * 'types + | PConst of ('constr, 'types, 'sort, 'univs) CPrimitives.prim_const
Of course, the proposed change is also invasive, but would make it easier to add new primitives on the long run, without having to change
Constr.kind_of_term again (which is annoying especially for plugins, I guess).
What do you think of this proposed change? If we can agree on a plan, I'm happy to implement it.
Sounds reasonable to me. I guess there is no good reason for stacking everything into
Constr.kind_of_term, it's rather that primitive integers were first alone then arrays and float were added somewhat independently.
I actually implemented this in a draft MR, to see what that would look like. It mostly seems to work, although
coqchk is broken due to the representation of terms having changed (or at least that is my rough understanding, I did not investigate much).
The coqchk issue is not very serious, it can be fixed rapidly. I don't have a lot of time these days but if nobody tackles it by then I'll have a look when possible.
I have nothing against the change, but I'm not so sure you gain a lot in practice : you'll have to repair the match plugins will do on the kind of primitive constants instead of the one on
I find the name
PConst not very explicit, especially in a world where "p" is also used for polymorphic and "const" for definitions.
I second the name issue, I'd rather have PrimFoo than PFoo
I have nothing against the change, but I'm not so sure you gain a lot in practice : you'll have to repair the match plugins will do on the kind of primitive constants instead of the one onkind_of_term.
To be honest, I'm also not super convinced that this improves anything. My initial thinking was that this would allow factoring a bunch of code paths that deal with head normal forms of primitive types, and that this would make it easier to add new primitives. But regardless of this refactoring, adding new primitives will lead to a change in the AST at one level or another.
Yes, that was exactly my point. Having suffered from it, I agree with the problem (extending terms is really tedious). But not sure what the proper solution is. I suspect that using a bit more abstraction (and a richer API on terms) in plugins would reduce the need for some calls to
kind_of_term. That way you can really gain because you have to adapt to the AST extension only once (on the Coq side) rather than many times for each plugin. But I haven't looked at plugin code recently to check if that's true.
Last updated: Dec 05 2023 at 12:01 UTC