[Agda] Reflection and Application terms

[Philipp Hausmann]

Hi all,

I'm currently trying to use Agda's Reflection to produce code fragments
at compile time, but the limited syntax
of Agda's Reflection makes this rather difficult. Most importantly,
there is no generalized application "app Term [Args]".

There is "def Name [Args]" for applying something to named definitions
and "var Index [Args]" for applying to de-bruijn indexed variables,
but applying to a Term in general ("app Term [Args]") is not possible
right now.

There is a clever trick which helps in some cases ("quote ((unquote t1)
(unquote t2))"), but that only works if t1 and t2 are closed terms.

Does anybody know a way to "fake" general application in Agda's
Reflection mechanism?

I also have looked into adding an additional general "app Term [Args]"
construct to Agda's Reflection mechanism, which seems to be
straightforward. But I'm not really sure if this is a good idea or not...
Agda changes:
https://github.com/phile314/agda/commit/80aa35b74eeee794b2f0b8b9dde5d6d32d4c9562
Example using this: https://gist.github.com/phile314/0a7711a9848b9a81f6f2

Does anybody know any tricks or solution for this?

All the best,
Philipp