<br><div class="gmail_quote">On Mon, Oct 3, 2011 at 6:26 PM, Alan Jeffrey <span dir="ltr">&lt;<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">

A question about internal compiler gore...<br>
<br>
Given an Agda QName q, is there a way inside the compiler to find the name of the top-level module which contains q&#39;s definition? For example:<br>
<br>
  module A.B where<br>
    module C.D where<br>
      E = ...<br>
<br>
Given a use of A.B.C.D.E, I need to be able to extract A.B (since this is the JS module which contains the definition of C.D.E). Is there a reliable way to do this?<br></blockquote><div><br></div><div>There isn&#39;t an easy way that I can think of, but</div>

<div><br></div><div>qnameModule will give you A.B.C.D (as I&#39;m sure you know). You can then compare that against stCurrentModule and stImportedModules (in the TCState) looking for a prefix.</div><div><br></div><div>/ Ulf</div>

</div>