search

gmalecha / template-coq

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

ExtLib dependency for monads notations #33

Open aa755 opened 7 years ago

aa755 commented 7 years ago

I have written a monad that allows programming with TemplateCoq operations in Gallina. The goal is to have eventually enough primitive operations in the monad so that many plugins (e.g. paramcoq) can be written in Gallina:

https://github.com/aa755/template-coq/blob/dd8187b12e55cde7809da0433302750592db5eb1/theories/Ast.v#L99

Example usage: https://github.com/aa755/template-coq/blob/dd8187b12e55cde7809da0433302750592db5eb1/test-suite/demo.v#L160

If such a feature is of interest to this repo, I can submit a PR once the work is more polished. If so, would it be okay for Template-Coq to depend on Extlib? I would like to define an Extlib.Monad instance for this monad and use its notations. Extlib would likely not need to depend on Template-Coq, would it?

gmalecha commented 7 years ago

This is an interesting question. I'm not sure the right answer to it. While we haven't done it this far (due to the lack of reflection) it would be nice to generate definitions inside of extlib, e.g. Show instances and the like. This suggests one of two possible choices:

1/ make a template-coq core package that exposes the low level interface (this one) and another that depends on extlib and provides a higher level interface (which most clients will use) 2/ split extlib into smaller pieces and have template-coq only depend on a relatively small piece. (I've been thinking about pulling extlib apart for a while, but am not sure if it a good idea. It would mimic the structure of the Ocaml Core library)

I'm tempted to do both, but do you have thoughts on pros and cons? @mattam82 any thoughts?

The really great thing about opam is that installation remains easy even if things get broken up.

aa755 commented 7 years ago

(Sorry for closing and reopening .. accidentally hit that button.) Autogenerating Show instances in Extlib would be cool. Along the lines of 2/, the code for autogenerating them can be put in another package, something like Extlib-autogen. 1/ would then not be needed, but it don't see any disadvantage in 1/.

Some people may not like to have external plugins in their TCB. They can still use Extlib and avoid Extlib-autogen and Template-Coq.

gmalecha commented 7 years ago

Good point. Technically, the TCB of Coq is only minimal in the checker, so in theory this shouldn't be an issue, but I don't think very many people actually run the checker so I think you're right.

@aa755 Perhaps we should move this repository into the coq-ext-lib organization and make its sister repository there as well?

aa755 commented 7 years ago

Moving wouldn't be a problem for me.