[Agda] Mapping QNames to module names?

Alan Jeffrey ajeffrey at bell-labs.com
Mon Oct 3 21:33:16 CEST 2011


Ah good point, finding the longest top-level visited module name which 
is a prefix of the qname should do the trick.

A.

On 10/03/2011 02:14 PM, Ulf Norell wrote:
> On Mon, Oct 3, 2011 at 8:19 PM, Alan Jeffrey <ajeffrey at bell-labs.com
> <mailto: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


More information about the Agda mailing list