with debug info
[prop.git] / tests / rewriting3.pcc
bloba610ef9ad8fd90f80230dc6dcd507accdd6a785c
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>
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> ]         
19 and      BOOL    = False | True                    // a boolean type
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
31 and      BinOp   = add | sub | mul | divide | mod  // binary operators
32                  | logical_and | logical_or     
33                  | eq  | ge | le | lt | gt | ne
35 and      UnaryOp = uminus | logical_not            // unary operators
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
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> ) 
51 and      Decl    = decl { name : Id, typ : Type }        // declarations
53 and  LabeledType = labeled_type (Id, Type)               // labeled types
55 where type Id    = const char *
56 ;   
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.
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
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   ;
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>;
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>;
138 /////////////////////////////////////////////////////////////////////////////
139 //  Defines the interface of a rewrite class Simplify.
140 //  All types that are referenced (directly or indirectly) should be
141 //  declared in the interface.
142 /////////////////////////////////////////////////////////////////////////////
143 rewrite class Simplify
144    ( Exp, BOOL, BinOp, UnaryOp, Stmt, Type, Decl, LabeledType,
145      List<Decl>, List<Stmt>, List<Type>, List<LabeledType>
146    )
148    // Method to print an error message 
149    void error(const char message[]) { cerr << message << '\n'; }
150 public:
151    Simplify() {}
154 /////////////////////////////////////////////////////////////////////////////
155 //  Now defines the rewrite rules.  These rules will be compiled into 
156 //  efficient pattern matching code by the translator.  A real life 
157 //  system will probably have many more rules than presented here.
158 //  (A machine code generator usually needs a few hundred rules)
159 //  Currently there are about 60 rules in this class.
160 /////////////////////////////////////////////////////////////////////////////
161 rewrite Simplify
162 {  
163    // Type coercion rules from integer -> real
164    binop(some_op, integer x, real y): rewrite(binop(some_op,real(x),real(y)));
165 |  binop(some_op, real x, integer y): rewrite(binop(some_op,real(x),real(y)));
167    // Constant folding rules for integers and reals.
168 |  binop(add,    integer x, integer y): rewrite(integer(x + y));
169 |  binop(sub,    integer x, integer y): rewrite(integer(x - y));
170 |  binop(mul,    integer x, integer y): rewrite(integer(x * y));
171 |  binop(divide, integer x, integer 0): { error("division by zero"); }
172 |  binop(divide, integer x, integer y): rewrite(integer(x / y));
173 |  binop(mod,    integer x, integer 0): { error("modulo by zero"); }
174 |  binop(mod,    integer x, integer y): rewrite(integer(x % y));
175 |  binop(add,    real x,    real y):    rewrite(real(x + y));
176 |  binop(sub,    real x,    real y):    rewrite(real(x - y));
177 |  binop(mul,    real x,    real y):    rewrite(real(x * y));
178 |  binop(divide, real x,    real 0.0):  { error("division by zero"); }
179 |  binop(divide, real x,    real y):    rewrite(real(x / y));
180 |  unaryop(uminus, integer x):          rewrite(integer(-x));
181 |  unaryop(uminus, real    x):          rewrite(real(-x));
183 // Constant folding rules for relational operators
184 |  binop(eq,  integer x, integer y):    rewrite(boolean((BOOL)(x == y)));
185 |  binop(ne,  integer x, integer y):    rewrite(boolean((BOOL)(x != y)));
186 |  binop(gt,  integer x, integer y):    rewrite(boolean((BOOL)(x > y)));
187 |  binop(lt,  integer x, integer y):    rewrite(boolean((BOOL)(x < y)));
188 |  binop(ge,  integer x, integer y):    rewrite(boolean((BOOL)(x >= y)));
189 |  binop(le,  integer x, integer y):    rewrite(boolean((BOOL)(x <= y)));
190 |  binop(eq,  real x,    real y):       rewrite(boolean((BOOL)(x == y)));
191 |  binop(ne,  real x,    real y):       rewrite(boolean((BOOL)(x != y)));
192 |  binop(gt,  real x,    real y):       rewrite(boolean((BOOL)(x > y)));
193 |  binop(lt,  real x,    real y):       rewrite(boolean((BOOL)(x < y)));
194 |  binop(ge,  real x,    real y):       rewrite(boolean((BOOL)(x >= y)));
195 |  binop(le,  real x,    real y):       rewrite(boolean((BOOL)(x <= y)));
197 // Constant folding rules for boolean operators
198 |  binop(logical_and, boolean x, boolean y):  rewrite(boolean((BOOL)(x && y)));
199 |  binop(logical_or,  boolean x, boolean y):  rewrite(boolean((BOOL)(x || y)));
200 |  unaryop(logical_not, boolean x):           rewrite(boolean((BOOL)(! x)));
202 // Simple algebraic laws for integers
203 |  binop(add, integer 0, x        ):  rewrite(x);
204 |  binop(add, x,         integer 0):  rewrite(x);
205 |  binop(sub, x,         integer 0):  rewrite(x);
206 |  binop(mul, integer 0, x        ):  rewrite(integer(0));
207 |  binop(mul, x,         integer 0):  rewrite(integer(0));
208 |  binop(mul, integer 1, x        ):  rewrite(x);
209 |  binop(mul, x,         integer 1):  rewrite(x);
210 |  binop(divide, x,      integer 1):  rewrite(x);
212 // Simple algebraic laws for reals
213 |  binop(add, real 0.0, x        ):  rewrite(x);
214 |  binop(add, x,         real 0.0):  rewrite(x);
215 |  binop(sub, x,         real 0.0):  rewrite(x);
216 |  binop(mul, real 0.0, x        ):  rewrite(real(0.0));
217 |  binop(mul, x,         real 0.0):  rewrite(real(0.0));
218 |  binop(mul, real 1.0, x        ):  rewrite(x);
219 |  binop(mul, x,         real 1.0):  rewrite(x);
220 |  binop(divide, x,      real 1.0):  rewrite(x);
221 // more ...
223 // Simple strength reduction (assume CSE will be applied)
224 |  binop(mul, integer 2, x        ):  rewrite(binop(add,x,x));
225 |  binop(mul, x, integer 2        ):  rewrite(binop(add,x,x));
226 // more ...
228 // Simple boolean identities
229 |  binop(logical_and, boolean False, _): rewrite(boolean(False));
230 |  binop(logical_and, boolean True, b):  rewrite(b);
231 |  binop(logical_and, _, boolean False): rewrite(boolean(False));
232 |  binop(logical_and, b, boolean True):  rewrite(b);
233 |  binop(logical_or,  boolean True, _):  rewrite(boolean(True));
234 |  binop(logical_or,  boolean False, b): rewrite(b);
235 |  binop(logical_or,  _, boolean True):  rewrite(boolean(True));
236 |  binop(logical_or,  b, boolean False): rewrite(b);
237 // more ...
239 // The following rules eliminate unreachable statements. 
240 |  if_stmt(boolean True, a, _):          rewrite(a);
241 |  if_stmt(boolean False, _, b):         rewrite(b);
242 |  #[while_stmt(boolean False, _) ... continuation]: 
243                                          rewrite(continuation);
244 // more ...
247 /////////////////////////////////////////////////////////////////////////////
248 //  The main program.
249 //  We'll test it with a simple program.
250 /////////////////////////////////////////////////////////////////////////////
251 int main()
252 {  
253    // Instantiate a rewriting object.
254    Simplify simplify;
256    // The input is the following block:
257    //
258    //  var x : int;
259    //  var y : int;
260    //  var z : array [10 * 30] of int;
261    //  begin
262    //     x = 0 + y * 1;
263    //     while (1 <> 1) y := y + 1;
264    //     print (not false);
265    //  end
266    //
267    Stmt prog = 
268       block_stmt( #[ decl("x", primitive_type("integer")),
269                      decl("y", primitive_type("integer")),
270                      decl("z", array_type(primitive_type("integer"),
271                                   binop(mul,integer(10), integer(30))
272                                          )
273                          )
274                   ],
275                   #[
276                    assign_stmt("x", 
277                       binop(add,integer(0),
278                          binop(mul,var("y"),integer(1)))),
279                    while_stmt(binop(ne, integer(1), integer(1)), 
280                               assign_stmt("y", 
281                                  binop(add,var("y"),integer(1)))),
282                    print_stmt(unaryop(logical_not,boolean(False)))
283                   ]
284                 );
285    cout << "Before:\n" << prog << "\n\n";
286    simplify(prog);
287    cout << "After:\n"  << prog << "\n";
288    return 0;