[plt-dev] Associating metadata with modules

Yes, if there were a way to add arbitrary properties to modules that
would be wonderful and greatly simplify my code.

Carl Eastlund

On Sun, Mar 7, 2010 at 8:33 PM, Robby Findler
<robby at eecs.northwestern.edu> wrote:
> 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