[Agda] Reflection and Application terms

[Nicolas Pouillard]

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
>

-- 
Best regards,
-- NP