[Agda] Reflection and Application terms

[Pepijn Kokke]

You want the ability to reduce Agda Terms, then? You could just see if you
could manage to expose the internal Agda normalisation procedure as a
function from Term to Term? I guess that would be a welcome addition?

Pepijn

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

>  Beta redexes are exactly what I want to use.... :-(
>
> Back to the drawing board then...
>
> Philipp
>
>
> On 06/15/2015 08:15 PM, Ulf Norell wrote:
>
> 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/fb088092/attachment.html