Stream: Coq devs & plugin devs

Topic: mutual_inductive_body API


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: Oct 16 2021 at 09:07 UTC