[Agda] Re: Agda reflection overhaul

[Ulf Norell]

Thanks everyone for the feedback. I have now merged the new-reflection
branch into master. Check out the documentation here:
http://agda.readthedocs.org/en/latest/language/reflection.html.

An example of something that we couldn't do before can be found here
https://github.com/UlfNorell/agda-prelude/blob/master/test/MonoidTactic.agda.
It's a simple monoid solver (the Hello World of proof by reflection) that
uses instance arguments to figure the monoid.

As always, don't hesitate to suggest improvements or report bugs.

/ Ulf

On Fri, Jan 15, 2016 at 11:58 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> I recently had the privilege to sit on David Christiansen's PhD committee,
> and thus had an excuse to take a closer look at what he's been doing with
> elaborator reflection in Idris. Basically what he's done is expose an
> interface to the proof engine to Idris metaprograms. It is very cool and
> lets you do things like backtracking and generating helper functions in
> tactic scripts. So, obviously, I had to steal it.
>
> It's all implemented in a branch on my Agda fork [1] and you can look at
> the release notes here [2]. Briefly, what I've done is add a new primitive
> monad TC with a bunch of primitive operations corresponding to operations
> on TCM in the Agda implementation. For instance,
>
>   catchTC : ∀ {a} {A : Set a} → TC A → TC A → TC A
>   unify : Term → Term → TC ⊤
>   newMeta : Type → TC Term
>   freshName : String → TC QName
>   etc.
>
> The unquote and unquoteDecl/Def primitives then expects TC computations
> instead of pure values, which enables a lot more interesting metaprograms
> than what we had before. A nice side-effect is that I could get rid of the
> reflection primitives (quote-goal etc) from the reflected Term data type.
>
> The idea is that we can get rid of most of the old primitives (quoteGoal,
> quoteContext, tactic) since that functionality is provided by the TC
> operations.
>
> I have updated agda-prelude [3] to the new framework and it seems to work,
> but I would be interested in feedback from people doing lots of reflection
> stuff (you know who you are) before merging this into master.
>
> / Ulf
>
> [1] https://github.com/UlfNorell/agda/tree/new-reflection
> [2]
> https://github.com/UlfNorell/agda/blob/new-reflection/doc/release-notes/2-5-1.txt#L383
> [3] https://github.com/UlfNorell/agda-prelude/tree/new-reflection
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160128/0f857781/attachment.html