[Agda] Expose more of Agda to reflection?

[Jesper Cockx]

I don't have much to say about exposing rewrite to the reflection, but I do
have a warning: the module Agda.TypeChecking.Rewriting is *not* for
checking functions that use the 'rewrite' keyword, but rather for a new
(and experimental) feature for adding user-defined rewrite rules to the
evaluator via {-# REWRITE ... #-} pragmas. For the code handling the
'rewrite' keyword, you can take a look at the checkRHS function in
Agda.TypeChecking.Rules.Def.

cheers,
Jesper

On Sun, Jan 31, 2016 at 8:53 PM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> Via reflection, it currently isn't straightforward to construct an agda
> function that invokes a rewrite. Exposing Agda's rewriting machinery to
> reflection would make this much easier. (Another neat idea is to expose
> agsy!) On the other hand, the exact same algorithms could be reproduced in
> the Agda language and it might be advisable to keep the reflection
> interface clean, especially considering that work done by "rewrite" or agsy
> might change in the future.
>
> Am I correct that Agda.TypeChecking.Rewriting can now be exactly
> reproduced in Agda? I'm studying the algorithm and would love to know that
> the path ahead of me is clear.
> --
> Martin Stone Davis
>
> Postal/Residential:
> 1223 Ferry St
> Apt 5
> Eugene, OR 97401
> Talk / Text / Voicemail: (310) 699-3578 <3106993578>
> Electronic Mail: martin.stone.davis at gmail.com
> Website: martinstonedavis.com
>
> _______________________________________________
> 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/20160201/f4532d2a/attachment.html