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 <ro...@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 <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
