Adding an Ltac2 API to manipulate inductive types.

[ppedrot]

Fixes #10095: Get list of constructors of Inductive.

• Added / updated test-suite
• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[JasonGross]

Nice! I think the API is a bit off, though. I think:

• ntypes should be called ninductives or nblocks
• nconstructors should have type t -> int, not data -> int
• get_type should be called get_inductive or nth_inductive or nth or nth_block or nth_mutual_inductive
• get_constructor should have type t -> int -> constructor, I think. But also it's redundant with Constr.Unsafe.constructor?

The intuition is that we have a collection of mutual inductives, and each inductive has constructors associated to it. That is data should be morally equivalent to list inductive or array inductive

It should be clear whether or not get_type (data ind) 0 is equal to ind, or whether data returns the same data for all inductives in the same mutual block.

I think we should also expose the number of parameters of an inductive, perhaps also the number of indices. (And perhaps the number of arguments to each constructor?)

Additionally (possibly beyond the scope of this PR), there should be an API for fetching the following information about inductives:

• is the inductive a record?
• is the inductive a coinductive?
• is the inductive a record?
• is the inductive non-recursive (is this BiFinite or something?)
• if a record, are there primitive projections? if so, API for fetching them
• if a record, is judgmental eta conversion on?

[ppedrot]

nconstructors should have type t -> int, not data -> int

Doing that would require accessing the environment again. It's easy to define a function with your signature in the current API, but using this as a primitive instead would require repeatedly getting the env. So the current signature is better behaved.

ntypes should be called ninductives or nblocks / get_type should be called get_inductive or nth_inductive or nth or nth_block or nth_mutual_inductive

Which one do you prefer?

[JasonGross]

Doing that would require accessing the environment again. It's easy to define a function with your signature in the current API, but using this as a primitive instead would require repeatedly getting the env. So the current signature is better behaved.

In that case, I think we should have something like one of the two following APIs:

Ltac2 Type data
(** Type of data representing a particular inductive and its associated data, independent of the environment. *)

Ltac2 Type mutual_block_data (* alternatively: mutual_data, mutual_blocks_data, or blocks_data *)
(** Type of data representing all mutually defined inductives of a particular mutual inductive block *)

Ltac2 @ external data : inductive -> data := "ltac2" "ind_data".
(** Get the data corresponding to an inductive type in the current
    environment. Panics if there is no such inductive. *)

Ltac2 @ external inductive : data -> inductive := "ltac2" "ind_inductive".
(** Get the inductive type corresponding to the given data. *)

Ltac2 @ external mutual_block : data -> mutual_block_data := "ltac2" "ind_mutual_block".
(** Get the mutual block data in which a given inductive is defined *)

Ltac2 @ external ninductives : mutual_block_data -> int := "ltac2" "ind_ninductives".
(** Returns the number of inductive types appearing in a mutual block. *)

Ltac2 @ external nth_inductive : mutual_block_data -> int -> data := "ltac2" "ind_nth_inductive".
(** Returns the nth inductive type in the block. Index must range between [0]
    and [ninductives mutual_block_data - 1], otherwise the function panics. *)

Ltac2 @ external nconstructors : data -> int := "ltac2" "ind_nconstructors".
(** Returns the number of constructors of the given inductive. *)

Ltac2 @ external nth_constructor : data -> int -> constructor := "ltac2" "ind_get_constructor".
(** Returns the nth constructor of the inductive type. Index must range between
    [0] and [nconstructors data - 1], otherwise the function panics. *)

Morally, data and inductive should represent the same thing, but data is the version that's already accessed the environment. That is, the data and inductive functions should be inverses.

---

Alternatively, if you don't want a separate type for just the mutual block data without an associated index, then we should have

Ltac2 Type data.
(** Type of data representing an inductive and its associated mutual block. *)

Ltac2 @ external data : t -> data := "ltac2" "ind_data".
(** Get the mutual blocks corresponding to an inductive type in the current
    environment. Panics if there is no such inductive. *)

Ltac2 @ external inductive : data -> t := "ltac2" "ind_get_type".
(** Returns the inductive, dropping the data associated with the mutual block. *)

Ltac2 @ external ninductives : data -> int := "ltac2" "ind_ninductives".
(** Returns the number of inductive types appearing in a mutual block. *)

Ltac2 @ external index : data -> int := "ltac2" "ind_index".
(** Returns the index of the inductive type in its mutual block. *)

Ltac2 @ external nth_inductive : data -> int -> data := "ltac2" "ind_nth_inductive".
(** Returns the data associated with the nth inductive type in the block. Index must range between [0]
    and [ntinductives data - 1], otherwise the function panics. *)

Ltac2 @ external nconstructors : data -> int := "ltac2" "ind_nconstructors".
(** Returns the number of constructors of the given inductive. *)

Ltac2 @ external nth_constructor : data -> int -> constructor := "ltac2" "ind_nth_constructor".
(** Returns the nth constructor of the inductive type. Index must range between
    [0] and [nconstructors data - 1], otherwise the function panics. *)

---

WDYT?

[ppedrot]

I actually wrote the original version of this PR using your second API variant, then decided against because it seemed very heavy to me. I couldn't find a particular use case where this would bring any benefit, only cruft.

[ppedrot]

@JasonGross I have pushed a tweak that makes the API similar to your second proposal. Please tell me what you think about it.

[JasonGross]

LGTM

[JasonGross]

I agree, btw, that there is no use case where this altered API brings technical benefit, but I think the interface is conceptually more coherent and thus brings some benefit of clarity in most use cases

[ppedrot]

This needs an assignee. @JasonGross you might want to take it up?

[JasonGross]

Let me know if you want to merge the suggestion to CHANGES, and then I'll tell coqbot to merge

[ppedrot]

Changelog tweaked.

[JasonGross]

@coqbot merge

[JasonGross]

@coqbot merge now

[coqbot-app]

@JasonGross: You can't merge the PR because there is no kind: label.

[JasonGross]

@coqbot merge now