[Agda] Reflection and Application terms

[Ulf Norell]

Could be there is...

https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Reflection/Substitute.agda#L60-74

The syntax doesn't admit beta redexes, and reducing a beta redex isn't
guaranteed to terminate, so
you need to prove that the function term is 'safe' (i.e. is not a lambda).

/ Ulf

On Mon, Jun 15, 2015 at 7:06 PM, Pepijn Kokke <pepijn.kokke at gmail.com>
wrote:

> 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
>>
>
>
> _______________________________________________
> 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/7dae89bb/attachment.html