Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-12 18:20:44 -0800 (Sun, 12 Feb 2006)
Revision: 8667
Log message:

      Working on .cmoz conversion.
      
      We discussed the following scheme for reflecting files:
      for an original (non-reflected) file foo.cmoz, we
      would generate a reflected file as foo_reflect.cmoz.
      
      However, the method has a problem, because the reflected
      theory includes ML code for resources.
      
      This is a pain.  Some options I see:
      
        1. Do not generate a separate file, but include the reflected
           code in the original foo.cmoz (with corresponding ML code in
           foo.cmo).
      
           Problem: it isn't modular, because you have to plan ahead
           for those files you want to reflect.  Also, you don't want the
           existence of theorems in the .cmoz to depend on how MetaPRL
           is configured.
      
           OTOH, if we _always_ generate reflected code, it is modular,
           with a cost.
      
        2. Provide tools:
      
              # Generates foo_reflect.cmi, foo_reflect.cmiz
              prlc --reflect foo_reflect foo.cmiz
      
              # Generates foo_reflect.cmo, foo_reflect.cmoz
              prlc --reflect foo_reflect foo.cmoz
      
           We would have to hack on omake:
              1. Make sure dependencies on _reflect files can be computed.
              2. Build the _reflect files automatically.
      
      I think option 2 is better _if_ it can be done.  The issue is that
      I'm not sure there is enough information in the .cm?z files to
      generate reflected theories.