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 <c...@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 > _________________________________________________ For list-related administrative tasks: http://list.cs.brown.edu/mailman/listinfo/plt-dev
