Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-13 14:42:11 -0800 (Fri, 13 Jan 2006)
Revision: 8469
Log message:

      - Do pro-active normalization of the numerical expressions (so that they are
        normalized before they are duplicated). This is done by changing the
        annotation processor for all the hoas_lof/hoas_normalize resources.
      
      - substl coalescing (substl_substl_lof2) is not a part of the normalizeLofC
        (it has the exactly right style and it is wasteful to dedicate a separate
        sweepUpC to it).
      
      - Tried making the "constant reduction" more robust. In particular, when
        normalizeLofC performs a "constant reduction", it will now follow up by
        using reduceC to fully propagate the constant. I've removed Jason's "I
        believe they are too fragile" comment because I think it no longer applies.
        Also, moved the hd_lof rewrite into the "constant reduction" section (where
        it belongs).
      
      This reduces the THEORIES=all expansion time and #of primitive steps by >10%.
      

Changes  Path
+33 -34 metaprl/theories/itt/reflection/experimental/itt_hoas_lof.ml
+5 -5 metaprl/theories/itt/reflection/experimental/itt_hoas_normalize.ml
+20 -3 metaprl/theories/itt/reflection/experimental/itt_hoas_util.ml
+7 -11 metaprl/theories/itt/reflection/experimental/itt_hoas_util.mli