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
