Stream: MetaCoq

Topic: Working with PCUICAst


view this post on Zulip Jason Gross (Oct 17 2022 at 10:57):

I wrote a function quote_term : MetaCoq.Template.Ast.term -> MetaCoq.Template.Ast.term which adds a level of quotation (https://github.com/JasonGross/metacoq-lob/blob/e9703eee66f2431654d659bf8d7b8bb63fc99e91/theories/QuoteGround.v#L100). I'm looking to do the same thing with MetaCoq.PCUIC.PCUICAst.term instead (and eventually with complete typing judgments; I'm working up to Lob's theorem). Is there any tactic / tactic monad / notation support for using the PCUIC AST, or do I have manually map everything though TemplateToPCUIC.trans or something?

view this post on Zulip Jason Gross (Oct 18 2022 at 09:56):

Is there a version of the template monad's tmQuote (and tmUnquote) that works on PCUIC?

view this post on Zulip Matthieu Sozeau (Oct 18 2022 at 11:04):

Nope, you have to go through the translation

view this post on Zulip Matthieu Sozeau (Oct 18 2022 at 11:04):

But that's fairly easy to program I guess

view this post on Zulip Jason Gross (Oct 18 2022 at 13:38):

The translation requires access to a PCUICProgram.global_env_map. Is there an easy way to manifest one with all the required inductives?

view this post on Zulip Jason Gross (Oct 18 2022 at 13:38):

(I'm currently in the process of trying to write a version of trans that doesn't take such a map and instead lives inside the template monad. (Perhaps this would be worth merging upstream, if there's not already an easy alternative?))

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 12:22):

You can easily build a global_env_map out of a global env using PCUICProgram.build_global_env_map

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 12:22):

I guess you found that


Last updated: Feb 04 2023 at 03:30 UTC