[Agda] More powerful quoting & reflection?

[Paul van der Walt]

Dear readers,

I am currently looking at what neat tricks can be done with the
new reflection API, and something I would like to be able to do
(inspired by the same thing using Template Haskell)
automatically generate embedding & projection functions for a
sum-of-products generic programming approach, given some data
definition.

It seems the Reflection module contains functions suggestively
named `constructors`, for example, but I don't know how to use
them, and they're not (yet) documented. Does anyone know the
status of these features? Are they usable yet? Also, can I
create (/modify) a function programatically then splice it back?

Thanks in advance for the pointers,

Paul van der Walt
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 836 bytes
Desc: Digital signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120621/73974b71/attachment.bin