Is there a way to find what information the different fields used as part of template-coq stand for?

For example, in `one_inductive_body`

,

```
Record one_inductive_body : Type := Build_one_inductive_body {
(* Name of the type *)
ind_name : ident;
(* Type of the type itself? *)
ind_type : term;
(* Top allowed elimination sort *)
ind_kelim : sort_family;
(* Constructors. But why the nat *)
ind_ctors : list ((ident × term) × nat);
(* Projection functions? But not records, right * )
ind_projs : list (ident × term)
}.
```

Couldn't figure out the significance of `ind_projs`

and the `nat`

part for `ind_ctors`

.

Found some comments as part of the source in here.

And some that I couldn't entirely get hold of in coq's source in here..

Although I work with these types often and a lot, I can't tell you off the top off my head

My suggestion would be to look at the representation of `bool`

, `nat`

and `list`

to find out what the `nat`

ind `ind_ctors`

is for

And to do

```
Set Primitive Projections.
Record test := {field : Type}.
```

and check what happens in `ind_projs`

It certainly has to do something with records (which, internally, are just inductive types, there is no distinct kernel representation of records)

I think it's the primitive projections.

Are you aware of the "The MetaCoq Project" paper (https://hal.inria.fr/view/index/docid/2167423) @Julin S? It is a bit outdated, but I was able to find out what's going on by Ctrl+F ing through the paper. Even with the paper you'll still have to ask lots of questions, that's just the way how to learn MetaCoq at the moment :)

And some that I couldn't entirely get hold of

What does that mean?

comments at https://github.com/MetaCoq/metacoq/blob/6fc160af22be79cd61e1868dfe139ac4926f92c0/template-coq/theories/Environment.v#L129-L132 seem complete

Yannick Forster said:

Are you aware of the "The MetaCoq Project" paper (https://hal.inria.fr/view/index/docid/2167423) Julin S? It is a bit outdated, but I was able to find out what's going on by Ctrl+F ing through the paper. Even with the paper you'll still have to ask lots of questions, that's just the way how to learn MetaCoq at the moment :)

Yeah, thanks. I had been going through it. Started from there. :sweat_smile:

Gaëtan Gilbert said:

And some that I couldn't entirely get hold of

What does that mean?

No, the comments are fine. I just couldn't put a finger on it when trying to relate the definitions in the coq source to the template-coq structures.

For example, couldn't figure out which part of the coq version corresponded to the `ind_projs`

of template-coq.

Template-coq form:

```
Record one_inductive_body := {
ind_name : ident;
ind_type : term; (* Closed arity *)
ind_kelim : sort_family; (* Top allowed elimination sort *)
ind_ctors : list (ident * term (* Under context of arities of the mutual inductive *)
* nat (* arity, w/o lets, w/o parameters *));
ind_projs : list (ident * term) (* names and types of projections, if any.
Type under context of params and inductive object *) }.
```

Coq form:

```
type one_inductive_body = {
(** {8 Primitive datas } *)
mind_typename : Id.t; (** Name of the type: [Ii] *)
mind_arity_ctxt : Constr.rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
mind_arity : inductive_arity; (** Arity sort and original user arity *)
mind_consnames : Id.t array; (** Names of the constructors: [cij] *)
mind_user_lc : types array;
(** Types of the constructors with parameters: [forall params, Tij],
where the Ik are replaced by de Bruijn index in the
context I1:forall params, U1 .. In:forall params, Un *)
(** {8 Derived datas } *)
mind_nrealargs : int; (** Number of expected real arguments of the type (no let, no params) *)
mind_nrealdecls : int; (** Length of realargs context (with let, no params) *)
mind_kelim : Sorts.family; (** Highest allowed elimination sort *)
mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
mind_consnrealargs : int array;
(** Number of expected proper arguments of the constructors (w/o params) *)
mind_consnrealdecls : int array;
(** Length of the signature of the constructors (with let, w/o params) *)
mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
mind_relevance : Sorts.relevance;
(** {8 Datas for bytecode compilation } *)
mind_nb_constant : int; (** number of constant constructor *)
mind_nb_args : int; (** number of no constant constructor *)
mind_reloc_tbl : Vmvalues.reloc_table;
}
```

it's in the record info in the mutual body, not in the one_body

https://github.com/coq/coq/blob/e64a5adb4a5431ff084a4e11f57a9cac7a3bf519/kernel/declarations.ml#L147

https://github.com/coq/coq/blob/e64a5adb4a5431ff084a4e11f57a9cac7a3bf519/kernel/declarations.ml#L210

We don't document the correspondence anywhere I think, and it might be unintuitive / strange. But there is a good reason for lacking documentation as of today: it is not necessary to understand what's happening in the kernel to understand Template-Coq. That's precisely what makes Template-Coq so great: You don't have to dive into the Coq sources, you can look at the Template-Coq sources and interactive play around with quoting

Yannick Forster said:

And to do

`Set Primitive Projections. Record test := {field : Type}.`

and check what happens in

`ind_projs`

```
MetaCoq Quote Recursively Definition qtest := test.
Print qtest.
```

shows an empty list for `ind_projs`

even with `Set Primitive Projections.`

I think setting that option doesn't make any difference for this record (or I am doing something wrong).

```
([(MPfile ["Top"], "test",
InductiveDecl
{|
ind_finite := BiFinite;
ind_npars := 0;
ind_params := [];
ind_bodies := [{|
ind_name := "test";
ind_type := tSort
(Universe.from_kernel_repr
(Level.Level "Top.138", true) []);
ind_kelim := InType;
ind_ctors := [("Build_test",
tProd (nNamed "field")
(tSort
(Universe.from_kernel_repr
(Level.Level "Top.138", false) []))
(tRel 1), 1)];
ind_projs := [] |}];
ind_universes := Monomorphic_ctx
(LevelSetProp.of_list [Level.Level "Top.138"],
ConstraintSet.empty);
ind_variance := None |})],
tInd {| inductive_mind := (MPfile ["Top"], "test"); inductive_ind := 0 |} [])
: program
*)
```

Not that familiar with logic and type theory yet. :grimacing:

I think setting that option doesn't make any difference for this record (or I am doing something wrong).

It certainly should make a difference, for instance `Check fun x => eq_refl : x = {| field := field x |}.`

should succeed

This is weird, I was expecting something else. @Matthieu Sozeau, do you know what's going on?

Sorry!!!

It was something that I did.

I had set `Primitive Projections`

only *after* the record was defined. I had thought it would affect only the printing. Now it's showing values in the `ind_projs`

field.

Got this as output when corrected:

```
qtest' =
([(MPfile ["tst"], "test",
InductiveDecl
{|
ind_finite := BiFinite;
ind_npars := 0;
ind_params := [];
ind_bodies := [{|
ind_name := "test";
ind_type := tSort
(Universe.from_kernel_repr
(Level.Level "tst.56", true) []);
ind_kelim := InType;
ind_ctors := [("Build_test",
tProd (nNamed "field")
(tSort
(Universe.from_kernel_repr
(Level.Level "tst.56", false) []))
(tRel 1), 1)];
ind_projs := [("field",
tSort
(Universe.from_kernel_repr
(Level.Level "tst.56", false) []))] |}];
ind_universes := Monomorphic_ctx
(LevelSetProp.of_list [Level.Level "tst.56"],
ConstraintSet.empty);
ind_variance := None |})]%list,
tInd
{| inductive_mind := (MPfile ["tst"]%list, "test"); inductive_ind := 0 |}
[]%list)
: program
```

So it's showing the projections possible for the record type I suppose.

Indeed, that field is for the primitive projections. You might get a better idea of the meaning/shape of each field by looking at EnvironmentTyping.on_inductive: there are the typing invariants related to each field

Don't we need to understand what the individual fields in the record types used for template-coq stand for to use template-coq?

Just wondering if there's a 'shortcut' that I have not yet come across.

In the end, you indeed need to understand them to use them :) A shortcut would be to work on a "by need" basis: Just learn what they are doing when you need them. What Matthieu is suggesting is to learn what the fields are doing by looking at the typing invariants for each field. They will give you a better impression to what the fields are connected and what they need to fulfil

Last updated: Jul 24 2024 at 11:01 UTC