[racket-dev] Module metadata

I would like to associate metadata with a module based on its
expansion.  In my case, I want the Dracula language to be able to
construct an s-expression representing an ACL2 proof obligation at
phase 1, associate it with the module, and have the Dracula tool in
DrRacket extract the proof obligation at phase 0 so it can send it to
ACL2.  In another case, someone on the IRC channel wants to associate
documentation with the exports of a module.  Again, this information
is constructed at phase 1, but might be read at some arbitrary other
phase by another tool.

Is there a way to do this?  I have not been able to find one.  We
currently have various metadata associated with modules, such as the
#:info and #:language-info options in syntax/module-reader, but those
come from the reader.  The metadata is constructed prior to expansion.
 Is it possible to add a similar channel for post-expansion metadata
associated with modules?

Carl Eastlund