<div dir="ltr"><div>On Wed, Aug 14, 2013 at 11:35 AM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br></div><div class="gmail_extra">
<div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Andrea,<br>
<br>
this feature is called "display form", and you can start looking in Syntax/Translation/<u></u>InternalToAbstract.hs<br>
<br></blockquote><div><br></div><div>Thanks, I had reached that module but was a bit lost, knowing about "display form" seems to help.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Anyhow, I think the discrepancy between Qualified and Unqualified is unwanted and deserves a bug report. There are some bugs on the tracker on "display form problems" already (most should be fixed).<br>
<br></blockquote><div><br></div><div>Ah, yes, there's issue 657 which is pretty much my second example, my first one seems unreported though, I guess I'll open another issue.</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Are you using Agda 2.3.2 or the darcs version?<br>
<br></blockquote><div><br></div><div>I'm using the darcs version, in fact I was referring to the goals I get from C-u C-u C-c C-t.</div><div><br></div><div>Thanks again,</div><div>Andrea</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Cheers,<br>
Andreas<div><div class="h5"><br>
<br>
On 14.08.13 7:31 AM, Andrea Vezzosi 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">
Hi all,<br>
<br>
making extensive use of parametrized modules and records, I'm wondering<br>
what's the proper mental model to predict how the normal forms of<br>
applied field selectors will show up, or maybe a summary of how this<br>
feature is implemented and where to look for it in the source.<br>
<br>
My question is general, but I'll also add an example for concreteness:<br>
<br>
module Use where<br>
<br>
postulate<br>
A : Set<br>
I : Set<br>
<br>
module R (_ : I) where<br>
postulate<br>
f : A<br>
<br>
postulate<br>
r : I<br>
X : I -> I<br>
Q : A -> Set<br>
<br>
module Qualified where<br>
K = X r<br>
open R K<br>
foo : Q f<br>
foo = { }0 -- normal form: Q (R.f (X r))<br>
module UnQualified where<br>
open R (X r)<br>
<br>
foo : Q f<br>
foo = { }1 -- normal form: Q f<br>
<br>
It's fairly counterintuitive that going through a simple definition like<br>
K alters the result, is it because we've gone through a reduction<br>
expanding K during normalization? But, as I said, I've little intuition<br>
over the whole issue.<br>
<br>
By the way, I've used the terms "qualified" and "unqualified" but the<br>
concern is really about not showing the parameters which I've opened the<br>
module with.<br>
<br>
My use cases tend to also include some rerouting of parameters that<br>
might make the reconstruction of the unqualified form harder:<br>
<br>
module X {A} {B} = Product (products A B)<br>
open X<br>
<br>
at this point we usually get normal forms like<br>
`Product.someField (products A B) ...` rather than `someField ...` which<br>
is especially unreadable for mixfix operators because of how the value<br>
of the record takes the place of the first underscore in the name.<br>
<br>
<br>
Thanks,<br>
Andrea<br>
<br>
<br></div></div>
______________________________<u></u>_________________<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" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br><span class="HOEnZb"><font color="#888888">
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</font></span></blockquote></div><br></div></div>