[Agda] Re: examples of tactics via reflection

[Dan Licata]

On Apr15, Nils Anders Danielsson wrote:
> On 2009-04-15 02:38, Dan Licata wrote:
> >
> >It would be nice for these sorts of things if Agda provided a quotation
> >datatype representing the syntax of Agda programs, along with an unquote
> >function.
> 
> Is unquote the construction which takes arbitrary program text and turns

What I meant by 'unquote' was the opposite: the function that takes a
representation to its meaning; e.g.

unquote : {A : Set} -> Rep Gamma A -> ([ Gamma ] -> [ A ])

As a first cut, I wasn't going to go so far as to suggest something
scary like quote.

You could roll your own Rep type, but it would be nice if definition
names, datatypes, etc. automagically had corresponding Rep formers, so
they didn't have to be treated as parameters in Gamma (which would make
the substitutions [ Gamma ] fairly large and tedious to write).  

> We have discussed adding a reflection mechanism before. The main issue
> is coming up with a nice representation. Should it be well-typed? How
> should variables be handled?

Agreed.  I'm hoping some support for variable binding will be helpful
here (but I need to get the dependently typed case to work, first).

-Dan