[Agda] Reflection and Application terms

[Philipp Hausmann]

Took me some time to try your suggestion, but it works perfectly :-)

Thanks for the idea.

Philipp

On 06/20/2015 10:07 PM, Nicolas Pouillard wrote:
> Can't you fake it by producing applications a definition such as ($)?
>
> app : (t u : Term) → Term
> app t u = def (quote _$_) (arg (arg-info visible relevant) t ∷
> arg (arg-info visible relevant) u ∷ [])
>
> Of course this is not full proof and will depend on your choice of
> type for _$_,
> the dependent version in the stdlib will then take 4 implicit
> arguments...
>
> On 06/15/2015 09:05 PM, Pepijn Kokke wrote:
>> 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
>> <mailto: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 <mailto: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 <mailto: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 <mailto:Agda at lists.chalmers.se>
>> >             https://lists.chalmers.se/mailman/listinfo/agda
>> >
>> >
>> >
>> >         _______________________________________________
>> >         Agda mailing list
>> >         Agda at lists.chalmers.se <mailto: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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20150702/68df1008/signature.bin