[Agda] Mapping QNames to module names?

[Nicolas Pouillard]

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?

No idea...

But this made me think of the reflection API.

Given that QName represents only globally defined names I see no trouble in
allowing a primitive like:

splitQName : QName -> List String

Or even simpler showQName : QName -> String and you then split on dots.

Best regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr