[plt-dev] Associating metadata with modules

For Hygienic ACL2, I need to associate a few pieces of metadata with
compiled modules.  These include the proof obligations of the module,
the exports of the module, and so forth.  I'm not sure where to
"stick" this information so that it will be available to clients (in
their transformer phase, should that be relevant).

It has been suggested to me that I add an export to the module with
the data I need, but this is inconvenient.  It means I eat up a point
in the module's namespace, and that I have to play "except-in" or
"rename-in" or "prefix-in" games with all of my module requires so
that this one common import doesn't clash between multiple
dependencies.

I have tried creating a hash table associating module names with
metadata, but it turns out that module names are a moving target.
They can be symbols or paths; for the modules I have tried, I get a
symbol back during the module's own transformer phase, but I get a
path back during its runtime phase and from either phase of another
module that depends on it.  (In all cases, I used the name of a
resolved module path.  In the module itself, I got this from a
variable reference; from a different module, I used the module name
resolver.)

Does anyone have a better suggestion for how to associate data with a
module, or for a reliable module identity to serve as a key in a hash
table?

Carl Eastlund