Stream: Coq devs & plugin devs

Topic: mutual_inductive_body API


view this post on Zulip Hugo Herbelin (Aug 20 2021 at 16:02):

I have questions about the mutual_inductive_body API.

For projections, we don't care about having the PrimRecord field to recursively refer to the kernel name of the inductive block. But for constructors, recursive calls are represented with Rels and a substitution by the actual Ind needs to be done everytime we need the type of a constructor. Why not to consistently adopt the convention used for projections also for constructors? The drawback is that the mutual_inductive_body refers to the name to which it is bound in the kernel but the advantage is that we save the process of substitution. Any opinion?

I wonder whether we could not put more basic small-size data in the inductive argument of Ind and Construct rather than having to query the env for simple things like the number of parameters, the name of the types and constructors, etc. Any opinions?

In a similar vein, I wonder whether more data could be precomputed in the mutual_inductive_body. I'm thinking e.g. to complementing mind_nparams with mind_nparamdecls (by analogy with mind_nrealargs and mind_nrealdecls), or to add a version of the arity context with params already chopped, or a version of constructor contexts with params already chopped, ...

view this post on Zulip Gaëtan Gilbert (Aug 20 2021 at 16:06):

Why not to consistently adopt the convention used for projections also for constructors?

sounds good

I wonder whether we could not put more basic small-size data in the inductive argument of Ind and Construct rather than having to query the env for simple things like the number of parameters, the name of the types and constructors, etc. Any opinions?
In a similar vein, I wonder whether more data could be precomputed in the mutual_inductive_body. I'm thinking e.g. to complementing mind_nparams with mind_nparamdecls (by analogy with mind_nrealargs and mind_nrealdecls), or to add a version of the arity context with params already chopped, or a version of constructor contexts with params already chopped, ...

needs:bench

view this post on Zulip Pierre-Marie Pédrot (Aug 20 2021 at 16:24):

beware with cluttering these datatypes with caches though, since it's likely to end up in the vo file

view this post on Zulip Pierre-Marie Pédrot (Aug 20 2021 at 16:24):

while constructor type substitution should probably be cached (I see it pop from time to time in the profiler) I'm quite dubious about anything else you mention

view this post on Zulip Hugo Herbelin (Aug 20 2021 at 16:39):

It is probably not critical if small data (integers and strings) are duplicated in the vo files, knowing that arguments to Ind and Construct are anyway shared, so it would be one copy per file.

view this post on Zulip Hugo Herbelin (Aug 20 2021 at 16:43):

As for having more precomputed data in the mutual_inductive_body it would be only in the file defining the corresponding inductive types. I would be surprised that it leads to overheads, on the contrary. (It is quite a burden to always have to do low-level context carvings that are basically standard.)


Last updated: May 24 2024 at 23:01 UTC