[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