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: Oct 13 2024 at 01:02 UTC