<div dir="ltr">Thanks everyone for the feedback. I have now merged the new-reflection branch into master. Check out the documentation here: <a href="http://agda.readthedocs.org/en/latest/language/reflection.html">http://agda.readthedocs.org/en/latest/language/reflection.html</a>.<div><br></div><div>An example of something that we couldn't do before can be found here <a href="https://github.com/UlfNorell/agda-prelude/blob/master/test/MonoidTactic.agda">https://github.com/UlfNorell/agda-prelude/blob/master/test/MonoidTactic.agda</a>. It's a simple monoid solver (the Hello World of proof by reflection) that uses instance arguments to figure the monoid.<div><br></div><div>As always, don't hesitate to suggest improvements or report bugs.<div><br></div><div>/ Ulf</div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jan 15, 2016 at 11:58 AM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>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.</div><div><br></div><div>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,</div><div><br></div><div> catchTC : ∀ {a} {A : Set a} → TC A → TC A → TC A</div><div> unify : Term → Term → TC ⊤</div><div><div> newMeta : Type → TC Term</div></div><div> freshName : String → TC QName<br></div><div> etc.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>/ Ulf</div><br><div>[1] <a href="https://github.com/UlfNorell/agda/tree/new-reflection" target="_blank">https://github.com/UlfNorell/agda/tree/new-reflection</a><br></div><div>[2] <a href="https://github.com/UlfNorell/agda/blob/new-reflection/doc/release-notes/2-5-1.txt#L383" target="_blank">https://github.com/UlfNorell/agda/blob/new-reflection/doc/release-notes/2-5-1.txt#L383</a><br></div><div><div>[3] <a href="https://github.com/UlfNorell/agda-prelude/tree/new-reflection" target="_blank">https://github.com/UlfNorell/agda-prelude/tree/new-reflection</a></div></div><div><br></div></div>
</blockquote></div><br></div>