Rodolphe Lepigre (Aug 07 2023 at 09:40): Rodolphe Lepigre (Aug 07 2023 at 09:40):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.
Pierre Roux (Aug 18 2023 at 13:29):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.
Rodolphe Lepigre (Aug 18 2023 at 14:44):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).
Pierre-Marie Pédrot (Aug 18 2023 at 14:51):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.
Maxime Dénès (Aug 18 2023 at 15:51):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.
Maxime Dénès (Aug 18 2023 at 15:51):I find the name PConst not very explicit, especially in a world where "p" is also used for polymorphic and "const" for definitions.
Pierre-Marie Pédrot (Aug 18 2023 at 16:08):I second the name issue, I'd rather have PrimFoo than PFoo
Rodolphe Lepigre (Aug 18 2023 at 20:31):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.
Maxime Dénès (Aug 19 2023 at 08:54):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