search

gmalecha / template-coq

Reflection library for Coq
MIT License
12 stars 0 forks source link

A monad for programming with template-coq operations #37

Open aa755 opened 7 years ago

aa755 commented 7 years ago

See Ast.TemplateMonad and some example programs in demo.v There are 2 more enhancements/fixes:

  1. This monad has a more informative quote function (Ast.tmQuote) for quoting inductives (fixes #17).
  2. Now, the denote_term function unquotes constants and fixpoints as well.
gmalecha commented 7 years ago

@aa755 What is the current status of this? Is it ready to review or are there more things that you are looking at?

gmalecha commented 7 years ago

The quoting operation here is beginning to look a lot more involved than I thought that it would. There also seems to be a lot of overlap with MetaCoq in terms of implementation and operation (the reification plugin in MirrorCore also works in a similar way). I'm wondering if some of this functionality should be merged into that project.

aa755 commented 7 years ago

Thanks for those pointers. Indeed, now I notice that some operations overlap with MetaCoq. I thought MetaCoq's monad was mainly for ltac-style proof automation, whereas I am mainly interested in program transformations. I will sometime take a closer look at MetaCoq and MirrorCore.

I currently don't plan to add any more operations to the monad in this PR. It seems that the current operations suffice for my project. The only thing that I am missing now is the ability to properly reify and reflect universes.

gmalecha commented 7 years ago

@aa755 Do you mind if I write a PR on top of this with a few cosmetic changes?

aa755 commented 7 years ago

Feel free to use the code here in any way you wish. I agree with all the changes you suggested -- thanks. However, I have been very busy lately because of some deadlines. It may take me a while to address all those changes.

gmalecha commented 7 years ago

Completely understandable given the time of year.