search

gmalecha / template-coq

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

unquoting changes Prop to Set #28

Closed aa755 closed 7 years ago

aa755 commented 7 years ago

https://github.com/aa755/template-coq/blob/coq-8.5/test-suite/bugUnquote1.v

aa755 commented 7 years ago

Indeed, there was a bug in the unquote_sort function. Prop and Set were interchanged:

https://github.com/aa755/template-coq/commit/70bfe07cbbe3b6f75647b12ed84b846e400feb60?diff=unified#diff-13ca600630240523dd50938ebdafd8a9L538

gmalecha commented 7 years ago

Can you submit a pull request?

gmalecha commented 7 years ago

Ah, thanks! Are you using the unquoting code anywhere?

On Wed, Nov 16, 2016, 5:14 PM Abhishek Anand notifications@github.com wrote:

Closed #28 https://github.com/gmalecha/template-coq/issues/28.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/gmalecha/template-coq/issues/28#event-861883828, or mute the thread https://github.com/notifications/unsubscribe-auth/AASlV4iqsOaz2rx-nxmCCaMzBBztZUsMks5q-4BXgaJpZM4Ky-Ik .

  • gregory malecha gmalecha.github.io
aa755 commented 7 years ago

Not yet. But I plan to. I want to develop something like the paramcoq plugin using template-coq. To be able to do that, I think template-coq needs to be extended in 2 ways:

1) Ability to reflect inductive declarations. I have started implementing it in my fork. I have defined a coq datatype in AST.v, and started working on the corresponding unquote function: https://github.com/aa755/template-coq/blob/1d75c3f602c81fd8fee201d22a5a482d99c013a9/theories/Ast.v#L71 https://github.com/aa755/template-coq/blob/1d75c3f602c81fd8fee201d22a5a482d99c013a9/src/reify.ml4#L819

Once it is complete, I would submit a PR.

2) To generate the abstraction theorem of some object, the paramcoq plugin often needs to create several definitions/inductives . One way to achieve this would be to have a "Make Definitions" command . I think a more general way would be to define a monad in Ast.v with operations corresponding to "Make Definition", "Make Inductive", and perhaps also operations to find and read declared objects, hint databases etc. I am not sure whether the "run" function of such a monad can be defined in reify.ml.

Any comment/suggestion is welcome.