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 Rel
s 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, ...
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
beware with cluttering these datatypes with caches though, since it's likely to end up in the vo file
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
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.
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 13 2024 at 01:02 UTC