Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-11 13:32:26 -0800 (Wed, 11 Jan 2006)
Revision: 8455
Log message:

      Modifying a bit the reduce annotation approach that I've added in the previous
      commit.
      
      Now the reduce annotations perform the following check on all the rewrites
      (regardless of whether they are conditional or not) - if a SO var will be
      duplicated by a rewrite (i.e. it appears more than once in the
      "contractum+assumptions"), then the reduceC will be called on the
      corresponding subterms before the rewrite is applied.
      
      For example,
      
      interactive_rw foo_reduce {| reduce |} :
         'a in footype -->
         'b in footype -->
         'c in footype -->
         foo{'a;'b;'b;'c;'d;'e} <--> foobar{'a;'b;'d;'d;'e}
      
      will add
         addrC [1] reduceC thenC addrC [2] reduceC thenC addrC [3] reduceC thenC
         addrC [5] reduceC thenC foo_reduce
      
      (the rewrite will duplicate 'a, 'b and 'd, so those are normalized
      before-hand).