Stream: MetaCoq

Topic: Significance of template-coq record fields


view this post on Zulip Julin S (Jan 06 2022 at 10:56):

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..

view this post on Zulip Yannick Forster (Jan 06 2022 at 11:11):

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

view this post on Zulip Yannick Forster (Jan 06 2022 at 11:12):

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

view this post on Zulip Yannick Forster (Jan 06 2022 at 11:12):

And to do

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

and check what happens in ind_projs

view this post on Zulip Yannick Forster (Jan 06 2022 at 11:13):

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

view this post on Zulip Théo Winterhalter (Jan 06 2022 at 11:14):

I think it's the primitive projections.

view this post on Zulip Yannick Forster (Jan 06 2022 at 11:16):

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 :)

view this post on Zulip Gaëtan Gilbert (Jan 06 2022 at 11:17):

And some that I couldn't entirely get hold of

What does that mean?

view this post on Zulip Gaëtan Gilbert (Jan 06 2022 at 11:18):

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

view this post on Zulip Julin S (Jan 06 2022 at 11:26):

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:

view this post on Zulip Julin S (Jan 06 2022 at 11:26):

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.

view this post on Zulip Julin S (Jan 06 2022 at 11:26):

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;
  }

view this post on Zulip Gaëtan Gilbert (Jan 06 2022 at 11:28):

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

view this post on Zulip Yannick Forster (Jan 06 2022 at 11:29):

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

view this post on Zulip Julin S (Jan 06 2022 at 11:33):

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:

view this post on Zulip Gaëtan Gilbert (Jan 06 2022 at 11:36):

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

view this post on Zulip Yannick Forster (Jan 06 2022 at 13:03):

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

view this post on Zulip Julin S (Jan 06 2022 at 13:06):

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.

view this post on Zulip Julin S (Jan 06 2022 at 13:08):

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

view this post on Zulip Julin S (Jan 06 2022 at 13:09):

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

view this post on Zulip Matthieu Sozeau (Jan 06 2022 at 13:11):

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

view this post on Zulip Julin S (Jan 07 2022 at 04:17):

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.

view this post on Zulip Yannick Forster (Jan 07 2022 at 08:03):

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: Aug 11 2022 at 01:03 UTC