[Agda] Agda reflection overhaul

[Ulf Norell]

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/20160115/9bc936dd/attachment.html