Stream: MetaCoq

Topic: Adding new types to the quoting mechanism


view this post on Zulip Lennard Gäher (Dec 10 2020 at 10:16):

Hi, I'm working on a MetaCoq implementation of the Coq guardedness checker. As part of that, I have changed the MC representation of inductives to incorporate the recargs tree for inductive bodies (what corresponds to mind_recargs in the OCaml impl).
Of course, that also requires adding that to TemplateCoq's quoting mechanism. I've changed the quoting functions to quote the wf_paths when quoting inductive bodies.
However, I'm having trouble with adding the right references to the Coq term constructors in src/constr_reification.ml. Since the type wf_paths is available in theories/Ast.v under that name, I thought that let twf_paths = ast "wf_paths" in src/constr_reification.ml would be the right thing.
But when using this for quoting in Coq, I get Error: not found in table: metacoq.ast.wf_paths.

So in short, I suppose my assumptions about how the lookup mechanism for the Coq names works are wrong.
Can someone please push me in the right direction? Where do I need to look to find out the right names I need to use in src/constr_reification.ml to reference my new Coq type?

view this post on Zulip Gaëtan Gilbert (Dec 10 2020 at 10:22):

You probably need the Register command, search the code for other uses to see how it's used

view this post on Zulip Matthieu Sozeau (Dec 10 2020 at 11:04):

You need to register them in template-coq/theories/Constants.v indeed

view this post on Zulip Lennard Gäher (Dec 10 2020 at 13:21):

Thanks a lot, that made it work


Last updated: Oct 13 2024 at 01:02 UTC