Merge remote branch 'master'
[prop.git] / tests / rewriting.cc
blob2e9a4d5ff1692efe37c3b4d5b93f2e8e31b2c9bd
1 ///////////////////////////////////////////////////////////////////////////////
2 // This file is generated automatically using Prop (version 2.3.2),
3 // last updated on Mar 14, 1997.
4 // The original source file is "rewriting.pcc".
5 ///////////////////////////////////////////////////////////////////////////////
7 #define PROP_REWRITING_USED
8 #define PROP_REFCOUNT_USED
9 #define PROP_QUARK_USED
10 #include <propdefs.h>
11 #line 1 "rewriting.pcc"
12 //////////////////////////////////////////////////////////////////////////////
13 // Testing the rewriting features.
14 //////////////////////////////////////////////////////////////////////////////
15 #include <new>
16 #include <iostream.h>
18 int balance; // number of allocation - number of deallocation
19 int div_by_zero; // number of division by zeros
21 //////////////////////////////////////////////////////////////////////////////
22 // We'll use reference counting with rewriting.
23 // The operators new and delete are redefined to keep track of
24 // the number of allocations and deallocation.
25 // This is for demonstration use only. In practice, it is
26 // unnecessary to redefine these operators if the normal ones
27 // suffice.
28 //////////////////////////////////////////////////////////////////////////////
29 class MEM {
30 public:
31 inline void * operator new (size_t n)
32 { balance++; return new char [n]; }
33 inline void operator delete (void * x)
34 { balance--; delete [] ((char*)x); }
37 //////////////////////////////////////////////////////////////////////////////
38 // Define the datatypes EXP and EXP_LIST. Currently, rewriting can only be
39 // performed on datatypes(and not views) in Prop. If replacement is
40 // to be performed on a datatype, then it should be declared using
41 // the ``rewrite'' qualifier.
43 // We'll extend these datatypes from class MEM so that it'll inherit
44 // MEM's operator new and delete.
45 //////////////////////////////////////////////////////////////////////////////
46 #line 35 "rewriting.pcc"
47 #line 48 "rewriting.pcc"
48 ///////////////////////////////////////////////////////////////////////////////
50 // Forward class definition for EXP
52 ///////////////////////////////////////////////////////////////////////////////
53 #ifndef datatype_EXP_defined
54 #define datatype_EXP_defined
55 class a_EXP;
56 typedef a_EXP * EXP;
57 #endif
59 # define om (EXP)0
61 ///////////////////////////////////////////////////////////////////////////////
63 // Forward class definition for EXP_LIST
65 ///////////////////////////////////////////////////////////////////////////////
66 #ifndef datatype_EXP_LIST_defined
67 #define datatype_EXP_LIST_defined
68 class a_EXP_LIST;
69 typedef a_EXP_LIST * EXP_LIST;
70 #endif
72 # define nil_1_ (EXP_LIST)0
74 ///////////////////////////////////////////////////////////////////////////////
76 // Base class for datatype EXP
78 ///////////////////////////////////////////////////////////////////////////////
79 class a_EXP : public MEM, public TermObj {
80 public:
81 enum Tag_EXP {
82 tag_num = 0, tag_var = 1, tag_add = 2,
83 tag_sub = 3, tag_mul = 4, tag_div = 5,
84 tag_exp_list = 6
87 public:
88 const Tag_EXP tag__; // variant tag
89 protected:
90 inline a_EXP(Tag_EXP t__) : tag__(t__) {}
91 public:
93 inline int boxed(const a_EXP * x) { return x != 0; }
94 inline int untag(const a_EXP * x) { return x ? (x->tag__+1) : 0; }
95 ///////////////////////////////////////////////////////////////////////////////
97 // Class for datatype constructor EXP::num
99 ///////////////////////////////////////////////////////////////////////////////
100 class EXP_num : public a_EXP {
101 public:
102 #line 36 "rewriting.pcc"
103 int num;
104 inline EXP_num (int x_num)
105 : a_EXP(tag_num), num(x_num)
110 ///////////////////////////////////////////////////////////////////////////////
112 // Class for datatype constructor EXP::var
114 ///////////////////////////////////////////////////////////////////////////////
115 class EXP_var : public a_EXP {
116 public:
117 #line 37 "rewriting.pcc"
118 char var;
119 inline EXP_var (char x_var)
120 : a_EXP(tag_var), var(x_var)
125 ///////////////////////////////////////////////////////////////////////////////
127 // Class for datatype constructor EXP::add
129 ///////////////////////////////////////////////////////////////////////////////
130 class EXP_add : public a_EXP {
131 public:
132 #line 38 "rewriting.pcc"
133 EXP _1; EXP _2;
134 inline EXP_add (EXP x_1, EXP x_2)
135 : a_EXP(tag_add), _1(x_1), _2(x_2)
140 ///////////////////////////////////////////////////////////////////////////////
142 // Class for datatype constructor EXP::sub
144 ///////////////////////////////////////////////////////////////////////////////
145 class EXP_sub : public a_EXP {
146 public:
147 #line 39 "rewriting.pcc"
148 EXP _1; EXP _2;
149 inline EXP_sub (EXP x_1, EXP x_2)
150 : a_EXP(tag_sub), _1(x_1), _2(x_2)
155 ///////////////////////////////////////////////////////////////////////////////
157 // Class for datatype constructor EXP::mul
159 ///////////////////////////////////////////////////////////////////////////////
160 class EXP_mul : public a_EXP {
161 public:
162 #line 40 "rewriting.pcc"
163 EXP _1; EXP _2;
164 inline EXP_mul (EXP x_1, EXP x_2)
165 : a_EXP(tag_mul), _1(x_1), _2(x_2)
170 ///////////////////////////////////////////////////////////////////////////////
172 // Class for datatype constructor EXP::div
174 ///////////////////////////////////////////////////////////////////////////////
175 class EXP_div : public a_EXP {
176 public:
177 #line 41 "rewriting.pcc"
178 EXP _1; EXP _2;
179 inline EXP_div (EXP x_1, EXP x_2)
180 : a_EXP(tag_div), _1(x_1), _2(x_2)
185 ///////////////////////////////////////////////////////////////////////////////
187 // Class for datatype constructor EXP::exp_list
189 ///////////////////////////////////////////////////////////////////////////////
190 class EXP_exp_list : public a_EXP {
191 public:
192 #line 42 "rewriting.pcc"
193 EXP_LIST exp_list;
194 inline EXP_exp_list (EXP_LIST x_exp_list)
195 : a_EXP(tag_exp_list), exp_list(x_exp_list)
200 ///////////////////////////////////////////////////////////////////////////////
202 // Datatype constructor functions for EXP
204 ///////////////////////////////////////////////////////////////////////////////
205 inline a_EXP * num (int x_num)
206 { return new EXP_num (x_num); }
207 inline a_EXP * var (char x_var)
208 { return new EXP_var (x_var); }
209 inline a_EXP * add (EXP x_1, EXP x_2)
210 { return new EXP_add (x_1, x_2); }
211 inline a_EXP * sub (EXP x_1, EXP x_2)
212 { return new EXP_sub (x_1, x_2); }
213 inline a_EXP * mul (EXP x_1, EXP x_2)
214 { return new EXP_mul (x_1, x_2); }
215 inline a_EXP * div (EXP x_1, EXP x_2)
216 { return new EXP_div (x_1, x_2); }
217 inline a_EXP * exp_list (EXP_LIST x_exp_list)
218 { return new EXP_exp_list (x_exp_list); }
219 ///////////////////////////////////////////////////////////////////////////////
221 // Downcasting functions for EXP
223 ///////////////////////////////////////////////////////////////////////////////
224 inline EXP_num * _num(const a_EXP * _x_) { return (EXP_num *)_x_; }
225 inline EXP_var * _var(const a_EXP * _x_) { return (EXP_var *)_x_; }
226 inline EXP_add * _add(const a_EXP * _x_) { return (EXP_add *)_x_; }
227 inline EXP_sub * _sub(const a_EXP * _x_) { return (EXP_sub *)_x_; }
228 inline EXP_mul * _mul(const a_EXP * _x_) { return (EXP_mul *)_x_; }
229 inline EXP_div * _div(const a_EXP * _x_) { return (EXP_div *)_x_; }
230 inline EXP_exp_list * _exp_list(const a_EXP * _x_) { return (EXP_exp_list *)_x_; }
232 ///////////////////////////////////////////////////////////////////////////////
234 // Class for datatype constructor EXP_LIST::#[...]
236 ///////////////////////////////////////////////////////////////////////////////
237 class a_EXP_LIST : public MEM, public TermObj {
238 public:
239 #line 46 "rewriting.pcc"
240 EXP _1; EXP_LIST _2;
241 inline a_EXP_LIST (EXP x_1, EXP_LIST x_2)
242 : _1(x_1), _2(x_2)
245 inline a_EXP_LIST (EXP x_1, int x_2)
246 : _1(x_1), _2((a_EXP_LIST *)x_2)
250 inline int boxed(const a_EXP_LIST * x) { return x != 0; }
251 inline int untag(const a_EXP_LIST * x) { return x ? 1 : 0; }
252 ///////////////////////////////////////////////////////////////////////////////
254 // Datatype constructor functions for EXP_LIST
256 ///////////////////////////////////////////////////////////////////////////////
257 inline a_EXP_LIST * list_1_ (EXP x_1, EXP_LIST x_2)
258 { return new a_EXP_LIST (x_1, x_2); }
259 inline a_EXP_LIST * list_1_ (EXP x_1, int x_2)
260 { return new a_EXP_LIST (x_1, x_2); }
261 ///////////////////////////////////////////////////////////////////////////////
263 // Downcasting functions for EXP_LIST
265 ///////////////////////////////////////////////////////////////////////////////
268 #line 48 "rewriting.pcc"
269 #line 48 "rewriting.pcc"
272 //////////////////////////////////////////////////////////////////////////////
273 // Define a method that prints an expression. This is a simple
274 // inductive definition
275 //////////////////////////////////////////////////////////////////////////////
276 ostream& operator << (ostream& f, EXP_LIST l);
277 ostream& operator << (ostream& f, EXP e)
279 #line 56 "rewriting.pcc"
280 #line 64 "rewriting.pcc"
282 if (e) {
283 switch (e->tag__) {
284 case a_EXP::tag_num: {
285 #line 58 "rewriting.pcc"
286 return f << _num(e)->num;
287 #line 58 "rewriting.pcc"
288 } break;
289 case a_EXP::tag_var: {
290 #line 59 "rewriting.pcc"
291 return f << _var(e)->var;
292 #line 59 "rewriting.pcc"
293 } break;
294 case a_EXP::tag_add: {
295 #line 60 "rewriting.pcc"
296 return f << '(' << _add(e)->_1 << " + " << _add(e)->_2 << ')';
297 #line 60 "rewriting.pcc"
298 } break;
299 case a_EXP::tag_sub: {
300 #line 61 "rewriting.pcc"
301 return f << '(' << _sub(e)->_1 << " - " << _sub(e)->_2 << ')';
302 #line 61 "rewriting.pcc"
303 } break;
304 case a_EXP::tag_mul: {
305 #line 62 "rewriting.pcc"
306 return f << '(' << _mul(e)->_1 << " * " << _mul(e)->_2 << ')';
307 #line 62 "rewriting.pcc"
308 } break;
309 case a_EXP::tag_div: {
310 #line 63 "rewriting.pcc"
311 return f << '(' << _div(e)->_1 << " / " << _div(e)->_2 << ')';
312 #line 63 "rewriting.pcc"
313 } break;
314 default: {
315 #line 64 "rewriting.pcc"
316 return f << '[' << _exp_list(e)->exp_list << ']';
317 #line 64 "rewriting.pcc"
318 } break;
320 } else {
321 #line 57 "rewriting.pcc"
322 return f << "om";
323 #line 57 "rewriting.pcc"
326 #line 65 "rewriting.pcc"
327 #line 65 "rewriting.pcc"
331 //////////////////////////////////////////////////////////////////////////////
332 // This prints an expression list
333 //////////////////////////////////////////////////////////////////////////////
334 ostream& operator << (ostream& f, EXP_LIST l)
336 #line 72 "rewriting.pcc"
337 #line 75 "rewriting.pcc"
339 if (l) {
340 if (l->_2) {
341 #line 75 "rewriting.pcc"
342 return f << l->_1 << ", " << l->_2;
343 #line 75 "rewriting.pcc"
344 } else {
345 #line 74 "rewriting.pcc"
346 return f << l->_1;
347 #line 74 "rewriting.pcc"
349 } else {
350 #line 73 "rewriting.pcc"
351 return f;
352 #line 73 "rewriting.pcc"
355 #line 76 "rewriting.pcc"
356 #line 76 "rewriting.pcc"
360 //////////////////////////////////////////////////////////////////////////////
361 // Define the interface to a ``rewriting class.'' A rewriting class
362 // is simply a C++ class with rewriting rules attached. In real programs
363 // this definition should be placed in some definition (i.e. .ph) files.
365 // In parenthesis, we must list all datatypes involved. Unlike
366 // simple pattern matching, rewriting can involve a set of mutually
367 // recursive (or mutually exclusive, if desired) datatype definitions.
368 // So in general this is a comma delimited list.
370 // In this example it involves only the datatypes EXP and EXP_LIST.
371 //////////////////////////////////////////////////////////////////////////////
372 #line 91 "rewriting.pcc"
373 #line 95 "rewriting.pcc"
374 class Simplify : public BURS {
375 private:
376 Simplify(const Simplify&); // no copy constructor
377 void operator = (const Simplify&); // no assignment
378 public:
379 struct Simplify_StateRec * stack__, * stack_top__;
380 public:
381 void labeler(const char *, int&, int);
382 void labeler(Quark, int&, int);
383 void labeler(EXP & redex, int&, int);
384 inline virtual void operator () (EXP & redex) { int s; labeler(redex,s,0); }
385 void labeler(EXP_LIST & redex, int&, int);
386 inline virtual void operator () (EXP_LIST & redex) { int s; labeler(redex,s,0); }
387 private:
388 #line 92 "rewriting.pcc"
389 // nothing here for now.
390 public:
391 Simplify() {}
392 #line 95 "rewriting.pcc"
394 #line 95 "rewriting.pcc"
395 #line 95 "rewriting.pcc"
398 //////////////////////////////////////////////////////////////////////////////
399 // Now we define the rewriting rules in the rewriting class Simplify. These
400 // rules should be placed in an implementation file (.pcc, .pC, .pc++ etc).
402 // In this brief sample class we have some rules that perform
403 // simple constant folding and strength reduction.
405 // Currently, all the rules for a rewrite class must be placed in
406 // the same rewrite construct. This will probably change in the future
407 // once I work out the details on incremental tree automata compilation.
408 //////////////////////////////////////////////////////////////////////////////
409 #line 108 "rewriting.pcc"
410 #line 128 "rewriting.pcc"
411 static const TreeTables::Offset Simplify_accept_base [ 15 ] = {
412 0, 1, 2, 3, 5, 7, 11, 13, 15, 18, 22, 30, 34, 37, 42
414 static const TreeTables::Rule Simplify_accept_vector [ 44 ] = {
415 -1, 17, -1, 16, -1, 1, -1, 0, 1, 10, -1, 0, -1, 2, -1, 2,
416 11, -1, 3, 5, 7, -1, 3, 4, 5, 6, 7, 8, 12, -1, 4, 6,
417 8, -1, 9, 14, -1, 9, 13, 14, 15, -1, 15, -1
419 static const TreeTables::State Simplify_theta_3[2][2] = {
420 { 0, 4 },
421 { 6, 5 }
425 static const TreeTables::State Simplify_theta_4[2][2] = {
426 { 0, 7 },
427 { 0, 8 }
431 static const TreeTables::State Simplify_theta_5[2][2] = {
432 { 0, 9 },
433 { 11, 10 }
437 static const TreeTables::State Simplify_theta_6[2][2] = {
438 { 0, 12 },
439 { 14, 13 }
443 static const TreeTables::State Simplify_mu_3_0[15] = {
444 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
448 static const TreeTables::State Simplify_mu_3_1[15] = {
449 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
453 static const TreeTables::State Simplify_mu_4_0[15] = {
454 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
458 static const TreeTables::State Simplify_mu_4_1[15] = {
459 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
463 static const TreeTables::State Simplify_mu_5_0[15] = {
464 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
468 static const TreeTables::State Simplify_mu_5_1[15] = {
469 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
473 static const TreeTables::State Simplify_mu_6_0[15] = {
474 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
478 static const TreeTables::State Simplify_mu_6_1[15] = {
479 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
483 inline void Simplify::labeler(char const * redex,int& s__,int)
486 s__ = 0;
490 inline void Simplify::labeler(Quark redex,int& s__,int)
493 s__ = 0;
497 void Simplify::labeler (EXP & redex, int& s__, int r__)
499 replacement__:
500 int cached__;
501 if (r__ && boxed(redex) && (cached__ = redex->get_rewrite_state()) != BURS::undefined_state)
502 { s__ = cached__; return; }
503 if ((redex)) {
504 switch(redex->tag__) {
505 case a_EXP::tag_num: {
506 int s0__;
507 s0__ = 0; // int
508 s__ = 2;} break;
509 case a_EXP::tag_var: {
510 int s0__;
511 s0__ = 0; // char
512 s__ = 0;} break;
513 case a_EXP::tag_add: {
514 int s0__;
515 int s1__;
516 labeler(_add(redex)->_1, s0__, r__);
517 labeler(_add(redex)->_2, s1__, r__);
518 s__ = Simplify_theta_3[Simplify_mu_3_0[s0__]][Simplify_mu_3_1[s1__]]; } break;
519 case a_EXP::tag_sub: {
520 int s0__;
521 int s1__;
522 labeler(_sub(redex)->_1, s0__, r__);
523 labeler(_sub(redex)->_2, s1__, r__);
524 s__ = Simplify_theta_4[Simplify_mu_4_0[s0__]][Simplify_mu_4_1[s1__]]; } break;
525 case a_EXP::tag_mul: {
526 int s0__;
527 int s1__;
528 labeler(_mul(redex)->_1, s0__, r__);
529 labeler(_mul(redex)->_2, s1__, r__);
530 s__ = Simplify_theta_5[Simplify_mu_5_0[s0__]][Simplify_mu_5_1[s1__]]; } break;
531 case a_EXP::tag_div: {
532 int s0__;
533 int s1__;
534 labeler(_div(redex)->_1, s0__, r__);
535 labeler(_div(redex)->_2, s1__, r__);
536 s__ = Simplify_theta_6[Simplify_mu_6_0[s0__]][Simplify_mu_6_1[s1__]]; } break;
537 default: {
538 int s0__;
539 labeler(_exp_list(redex)->exp_list, s0__, r__);
540 s__ = 0;} break;
542 } else {s__ = 0;
544 const TreeTables::Rule * o__ = Simplify_accept_vector + Simplify_accept_base[s__];
545 accept__:
546 switch (*o__) {
547 case 15: if ((_num(_div(redex)->_1)->num == 0))
549 #line 126 "rewriting.pcc"
550 { redex = _div(redex)->_1; r__ = 1; goto replacement__; }
551 #line 126 "rewriting.pcc"
553 else { ++o__; goto accept__; } break;
554 case 14: if ((_num(_div(redex)->_2)->num == 0))
556 #line 123 "rewriting.pcc"
557 cout << "Division by zero!\n";
558 div_by_zero++;
560 #line 125 "rewriting.pcc"
562 else { ++o__; goto accept__; } break;
563 case 13: if ((_num(_div(redex)->_2)->num != 0))
565 #line 122 "rewriting.pcc"
566 { redex = num((_num(_div(redex)->_1)->num / _num(_div(redex)->_2)->num)); r__ = 1; goto replacement__; }
567 #line 122 "rewriting.pcc"
569 else { ++o__; goto accept__; } break;
570 case 12: {
571 #line 121 "rewriting.pcc"
572 { redex = num((_num(_mul(redex)->_1)->num * _num(_mul(redex)->_2)->num)); r__ = 1; goto replacement__; }
573 #line 121 "rewriting.pcc"
574 } break;
575 case 11: {
576 #line 120 "rewriting.pcc"
577 { redex = num((_num(_sub(redex)->_1)->num - _num(_sub(redex)->_2)->num)); r__ = 1; goto replacement__; }
578 #line 120 "rewriting.pcc"
579 } break;
580 case 10: {
581 #line 119 "rewriting.pcc"
582 { redex = num((_num(_add(redex)->_1)->num + _num(_add(redex)->_2)->num)); r__ = 1; goto replacement__; }
583 #line 119 "rewriting.pcc"
584 } break;
585 case 9: if ((_num(_div(redex)->_2)->num == 1))
587 #line 118 "rewriting.pcc"
588 { redex = _div(redex)->_1; r__ = 1; goto replacement__; }
589 #line 118 "rewriting.pcc"
591 else { ++o__; goto accept__; } break;
592 case 8: if ((_num(_mul(redex)->_1)->num == 2))
594 #line 117 "rewriting.pcc"
595 { redex = add(_mul(redex)->_2,_mul(redex)->_2); r__ = 1; goto replacement__; }
596 #line 117 "rewriting.pcc"
598 else { ++o__; goto accept__; } break;
599 case 7: if ((_num(_mul(redex)->_2)->num == 2))
601 #line 116 "rewriting.pcc"
602 { redex = add(_mul(redex)->_1,_mul(redex)->_1); r__ = 1; goto replacement__; }
603 #line 116 "rewriting.pcc"
605 else { ++o__; goto accept__; } break;
606 case 6: if ((_num(_mul(redex)->_1)->num == 1))
608 #line 115 "rewriting.pcc"
609 { redex = _mul(redex)->_2; r__ = 1; goto replacement__; }
610 #line 115 "rewriting.pcc"
612 else { ++o__; goto accept__; } break;
613 case 5: if ((_num(_mul(redex)->_2)->num == 1))
615 #line 114 "rewriting.pcc"
616 { redex = _mul(redex)->_1; r__ = 1; goto replacement__; }
617 #line 114 "rewriting.pcc"
619 else { ++o__; goto accept__; } break;
620 case 4: if ((_num(_mul(redex)->_1)->num == 0))
622 #line 113 "rewriting.pcc"
623 { redex = num(0); r__ = 1; goto replacement__; }
624 #line 113 "rewriting.pcc"
626 else { ++o__; goto accept__; } break;
627 case 3: if ((_num(_mul(redex)->_2)->num == 0))
629 #line 112 "rewriting.pcc"
630 { redex = num(0); r__ = 1; goto replacement__; }
631 #line 112 "rewriting.pcc"
633 else { ++o__; goto accept__; } break;
634 case 2: if ((_num(_sub(redex)->_2)->num == 0))
636 #line 111 "rewriting.pcc"
637 { redex = _sub(redex)->_1; r__ = 1; goto replacement__; }
638 #line 111 "rewriting.pcc"
640 else { ++o__; goto accept__; } break;
641 case 1: if ((_num(_add(redex)->_2)->num == 0))
643 #line 110 "rewriting.pcc"
644 { redex = _add(redex)->_1; r__ = 1; goto replacement__; }
645 #line 110 "rewriting.pcc"
647 else { ++o__; goto accept__; } break;
648 case 0: if ((_num(_add(redex)->_1)->num == 0))
650 #line 109 "rewriting.pcc"
651 { redex = _add(redex)->_2; r__ = 1; goto replacement__; }
652 #line 109 "rewriting.pcc"
654 else { ++o__; goto accept__; } break;
656 if (boxed(redex)) {
657 redex->set_rewrite_state(s__);
662 void Simplify::labeler (EXP_LIST & redex, int& s__, int r__)
664 replacement__:
665 int cached__;
666 if (r__ && boxed(redex) && (cached__ = redex->get_rewrite_state()) != BURS::undefined_state)
667 { s__ = cached__; return; }
668 if ((redex)) {
669 int s0__;
670 int s1__;
671 labeler(redex->_1, s0__, r__);
672 labeler(redex->_2, s1__, r__);
673 s__ = 3;
674 } else {s__ = 1;
676 switch (s__) {
677 case 1: {
678 #line 128 "rewriting.pcc"
679 cout << "nil found\n";
680 #line 128 "rewriting.pcc"
681 } break;
682 case 3: {
683 #line 127 "rewriting.pcc"
684 cout << "list found\n";
685 #line 127 "rewriting.pcc"
686 } break;
688 if (boxed(redex)) {
689 redex->set_rewrite_state(s__);
694 #line 129 "rewriting.pcc"
695 #line 129 "rewriting.pcc"
698 //////////////////////////////////////////////////////////////////////////////
699 // Instantiate the datatypes
700 //////////////////////////////////////////////////////////////////////////////
701 #line 134 "rewriting.pcc"
702 #line 134 "rewriting.pcc"
703 ///////////////////////////////////////////////////////////////////////////////
704 // Instantiation of datatype EXP
705 ///////////////////////////////////////////////////////////////////////////////
706 #line 134 "rewriting.pcc"
709 ///////////////////////////////////////////////////////////////////////////////
710 // Instantiation of datatype EXP_LIST
711 ///////////////////////////////////////////////////////////////////////////////
712 #line 134 "rewriting.pcc"
715 #line 134 "rewriting.pcc"
716 #line 134 "rewriting.pcc"
719 //////////////////////////////////////////////////////////////////////////////
720 // Now defines the main program that uses all this stuff.
721 //////////////////////////////////////////////////////////////////////////////
722 int main()
725 // Instantiate a rewriting class
727 Simplify sim;
730 // (0 + x * 2) / (1 * 5 + 1 * 3) / (0 / y);
732 EXP t1 = div(div(add(num(0), mul(var('x'),num(2))),
733 add(mul(num(1), num(5)),mul(num(1),num(3)))),
734 div(num(0),var('y')));
735 EXP term = mul(t1,t1);
738 // Rewrite the big term above.
740 cout << "Before: " << term << '\n';
741 sim(term);
742 cout << "After: " << term << '\n';
745 // Rewrite it again. It should have no effect since the term
746 // is already in normal form.
748 sim(term);
749 cout << "Again (should have no effect): " << term << '\n';
752 // Rewrite some other term.
754 EXP term2 = add(sub(num(3),num(3)), var('z'));
755 cout << "Before: " << term2 << '\n';
756 sim(term2);
757 cout << "After: " << term2 << '\n';
760 // Rewrite some other term.
762 EXP term3 = div(num(1),num(0));
763 sim(term3);
766 // Rewrite some other term.
767 // Notice that even though the patterns do not involve `exp_list'
768 // directly the internal components of `exp_list' are still candidates
769 // for rewrites: rewriting operates on the entire tree, and not just
770 // on the cover like vanilla pattern matching.
772 EXP term4 = exp_list(
773 #line 189 "rewriting.pcc"
774 #line 189 "rewriting.pcc"
775 list_1_(div(num(1),num(0)),list_1_(var('x'),nil_1_))
776 #line 189 "rewriting.pcc"
777 #line 189 "rewriting.pcc"
779 sim(term4);
783 // Set the terms to 'om' so that their storage is released.
785 t1 = term = term2 = term3 = term4 = om;
786 if (div_by_zero != 6) { cerr << "BUG in rewriting!\n"; return 1; }
787 if (balance != 0) { cerr << "BUG in reference counting!\n"; return 1; }
788 return 0;
790 #line 201 "rewriting.pcc"
792 ------------------------------- Statistics -------------------------------
793 Merge matching rules = yes
794 Number of DFA nodes merged = 1
795 Number of ifs generated = 3
796 Number of switches generated = 1
797 Number of labels = 0
798 Number of gotos = 0
799 Adaptive matching = disabled
800 Fast string matching = disabled
801 Inline downcasts = disabled
802 --------------------------------------------------------------------------