<div dir="ltr">Thanks Ulf. Maybe complicated is not entirely the right word.<div><br></div><div>If i use unify to return a value it is always being unquoted, so in order to do that i have to quote it first. That's the step that seemed odd to me. I already have the exact thing i need but it always has to be quoted and unquoted to escape TC. It feels a bit like i am working against the system. I don't know how this is implemented, but wouldn't this become slow if i want to return big things?</div><div><br></div><div>An emacs mode command to run TC computations would spare me some repetitive typing, though i think i can already use the evaluate command on something like '<span style="font-size:12.8px">unquote (runTC (countConstructors (quote Foo)))' to get the same result.</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">I do agree that this is not a huge issue. It took me a while to find the right method but once i had it it is obvious enough.</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">Yorick</span></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 8, 2016 at 9:09 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">I'm not sure I understand why you think your runTC is a complicated solution (it's certainly not an abuse of the unify function). Adding a built-in runTC and special handling for macros would surely be more complicated.<div><br></div><div>Something that's on my list of things to do is an Emacs mode command to run TC computations. This would make it a lot easier to debug tactics. Would that address your problems?</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Sat, Feb 6, 2016 at 5:26 PM, Yorick Sijsling <span dir="ltr"><<a href="mailto:yoricksijsling@gmail.com" target="_blank">yoricksijsling@gmail.com</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr">Hi everyone,<div><br></div><div>I'm experimenting with the new reflection stuff in 2.5.1. These changes are quite exciting!</div><div><br></div><div>I noticed that all the unquoting operations (unquote/unquoteDecl/unquoteDef) take a TC ⊤, making it hard to return results of a computation in this monad. Let's say we want to count the number of constructors of a datatype:</div><div><br></div><div>---</div><div><div>open import Prelude<br></div><div>open import Builtin.Reflection</div><div><br></div><div>data Foo : Set where</div><div> foo1 : Foo</div><div> foo2 : Foo</div><div><br></div><div>countConstructors : Name → TC Nat</div><div>countConstructors dt = length <$> getConstructors dt</div></div><div>---</div><div><br></div><div>Now i believe in an ideal situation one would have a way to run this computation and return the result:</div><div><br></div><div>---</div><div><div>-- test-countConstructors : runquote (countConstructors (quote Foo)) ≡ 2</div><div>-- test-countConstructors = refl</div></div><div>---</div><div><br></div><div>As it turns out, it is possible to abuse the unify function to return arbitrary results by quoting them to a Term first. So we can define a function which takes a TC A and gives us a tactic which puts the value in the hole:</div><div><br></div><div>---</div><div><div>runTC : ∀ {a} {A : Set a} → TC A → Tactic</div><div>runTC c hole =</div><div> do v ← c</div><div> =| `v ← quoteTC v</div><div> =| unify hole `v</div><div><br></div><div>test-countConstructors : unquote (runTC (countConstructors (quote Foo))) ≡ 2</div><div>test-countConstructors = refl</div></div><div>---</div><div><br></div><div>This is usable, but the notation is awkward. I used the new macro functionality to clean it up:</div><div><br></div><div>---</div><div><div>macro</div><div> countConstructors′ : Name → Tactic</div><div> countConstructors′ dt = runTC (countConstructors dt)</div><div><br></div><div>test-countConstructors′ : countConstructors′ Foo ≡ 2</div><div>test-countConstructors′ = refl</div></div><div>---</div><div><br></div><div>All of this took quite a while for me to figure out, so i thought it was worth sharing. But i also think this is a complicated solution to something which should be quite simple. Is this the right way to do it or am i missing something here?</div><div><br></div><div>Would it maybe make sense to have runTC as a built-in, and extend the macro's to allow result types of something else than TC ⊤ in which case runTC is used? I imagine something like this would be possible:</div><div><br></div><div>---</div><div><div>-- macro</div><div>-- countConstructors : Name → TC Nat</div><div>-- countConstructors dt = length <$> getConstructors dt</div><div><br></div><div>-- test-countConstructors : countConstructors Foo ≡ 2</div><div>-- test-countConstructors = refl</div></div><div>---</div><div><br></div><div>I would like to hear your opinions on this,</div><div><br></div><div>Yorick</div></div>
<br></div></div>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>