Meta-programming library

[TheoWinterhalter]

We have been using this prelude for the MetaCoq tutorial and our MPRI course, and we've updated it to include nice combinators.

I open this draft to keep track of the consolidation efforts to make it part of the MetaCoq meta-programming library

[MevenBertrand]

In my logrel experiments I ended up writing some code to do locally nameless shenanigans (computing fresh names wrt a term, opening and closing a binder), I guess it would make sense to add it here too? :)

[TheoWinterhalter]

Sure!

[MathisBD]

@MevenBertrand for the locally nameless stuff it would make sense to wait a bit. I will be implementing unification in the next weeks which involves adding named contexts (and utility functions around named contexts) to template-coq :)

[MevenBertrand]

Ah, great! Then I won't do it myself. FYI, my current ugly code is here.

[MathisBD]

I integrated my changes :

• added traversal functions (all variants, including the exotic stuff such as map_term_with_binders and fold_termM)
• moved the specialized template monad notations to a module which users can import or not depending on their needs
• added a notion of packed_inductive and packed_constructor which are useful for metaprogramming

[MathisBD]

@MevenBertrand and @TheoWinterhalter if CI passes then I'm ready to merge

[TheoWinterhalter]

Thanks. One thing we need to discuss before merge is the use of the Monad class. With Yannick we purposefully removed dependency on monad_utils because then all error messages are that the monad was not found.

What is the stance of others? I see Mathis that you reverted some of our changes in that direction, is it a strong opinion? At least in the $run notations, for sure it seems dangerous, because it's very hard to debug.

[MathisBD]

I don't have a strong opinion yet :)
Monads are used in two places at the moment :

• in traversal functions (e.g. map_termM) : they really do belong here
• in dollar functions (e.g. $quote_def). When the input is incorrect we have a choice between : failing (tmFail) or returning a dummy result. I think the user experience is nicer if the functions fail. For instance $quote_def nat would fail because nat is not a constant, instead of returning a dummy term.

[MathisBD]

I don't get your comment "because then all error messages are that the monad was not found", can you explain ?

[TheoWinterhalter]

I meant relying on monad_utils and the type class resolution for the class Monad. I think we should avoid this, and you reverted our changes in that direction I think.

[MathisBD]

Oh I see, this is an issue since the $ functions are only Notationss, so elaboration happens later...

Would changing the $ functions so that they use tmBind and tmReturn explicitly be enough ?

[TheoWinterhalter]

Yeah, this is how they were before and I think this would be much better.
But then with @yforster we thought it's better not to use the monad class at all, because it never works well…

[MathisBD]

I reverted to tmBind/tmReturn. Still I think completely removing the template monad is not good idea, but I'm open to discussion. Also I moved the traversal functions to AstUtils.v (because of dependency considerations : this way we can use the traversal functions in template-coq itself.

[MathisBD]

The remaining failures seem to be due to faulty extraction (and orthogonal to the modifications we did in this branch). I don't know how to solve them, could someone have a look ?

[TheoWinterhalter]

I reverted to tmBind/tmReturn. Still I think completely removing the template monad is not good idea, but I'm open to discussion.

Maybe there is a misunderstanding because I think what you did is perfect. Thanks.

[TheoWinterhalter]

The errors seem completely unrelated to our changes… But maybe it's because now lib.ml is generated or something?

[MathisBD]

Some of the errors (those which are due to recent changes in coq-core or coq-stdlib) are also present in the main branch of metacoq, and I think I've solved them in this branch. For the extraction errors, I have no idea...

[TheoWinterhalter]

Maybe I shouldn't have made the PR against main? I don't know what the process these days?

[yforster]

Just changing the base branch here doesn't work, can you refactor a bit @MathisBD so we can file against 8.20?

[MathisBD]

I'm closing since this has been merged into coq.8-20.