[Agda] Mapping QNames to module names?

[Ulf Norell]

On Mon, Oct 3, 2011 at 6:26 PM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:

> A question about internal compiler gore...
>
> Given an Agda QName q, is there a way inside the compiler to find the name
> of the top-level module which contains q's definition? For example:
>
>  module A.B where
>    module C.D where
>      E = ...
>
> 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?
>

There isn't an easy way that I can think of, but

qnameModule will give you A.B.C.D (as I'm sure you know). You can then
compare that against stCurrentModule and stImportedModules (in the TCState)
looking for a prefix.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111003/03978eae/attachment.html