[Agda] Reflection and Application terms

[Pepijn Kokke]

Hey Philipp,

You should be able to check whether you're dealing with a defined name or a
constructor using Reflection.definition. That should set you well on your
way to defining the "app" function you're looking for.

In addition, I would check Ulf's prelude, if I were you. There's a chance
there's something in there that already does this.

Regards,
Pepijn

On 15 June 2015 at 18:50, Philipp Hausmann <philipp.hausmann at 314.ch> wrote:

> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150615/2596c2c3/attachment.html