<div dir="ltr">You want the ability to reduce Agda Terms, then? You could just see if you could manage to expose the internal Agda normalisation procedure as a function from Term to Term? I guess that would be a welcome addition?<div><br></div><div>Pepijn</div></div><div class="gmail_extra"><br><div class="gmail_quote">On 15 June 2015 at 20:36, Philipp Hausmann <span dir="ltr"><<a href="mailto:philipp.hausmann@314.ch" target="_blank">philipp.hausmann@314.ch</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#FFFFFF" text="#000000">
<div>Beta redexes are exactly what I want to
use.... :-(<br>
<br>
Back to the drawing board then...<span class="HOEnZb"><font color="#888888"><br>
<br>
Philipp</font></span><div><div class="h5"><br>
<br>
On 06/15/2015 08:15 PM, Ulf Norell wrote:<br>
</div></div></div><div><div class="h5">
<blockquote type="cite">
<div dir="ltr">Could be there is...
<div><br>
</div>
<div><a href="https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Reflection/Substitute.agda#L60-74" target="_blank">https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Reflection/Substitute.agda#L60-74</a><br>
</div>
<div><br>
</div>
<div>The syntax doesn't admit beta redexes, and reducing a beta
redex isn't guaranteed to terminate, so</div>
<div>you need to prove that the function term is 'safe' (i.e. is
not a lambda).</div>
<div><br>
</div>
<div>/ Ulf</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Mon, Jun 15, 2015 at 7:06 PM, Pepijn
Kokke <span dir="ltr"><<a href="mailto:pepijn.kokke@gmail.com" target="_blank">pepijn.kokke@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">Hey Philipp,
<div><br>
</div>
<div>You should be able to check whether you're dealing
with a defined name or a constructor using
Reflection.definition. That should set you well on your
way to defining the "app" function you're looking for.</div>
<div><br>
</div>
<div>In addition, I would check Ulf's prelude, if I were
you. There's a chance there's something in there that
already does this.</div>
<div><br>
</div>
<div>Regards,</div>
<div>Pepijn</div>
</div>
<div>
<div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On 15 June 2015 at 18:50,
Philipp Hausmann <span dir="ltr"><<a href="mailto:philipp.hausmann@314.ch" target="_blank">philipp.hausmann@314.ch</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi
all,<br>
<br>
I'm currently trying to use Agda's Reflection to
produce code fragments<br>
at compile time, but the limited syntax<br>
of Agda's Reflection makes this rather difficult.
Most importantly,<br>
there is no generalized application "app Term
[Args]".<br>
<br>
There is "def Name [Args]" for applying something
to named definitions<br>
and "var Index [Args]" for applying to de-bruijn
indexed variables,<br>
but applying to a Term in general ("app Term
[Args]") is not possible<br>
right now.<br>
<br>
There is a clever trick which helps in some cases
("quote ((unquote t1)<br>
(unquote t2))"), but that only works if t1 and t2
are closed terms.<br>
<br>
Does anybody know a way to "fake" general
application in Agda's<br>
Reflection mechanism?<br>
<br>
I also have looked into adding an additional
general "app Term [Args]"<br>
construct to Agda's Reflection mechanism, which
seems to be<br>
straightforward. But I'm not really sure if this
is a good idea or not...<br>
Agda changes:<br>
<a href="https://github.com/phile314/agda/commit/80aa35b74eeee794b2f0b8b9dde5d6d32d4c9562" rel="noreferrer" target="_blank">https://github.com/phile314/agda/commit/80aa35b74eeee794b2f0b8b9dde5d6d32d4c9562</a><br>
Example using this: <a href="https://gist.github.com/phile314/0a7711a9848b9a81f6f2" rel="noreferrer" target="_blank">https://gist.github.com/phile314/0a7711a9848b9a81f6f2</a><br>
<br>
Does anybody know any tricks or solution for this?<br>
<br>
All the best,<br>
Philipp<br>
<br>
_______________________________________________<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>
</blockquote>
</div>
<br>
</div>
</div>
</div>
<br>
_______________________________________________<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>
<br>
</div></div></div>
</blockquote></div><br></div>