tests/prop7.pcc

   1 /////////////////////////////////////////////////////////////////////////////
   2 //  This test implements a rewrite based simplifier for the abstract
   3 //  syntax of a toy imperative language.
   4 //
   5 //  The test is quite elobarate and requires polymorphic datatypes to work
   6 //  correctly with garbage collection, pretty printing and rewriting.
   7 /////////////////////////////////////////////////////////////////////////////
   8 #include <iostream.h>
   9
  10 /////////////////////////////////////////////////////////////////////////////
  11 //  The following recursive type equations define the abstract syntax
  12 //  of our small language.
  13 //  ( Note: we define our own boolean type because not all C++ compilers
  14 //    have bool built-in yet. )
  15 /////////////////////////////////////////////////////////////////////////////
  16 datatype List<T> = #[]                             // a polymorphic list
  17                  | #[ T ... List<T> ]
  18
  19 and      BOOL    = False | True                    // a boolean type
  20
  21 and      Exp     = integer ( int )                 // integers
  22                  | real    ( double )              // real numbers
  23                  | string  ( char * )              // strings
  24                  | boolean ( BOOL )                // booleans
  25                  | binop   ( BinOp, Exp, Exp )     // binary op expression
  26                  | unaryop ( UnaryOp, Exp )        // unary op expression
  27                  | var     ( Id )                  // variables
  28                  | no_exp
  29                  | om_exp
  30
  31 and      BinOp   = add | sub | mul | divide | mod  // binary operators
  32                  | logical_and | logical_or
  33                  | eq  | ge | le | lt | gt | ne
  34
  35 and      UnaryOp = uminus | logical_not            // unary operators
  36
  37 and      Stmt    = assign_stmt ( Id, Exp )                // assignments
  38                  | while_stmt  ( Exp, Stmt )              // while statements
  39                  | if_stmt     ( Exp, Stmt, Stmt )        // if statements
  40                  | print_stmt  ( Exp )                    // print statements
  41                  | block_stmt  ( List<Decl>, List<Stmt> ) // blocks
  42                  | skip_stmt
  43
  44 and      Type    = primitive_type ( Id )                  // type expressions
  45                  | pointer_type   ( Type )
  46                  | array_type     { element : Type, bound : Exp }
  47                  | function_type  { args : Type, range : Type }
  48                  | tuple_type     ( List<Type> )
  49                  | record_type    ( List<LabeledType> )
  50
  51 and      Decl    = decl { name : Id, typ : Type }        // declarations
  52
  53 and  LabeledType = labeled_type (Id, Type)               // labeled types
  54
  55 where type Id    = const char *
  56 ;
  57
  58 /////////////////////////////////////////////////////////////////////////////
  59 //  Refine the implementation of the datatypes.
  60 //  The qualifiers may be also declared in the datatype definition.
  61 //  We qualify the datatypes here so that they won't clutter up
  62 //  the equations above.
  63 //
  64 //  All types are declared to be garbage collectable, printable by
  65 //  the printer method and rewritable.
  66 /////////////////////////////////////////////////////////////////////////////
  67 refine List<T>     :: collectable printable rewrite
  68 and    BOOL        :: collectable printable rewrite
  69 and    Exp         :: collectable printable rewrite
  70 and    BinOp       :: collectable printable rewrite
  71 and    UnaryOp     :: collectable printable rewrite
  72 and    Stmt        :: collectable printable rewrite
  73 and    Type        :: collectable printable rewrite
  74 and    Decl        :: collectable printable rewrite
  75 and    LabeledType :: collectable printable rewrite
  76
  77 /////////////////////////////////////////////////////////////////////////////
  78 //  Specify the pretty printing formats.
  79 /////////////////////////////////////////////////////////////////////////////
  80 and printable
  81     False          => "false"
  82   | True           => "true"
  83   | integer        => _
  84   | real           => _
  85   | string         => "\"" _ "\""
  86   | var            => _
  87   | boolean        => _
  88   | binop          => "(" 2 1 3 ")"  // reorder the arguments
  89   | unaryop        => "(" _ _")"
  90   | add            => "+"
  91   | sub            => "-"
  92   | mul            => "*"
  93   | divide         => "/"
  94   | mod            => "mod"
  95   | logical_and    => "and"
  96   | logical_or     => "or"
  97   | eq             => "="
  98   | ne             => "<>"
  99   | gt             => ">"
 100   | lt             => "<"
 101   | ge             => ">="
 102   | le             => "<="
 103   | uminus         => "-"
 104   | logical_not    => "not"
 105   | assign_stmt    => _ ":=" _ ";"
 106   | while_stmt     => "while" _ "do" { _ } "end while;"
 107   | if_stmt        => "if" _ " then" { _ } "else" { _ } "endif;"
 108   | print_stmt     => "print" _ ";"
 109   | block_stmt     => "begin" { _ / _ } "end"
 110   | primitive_type => _
 111   | pointer_type   => _ "^"
 112   | array_type     => "array" bound "of" element
 113   | function_type  => args "->" range
 114   | decl           => "var" name ":" typ ";"
 115   | labeled_type   => _ ":" _
 116   | #[]            => ""
 117   | #[...]         => _ / _
 118   ;
 119
 120 /////////////////////////////////////////////////////////////////////////////
 121 //  Generate the interfaces to instantiated polymorphic datatypes.
 122 //  These are not strictly necessary since the instantiation is in the
 123 //  same file below.  However, in general the 'instantiate extern' declaration
 124 //  must be placed in the .h files for each instance of a polymorphic
 125 //  datatype.
 126 /////////////////////////////////////////////////////////////////////////////
 127 instantiate extern datatype
 128    List<Type>, List<Stmt>, List<LabeledType>, List<Decl>;
 129
 130 /////////////////////////////////////////////////////////////////////////////
 131 //  Now instantiate all the datatypes.
 132 //  As specified in the definition, garbage collector type info and
 133 //  pretty printers will be generated automatically.
 134 /////////////////////////////////////////////////////////////////////////////
 135 instantiate datatype Exp, BOOL, BinOp, UnaryOp, Stmt, Type, Decl, LabeledType,
 136                      List<Type>, List<Stmt>, List<LabeledType>, List<Decl>;
 137
 138 /////////////////////////////////////////////////////////////////////////////
 139 //  Test the debugging facilities
 140 /////////////////////////////////////////////////////////////////////////////
 141 #define DEBUG_Simplify(a,b,c,d,e) print_rule(a,b,c,d,e)
 142 template <class T>
 143   T print_rule(T replacement, T redex, const char * file,
 144                int line, const char * rule)
 145   {  cout << '"' << file << "\", " << line << ": "
 146           << rule << endl
 147           << "\tBefore = " << redex << endl
 148           << "\tAfter  = " << replacement << endl;
 149      return replacement;
 150   }
 151
 152 /////////////////////////////////////////////////////////////////////////////
 153 //  Defines the interface of a rewrite class Simplify.
 154 //  All types that are referenced (directly or indirectly) should be
 155 //  declared in the interface.
 156 /////////////////////////////////////////////////////////////////////////////
 157 rewrite class Simplify
 158    ( Exp, BOOL, BinOp, UnaryOp, Stmt, Type, Decl, LabeledType,
 159      List<Decl>, List<Stmt>, List<Type>, List<LabeledType>
 160    )
 161 {
 162    // Method to print an error message
 163    void error(const char message[]) { cerr << message << '\n'; }
 164 public:
 165    Simplify() {}
 166 };
 167
 168 /////////////////////////////////////////////////////////////////////////////
 169 //  Now defines the rewrite rules.  These rules will be compiled into
 170 //  efficient pattern matching code by the translator.  A real life
 171 //  system will probably have many more rules than presented here.
 172 //  (A machine code generator usually needs a few hundred rules)
 173 //  Currently there are about 60 rules in this class.
 174 /////////////////////////////////////////////////////////////////////////////
 175 rewrite Simplify
 176 {
 177    // Type coercion rules from integer -> real
 178    binop(some_op, integer x, real y): rewrite(binop(some_op,real(x),real(y)));
 179 |  binop(some_op, real x, integer y): rewrite(binop(some_op,real(x),real(y)));
 180
 181    // Constant folding rules for integers and reals.
 182 |  binop(add,    integer x, integer y): rewrite(integer(x + y));
 183 |  binop(sub,    integer x, integer y): rewrite(integer(x - y));
 184 |  binop(mul,    integer x, integer y): rewrite(integer(x * y));
 185 |  binop(divide, integer x, integer 0): { error("division by zero"); }
 186 |  binop(divide, integer x, integer y): rewrite(integer(x / y));
 187 |  binop(mod,    integer x, integer 0): { error("modulo by zero"); }
 188 |  binop(mod,    integer x, integer y): rewrite(integer(x % y));
 189 |  binop(add,    real x,    real y):    rewrite(real(x + y));
 190 |  binop(sub,    real x,    real y):    rewrite(real(x - y));
 191 |  binop(mul,    real x,    real y):    rewrite(real(x * y));
 192 |  binop(divide, real x,    real 0.0):  { error("division by zero"); }
 193 |  binop(divide, real x,    real y):    rewrite(real(x / y));
 194 |  unaryop(uminus, integer x):          rewrite(integer(-x));
 195 |  unaryop(uminus, real    x):          rewrite(real(-x));
 196
 197 // Constant folding rules for relational operators
 198 |  binop(eq,  integer x, integer y):    rewrite(boolean((BOOL)(x == y)));
 199 |  binop(ne,  integer x, integer y):    rewrite(boolean((BOOL)(x != y)));
 200 |  binop(gt,  integer x, integer y):    rewrite(boolean((BOOL)(x > y)));
 201 |  binop(lt,  integer x, integer y):    rewrite(boolean((BOOL)(x < y)));
 202 |  binop(ge,  integer x, integer y):    rewrite(boolean((BOOL)(x >= y)));
 203 |  binop(le,  integer x, integer y):    rewrite(boolean((BOOL)(x <= y)));
 204 |  binop(eq,  real x,    real y):       rewrite(boolean((BOOL)(x == y)));
 205 |  binop(ne,  real x,    real y):       rewrite(boolean((BOOL)(x != y)));
 206 |  binop(gt,  real x,    real y):       rewrite(boolean((BOOL)(x > y)));
 207 |  binop(lt,  real x,    real y):       rewrite(boolean((BOOL)(x < y)));
 208 |  binop(ge,  real x,    real y):       rewrite(boolean((BOOL)(x >= y)));
 209 |  binop(le,  real x,    real y):       rewrite(boolean((BOOL)(x <= y)));
 210
 211 // Constant folding rules for boolean operators
 212 |  binop(logical_and, boolean x, boolean y):  rewrite(boolean((BOOL)(x && y)));
 213 |  binop(logical_or,  boolean x, boolean y):  rewrite(boolean((BOOL)(x || y)));
 214 |  unaryop(logical_not, boolean x):           rewrite(boolean((BOOL)(! x)));
 215
 216 // Simple algebraic laws for integers
 217 |  binop(add, integer 0, x        ):  rewrite(x);
 218 |  binop(add, x,         integer 0):  rewrite(x);
 219 |  binop(sub, x,         integer 0):  rewrite(x);
 220 |  binop(mul, integer 0, x        ):  rewrite(integer(0));
 221 |  binop(mul, x,         integer 0):  rewrite(integer(0));
 222 |  binop(mul, integer 1, x        ):  rewrite(x);
 223 |  binop(mul, x,         integer 1):  rewrite(x);
 224 |  binop(divide, x,      integer 1):  rewrite(x);
 225
 226 // Simple algebraic laws for reals
 227 |  binop(add, real 0.0, x        ):  rewrite(x);
 228 |  binop(add, x,         real 0.0):  rewrite(x);
 229 |  binop(sub, x,         real 0.0):  rewrite(x);
 230 |  binop(mul, real 0.0, x        ):  rewrite(real(0.0));
 231 |  binop(mul, x,         real 0.0):  rewrite(real(0.0));
 232 |  binop(mul, real 1.0, x        ):  rewrite(x);
 233 |  binop(mul, x,         real 1.0):  rewrite(x);
 234 |  binop(divide, x,      real 1.0):  rewrite(x);
 235 // more ...
 236
 237 // Simple strength reduction (assume CSE will be applied)
 238 |  binop(mul, integer 2, x        ):  rewrite(binop(add,x,x));
 239 |  binop(mul, x, integer 2        ):  rewrite(binop(add,x,x));
 240 // more ...
 241
 242 // Simple boolean identities
 243 |  binop(logical_and, boolean False, _): rewrite(boolean(False));
 244 |  binop(logical_and, boolean True, b):  rewrite(b);
 245 |  binop(logical_and, _, boolean False): rewrite(boolean(False));
 246 |  binop(logical_and, b, boolean True):  rewrite(b);
 247 |  binop(logical_or,  boolean True, _):  rewrite(boolean(True));
 248 |  binop(logical_or,  boolean False, b): rewrite(b);
 249 |  binop(logical_or,  _, boolean True):  rewrite(boolean(True));
 250 |  binop(logical_or,  b, boolean False): rewrite(b);
 251 // more ...
 252
 253 // The following rules eliminate unreachable statements.
 254 |  if_stmt(boolean True, a, _):          rewrite(a);
 255 |  if_stmt(boolean False, _, b):         rewrite(b);
 256 |  #[while_stmt(boolean False, _) ... continuation]:
 257                                          rewrite(continuation);
 258 // more ...
 259 };
 260
 261 /////////////////////////////////////////////////////////////////////////////
 262 //  The main program.
 263 //  We'll test it with a simple program.
 264 /////////////////////////////////////////////////////////////////////////////
 265 int main()
 266 {
 267    // Instantiate a rewriting object.
 268    Simplify simplify;
 269
 270    // The input is the following block:
 271    //
 272    //  var x : int;
 273    //  var y : int;
 274    //  var z : array [10 * 30] of int;
 275    //  begin
 276    //     x = 0 + y * 1;
 277    //     while (1 <> 1) y := y + 1;
 278    //     print (not false);
 279    //  end
 280    //
 281    Stmt prog =
 282       block_stmt( #[ decl("x", primitive_type("integer")),
 283                      decl("y", primitive_type("integer")),
 284                      decl("z", array_type(primitive_type("integer"),
 285                                   binop(mul,integer(10), integer(30))
 286                                          )
 287                          )
 288                   ],
 289                   #[
 290                    assign_stmt("x",
 291                       binop(add,integer(0),
 292                          binop(mul,var("y"),integer(1)))),
 293                    while_stmt(binop(ne, integer(1), integer(1)),
 294                               assign_stmt("y",
 295                                  binop(add,var("y"),integer(1)))),
 296                    print_stmt(unaryop(logical_not,boolean(False)))
 297                   ]
 298                 );
 299    cout << "Before:\n" << prog << "\n\n";
 300    simplify(prog);
 301    cout << "After:\n"  << prog << "\n";
 302    return 0;
 303 }