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