tests/rewriting.pcc

   1 //////////////////////////////////////////////////////////////////////////////
   2 //  Testing the rewriting features.
   3 //////////////////////////////////////////////////////////////////////////////
   4 #include <new.h>
   5 #include <iostream.h>
   6
   7 int balance;     // number of allocation - number of deallocation
   8 int div_by_zero; // number of division by zeros
   9
  10 //////////////////////////////////////////////////////////////////////////////
  11 // We'll use reference counting with rewriting.
  12 // The operators new and delete are redefined to keep track of
  13 // the number of allocations and deallocation.
  14 // This is for demonstration use only.  In practice, it is
  15 // unnecessary to redefine these operators if the normal ones
  16 // suffice.
  17 //////////////////////////////////////////////////////////////////////////////
  18 class MEM {
  19 public:
  20    inline void * operator new (size_t n)
  21       { balance++; return new char [n]; }
  22    inline void   operator delete (void * x)
  23       { balance--; delete [] ((char*)x); }
  24 };
  25
  26 //////////////////////////////////////////////////////////////////////////////
  27 //  Define the datatypes EXP and EXP_LIST.  Currently, rewriting can only be
  28 //  performed on datatypes(and not views) in Prop.  If replacement is
  29 //  to be performed on a datatype, then it should be declared using
  30 //  the ``rewrite'' qualifier.
  31 //
  32 //  We'll extend these datatypes from class MEM so that it'll inherit
  33 //  MEM's operator new and delete.
  34 //////////////////////////////////////////////////////////////////////////////
  35 datatype EXP : MEM :: traced rewrite = om
  36                                      | num (int)
  37                                      | var (char)
  38                                      | add (EXP, EXP)
  39                                      | sub (EXP, EXP)
  40                                      | mul (EXP, EXP)
  41                                      | div (EXP, EXP)
  42                                      | exp_list (EXP_LIST)
  43 //////////////////////////////////////////////////////////////////////////////
  44 //  A list of expressions.
  45 //////////////////////////////////////////////////////////////////////////////
  46 and EXP_LIST : MEM :: traced rewrite = #[]
  47                                      | #[ EXP ... EXP_LIST ]
  48                                      ;
  49
  50 //////////////////////////////////////////////////////////////////////////////
  51 //  Define a method that prints an expression.  This is a simple
  52 //  inductive definition
  53 //////////////////////////////////////////////////////////////////////////////
  54 ostream& operator << (ostream& f, EXP_LIST l);
  55 ostream& operator << (ostream& f, EXP e)
  56 {  match (e) {
  57       om:          { return f << "om"; }
  58    |  num i:       { return f << i; }
  59    |  var v:       { return f << v; }
  60    |  add(a,b):    { return f << '(' << a << " + " << b << ')'; }
  61    |  sub(a,b):    { return f << '(' << a << " - " << b << ')'; }
  62    |  mul(a,b):    { return f << '(' << a << " * " << b << ')'; }
  63    |  div(a,b):    { return f << '(' << a << " / " << b << ')'; }
  64    |  exp_list(l): { return f << '[' << l << ']'; }
  65    }
  66 }
  67
  68 //////////////////////////////////////////////////////////////////////////////
  69 //  This prints an expression list
  70 //////////////////////////////////////////////////////////////////////////////
  71 ostream& operator << (ostream& f, EXP_LIST l)
  72 {  match (l) {
  73       #[]:        { return f; }
  74    |  #[l]:       { return f << l; }
  75    |  #[h ... t]: { return f << h << ", " << t; }
  76    }
  77 }
  78
  79 //////////////////////////////////////////////////////////////////////////////
  80 //  Define the interface to a ``rewriting class.''  A rewriting class
  81 //  is simply a C++ class with rewriting rules attached.  In real programs
  82 //  this definition should be placed in some definition (i.e. .ph) files.
  83 //
  84 //  In parenthesis, we must list all datatypes involved.   Unlike
  85 //  simple pattern matching, rewriting can involve a set of mutually
  86 //  recursive (or mutually exclusive, if desired) datatype definitions.
  87 //  So in general this is a comma delimited list.
  88 //
  89 //  In this example it involves only the datatypes EXP and EXP_LIST.
  90 //////////////////////////////////////////////////////////////////////////////
  91 rewrite class Simplify (EXP, EXP_LIST)
  92 {  // nothing here for now.
  93 public:
  94    Simplify() {}
  95 };
  96
  97 //////////////////////////////////////////////////////////////////////////////
  98 //  Now we define the rewriting rules in the rewriting class Simplify.  These
  99 //  rules should be placed in an implementation file (.pcc, .pC, .pc++ etc).
 100 //
 101 //  In this brief sample class we have some rules that perform
 102 //  simple constant folding and strength reduction.
 103 //
 104 //  Currently, all the rules for a rewrite class must be placed in
 105 //  the same rewrite construct.  This will probably change in the future
 106 //  once I work out the details on incremental tree automata compilation.
 107 //////////////////////////////////////////////////////////////////////////////
 108 rewrite Simplify {
 109    add (num 0, x):                    rewrite(x);
 110 |  add (x, num 0):                    rewrite(x);
 111 |  sub (x, num 0):                    rewrite(x);
 112 |  mul (x, num 0):                    rewrite(num(0));
 113 |  mul (num 0, x):                    rewrite(num(0));
 114 |  mul (x, num 1):                    rewrite(x);
 115 |  mul (num 1, x):                    rewrite(x);
 116 |  mul (x, num 2):                    rewrite(add(x,x));
 117 |  mul (num 2, x):                    rewrite(add(x,x));
 118 |  div (x, num 1):                    rewrite(x);
 119 |  add (num x, num y):                rewrite(num(x + y));
 120 |  sub (num x, num y):                rewrite(num(x - y));
 121 |  mul (num x, num y):                rewrite(num(x * y));
 122 |  div (num x, num y) where (y != 0): rewrite(num(x / y));
 123 |  div (_, num 0):                    {  cout << "Division by zero!\n";
 124                                          div_by_zero++;
 125                                       }
 126 |  div (zero as num 0, x):            rewrite(zero);
 127 |  #[ _ ... _ ]:                      { cout << "list found\n"; }
 128 |  #[]:                               { cout << "nil found\n"; }
 129 };
 130
 131 //////////////////////////////////////////////////////////////////////////////
 132 //  Instantiate the datatypes
 133 //////////////////////////////////////////////////////////////////////////////
 134 instantiate datatype EXP, EXP_LIST;
 135
 136 //////////////////////////////////////////////////////////////////////////////
 137 //  Now defines the main program that uses all this stuff.
 138 //////////////////////////////////////////////////////////////////////////////
 139 int main()
 140 {
 141    //
 142    // Instantiate a rewriting class
 143    //
 144    Simplify sim;
 145
 146    //
 147    // (0 + x * 2) / (1 * 5 + 1 * 3) / (0 / y);
 148    //
 149    EXP t1 = div(div(add(num(0), mul(var('x'),num(2))),
 150                     add(mul(num(1), num(5)),mul(num(1),num(3)))),
 151                 div(num(0),var('y')));
 152    EXP term = mul(t1,t1);
 153
 154    //
 155    //  Rewrite the big term above.
 156    //
 157    cout << "Before: " << term << '\n';
 158    sim(term);
 159    cout << "After: " << term << '\n';
 160
 161    //
 162    //  Rewrite it again.  It should have no effect since the term
 163    //  is already in normal form.
 164    //
 165    sim(term);
 166    cout << "Again (should have no effect): " << term << '\n';
 167
 168    //
 169    //  Rewrite some other term.
 170    //
 171    EXP term2 = add(sub(num(3),num(3)), var('z'));
 172    cout << "Before: " << term2 << '\n';
 173    sim(term2);
 174    cout << "After: " << term2 << '\n';
 175
 176    //
 177    //  Rewrite some other term.
 178    //
 179    EXP term3 = div(num(1),num(0));
 180    sim(term3);
 181
 182    //
 183    //  Rewrite some other term.
 184    //  Notice that even though the patterns do not involve `exp_list'
 185    //  directly the internal components of `exp_list' are still candidates
 186    //  for rewrites: rewriting operates on the entire tree, and not just
 187    //  on the cover like vanilla pattern matching.
 188    //
 189    EXP term4 = exp_list(#[div(num(1),num(0)), var('x')]);
 190    sim(term4);
 191
 192    //
 193    //
 194    //  Set the terms to 'om' so that their storage is released.
 195    //
 196    t1 = term = term2 = term3 = term4 = om;
 197    if (div_by_zero != 6) { cerr << "BUG in rewriting!\n"; return 1; }
 198    if (balance != 0)     { cerr << "BUG in reference counting!\n"; return 1; }
 199    return 0;
 200 }