[Agda] Mapping QNames to module names?

[Alan Jeffrey]

I'm currently running through stImportedModules looking for a prefix, 
but that fails (er, currently crashing the --js compiler) in the case 
where a name is used without its defining module being imported.

AFAICT, I'd have to run through all the prefixes, looking to find a 
prefix ms.n such that module m is a top-level module which defines n, 
which seems tricky, and possibly expensive. Oh, and I'm having to do 
this *every time* a name is emitted.

A.

On 10/03/2011 12:51 PM, Ulf Norell wrote:
>
> On Mon, Oct 3, 2011 at 6:26 PM, Alan Jeffrey <ajeffrey at bell-labs.com
> <mailto: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