[plt-dev] Associating metadata with modules

There are properties in the compiled file that tell us about a
module's exports. Would something like that work, if that mechanism
could be extended?

Robby

On Sun, Mar 7, 2010 at 2:15 PM, Carl Eastlund <cce at ccs.neu.edu> wrote:
> 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
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-dev
>