[Agda] Mapping QNames to module names?

[Ulf Norell]

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

> 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.


Try looking at the stVisitedModules instead of the imported modules. You
shouldn't have to worry about whether the module you find defines the thing,
if it has the right name it does. Just looking through the names of all
top-level modules for each name you have to emit shouldn't be a problem.

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