<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jan 15, 2016 at 2:58 PM, Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div>Hi Ulf,<br></div><div><br>This looks very nice and useful, I'm looking forward to experimenting with the new features when I have time. Meanwhile, I tried to convert some of my code that uses reflection a lot, here are my remarks:<br><br></div>- I don't really understand how I would use extendContext and inContext, can you give an example?<br></div></div></div></div></div></blockquote><div><br></div><div>See Tactic.Nat.Induction for an example (<a href="https://github.com/UlfNorell/agda-prelude/blob/new-reflection/src/Tactic/Nat/Induction.agda#L40">https://github.com/UlfNorell/agda-prelude/blob/new-reflection/src/Tactic/Nat/Induction.agda#L40</a>). When you create a new meta (newMeta) you get a term valid in the current context, and inferType and checkType does checking relative to the current context.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div dir="ltr"><div><div><div><div></div>- Since typeError expects a String, maybe it would be useful to have some functions for pretty-printing terms/types? Or alternatively we could have a richer type for error messages.<br></div></div></div></div></blockquote><div><br></div><div>I'm going for the latter. I have an implementation of an error message type with string and term constructors that I did before the current overhaul. I just need to merge it.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div dir="ltr"><div><div><div></div><div>- There seems to be a problem with either unquoteDef (expects an argument of type TC T) or deriveEqDef in the prelude (returns a TC (List Clause)).<br></div></div></div></div></blockquote><div><br></div><div>You have to use defineFun:</div><div><br></div><div> unquoteDef myEq = defineFun myEq =<< deriveEqDef (quote SomeType)</div><div><br></div><div>I only did the minimal changes necessary to get agda-prelude working. With the new framework many things can be cleaned up and made more useful.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div dir="ltr"><div><div><div></div><div>- Some functions that used to be pure are now integrated into the TC monad, which causes a lot of my code to become monadic as well. I'm mainly talking about getType (previously typeOf), getDefinition (previously definitionOf), getParameters and getConstructors. Would it be possible to keep these functions pure?<br></div></div></div></div></blockquote><div><br></div><div>Short answer: no. They were already not quite pure. For instance, you could call definitionOf in a mutual block before you actually have the definition, but depending on when the call was actually evaluated you may or may not get the full definition. With the new API things are even worse since you can create new definitions on the fly (with freshName, declareDef and defineFun). I guess the parameter and constructor functions could still be pure, but it felt more consistent to put everything in the monad.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div dir="ltr"><div><div><div></div><div>- One thing I noticed when converting my pure code to monadic code (probably has nothing to do with this change): you cannot combine two monadic computations at different universe levels (at least with the definition of monad in the prelude). This is rather annoying, especially since I don't know a workaround.<br></div></div></div></div></blockquote><div><br></div><div>There is PMonad type class with a bind function _>>=′_ that accepts things at different levels. I forgot to make TC an instance though.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div dir="ltr"><div><div><div></div><br></div>cheers,<br></div>Jesper<br><div><div><br>ps: A funny thing happened last year when the agda repository was deleted and recreated on github, causing all forks to use masondesu/agda as their new base. I saw this happened with your fork as well. Unfortunately, the only solution I found was to delete and recreate my fork of agda/agda on github.<br></div></div></div></blockquote><div><br></div><div>Huh, I hadn't noticed that. I guess I should sort that out at some point :).</div><div><br></div><div>/ Ulf</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div dir="ltr"><div><div></div></div></div><div class=""><div class="h5"><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:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style: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>
</div></div></blockquote></div><br></div></div>