Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-14 18:49:24 -0800 (Tue, 14 Feb 2006)
Revision: 8699
Log message:

      Added the template for reflecting theories from the .cmoz file.
      The only thing handled at the moment are the "extends" directives.
      
      The reflected theory for a theory Foo is named Reflect_foo.
      
      Whew, this wasn't easy.
      
         - Filter_cache_fun has an issue with loading "summarized"
           modules.  A "summarized" module is formed when a module
           is loaded.  If another "extends" for that theory is
           encountered, then the module is loaded from the
           summary.  In other words, the file is cached.
      
           Unfortunately, this is very damaged.  The only thing
           included from a cached file is the opnames.
           The other stuff, like resources and grammars, are ignored.
      
           This should be fixed.  In the meantime, I added a
           "reset_hack" function that resets the cache.  This is
           expensive, and should be removed asap.
      
         - For the moment, I'm hand-coding the dependencies for
           reflected files.
      
           Unfortunately, this is broken.  If you add an explicit
           dependency to theories/foo/OMakefile.  For example,
           the following dependency seems like it should work.
      
               reflect_x.cmoz: x.cmoz
      
           However reflect_x.cmoz will be compiled _without_
           OCAMLINCLUDES being defined to include THEORY_DEPS.
           In fact, it won't even include meta/base:(
      
           Again, this should be fixed.