Stream: MetaCoq

Topic: Constructing Records and Classes


view this post on Zulip Yakir Forman (Jul 06 2023 at 14:14):

I'm trying to explore the possibility of using Template Coq functions such as tmMkDefinition to construct Records and/or Classes. I can construct an inductive with a single constructor and all the field projections. Is there a way using MetaCoq to better mimic what Coq does when a Record is defined (e.g., allowing the projections to be using the field syntax)? Or is this the best that can be done?

view this post on Zulip Yannick Forster (Jul 06 2023 at 14:16):

I don't fully understand the question I think. Are you saying the records defined using MetaCoq and records defined manually in Coq behave differently?

view this post on Zulip Yakir Forman (Jul 10 2023 at 16:48):

I can use tmMkInductive' to construct an inductive with a single constructor which has the same "internal structure" as a Coq-defined record, but if I run Print, it prints as an Inductive and not as a Record. Similarly, the field projections aren't automatically defined; I can define them myself using MetaCoq, but the record.(field) notation won't work.

view this post on Zulip Paolo Giarrusso (Jul 10 2023 at 21:51):

Potentially relevant bit in the Coq kernel: https://github.com/coq/coq/blob/315590487491821a8ff285f5e47415dca7827d35/kernel/declarations.mli#L142

view this post on Zulip Paolo Giarrusso (Jul 10 2023 at 22:09):

More directly relevant: https://github.com/MetaCoq/metacoq/blob/943cc72bd12ab41d1f67af96f5744c32e40338bf/erasure/theories/EAst.v#L122; this is used in https://github.com/coq/coq/blob/315590487491821a8ff285f5e47415dca7827d35/kernel/indtypes.ml#L580

view this post on Zulip Yannick Forster (Jul 10 2023 at 22:11):

EAst shouldn't be relevant, the parts related to the template monad will be in TemplateCoq.Ast

view this post on Zulip Paolo Giarrusso (Jul 10 2023 at 22:11):

IIUC, you'd need mind_entry_record := Some None to get a (non-primitive) record, and Some (Some ...) for primitive records?

view this post on Zulip Yannick Forster (Jul 10 2023 at 22:12):

(EAst and Ast are similar, but EAst is after type and proof erasure)

view this post on Zulip Paolo Giarrusso (Jul 10 2023 at 22:13):

Thanks, https://github.com/MetaCoq/metacoq/blob/943cc72bd12ab41d1f67af96f5744c32e40338bf/template-coq/theories/Ast.v#L736 then?

view this post on Zulip Yannick Forster (Jul 10 2023 at 22:13):

Yes, that looks right

view this post on Zulip Yakir Forman (Jul 13 2023 at 17:03):

Thank you!


Last updated: Jul 23 2024 at 20:01 UTC