app/willard/phase3.cc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //  This file is generated automatically using Prop (version 2.3.5),
   3 //  last updated on Jun 18, 1997.
   4 //  The original source file is "phase3.pcc".
   5 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #define PROP_REWRITING_USED
   8 #define PROP_STRCMP_USED
   9 #define PROP_QUARK_USED
  10 #define PROP_TUPLE2_USED
  11 #include <propdefs.h>
  12 #line 1 "phase3.pcc"
  13 #include <AD/pretty/postream.h>
  14 #include "phase3.h"
  15 #include "list.h"
  16
  17 ///////////////////////////////////////////////////////////////////////////////
  18 //
  19 //  Constructors and destructors for phase3
  20 //
  21 ///////////////////////////////////////////////////////////////////////////////
  22 Phase3::Phase3() {}
  23 Phase3::~Phase3() {}
  24
  25 ///////////////////////////////////////////////////////////////////////////////
  26 //
  27 //  Methods to invoke phase3
  28 //
  29 ///////////////////////////////////////////////////////////////////////////////
  30 Exp Phase3::phase3(Exp e)
  31 {  message("Disjunction removal phase", e); (*this)(e); return e; }
  32
  33 ///////////////////////////////////////////////////////////////////////////////
  34 //
  35 //  Transformations to change disjunctions into unions
  36 //
  37 ///////////////////////////////////////////////////////////////////////////////
  38 #line 26 "phase3.pcc"
  39 #line 58 "phase3.pcc"
  40 ///////////////////////////////////////////////////////////////////////////////
  41 //
  42 // This macro can be redefined by the user for debugging
  43 //
  44 ///////////////////////////////////////////////////////////////////////////////
  45 #ifndef DEBUG_Phase3
  46 #define DEBUG_Phase3(repl,redex,file,line,rule) repl
  47 #else
  48 static const char * Phase3_file_name = "phase3.pcc";
  49 #endif
  50
  51 static const TreeTables::ShortState Phase3_theta_0[2][2] = {
  52    { 0, 0 },
  53    { 4, 10 }
  54 };
  55
  56
  57 static const TreeTables::ShortState Phase3_theta_7[2][1] = {
  58    { 0 },
  59    { 6 }
  60 };
  61
  62
  63 static const TreeTables::ShortState Phase3_theta_8[1][1][2] = {
  64    { { 0, 8 } }
  65 };
  66
  67
  68 static const TreeTables::ShortState Phase3_theta_9[1][2][1] = {
  69    { { 3 },
  70    { 5 } }
  71 };
  72
  73
  74 static const TreeTables::ShortState Phase3_theta_11[2][3] = {
  75    { 0, 0, 9 },
  76    { 0, 7, 9 }
  77 };
  78
  79
  80 static const TreeTables::ShortState Phase3_mu_0_0[11] = {
  81    0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0
  82 };
  83
  84
  85 static const TreeTables::ShortState Phase3_mu_0_1[11] = {
  86    0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0
  87 };
  88
  89
  90 static const TreeTables::ShortState Phase3_mu_7_0[11] = {
  91    0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1
  92 };
  93
  94
  95 static const TreeTables::ShortState Phase3_mu_8_2[11] = {
  96    0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0
  97 };
  98
  99
 100 static const TreeTables::ShortState Phase3_mu_9_1[11] = {
 101    0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0
 102 };
 103
 104
 105 static const TreeTables::ShortState Phase3_mu_11_0[11] = {
 106    0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1
 107 };
 108
 109
 110 static const TreeTables::ShortState Phase3_mu_11_1[11] = {
 111    0, 1, 0, 0, 0, 0, 0, 2, 0, 0, 0
 112 };
 113
 114
 115 inline void  Phase3::labeler(char const * redex,int& s__,int)
 116 {
 117    {
 118       if (_equal_string(redex,"or")) {s__ = 2;}
 119       else {s__ = 0;}
 120    }
 121 }
 122
 123 inline void  Phase3::labeler(Quark redex,int& s__,int)
 124 {
 125    {
 126 s__ = 0;
 127    }
 128 }
 129
 130 void  Phase3::labeler (Exp & redex, int& s__, int r__)
 131 {
 132 replacement__:
 133    {
 134       switch (redex->tag__) {
 135          case a_Exp::tag_GENERATOR: {
 136             switch (_GENERATOR(redex)->_3->tag__) {
 137                case a_Exp::tag_GENERATOR: {
 138 #line 31 "phase3.pcc"
 139                   { redex = DEBUG_Phase3(GENERATOR(append(_GENERATOR(redex)->_1,_GENERATOR(_GENERATOR(redex)->_3)->_1),append(_GENERATOR(redex)->_2,_GENERATOR(_GENERATOR(redex)->_3)->_2),_GENERATOR(_GENERATOR(redex)->_3)->_3),redex,Phase3_file_name,31,"GENERATOR (x, A, GENERATOR (y, B, C)): ...");
 140                     r__ = 1; goto replacement__; }
 141 #line 33 "phase3.pcc"
 142                   } break;
 143                default: {} break;
 144             }
 145             } break;
 146          default: {} break;
 147       }
 148    }
 149    int cached__;
 150    if (r__ && boxed(redex) && (cached__ = redex->get_rewrite_state()) != BURS::undefined_state)
 151    { s__ = cached__; return; }
 152    switch(redex->tag__) {
 153       case a_Exp::tag_OP: {
 154          int s0__;
 155          int s1__;
 156          labeler(_OP(redex)->_1, s0__, r__);
 157          labeler(_OP(redex)->_2, s1__, r__);
 158          s__ = Phase3_theta_0[Phase3_mu_0_0[s0__]][Phase3_mu_0_1[s1__]]; } break;
 159       case a_Exp::tag_APP: {
 160          int s0__;
 161          int s1__;
 162          labeler(_APP(redex)->_1, s0__, r__);
 163          labeler(_APP(redex)->_2, s1__, r__);
 164          s__ = 0;} break;
 165       case a_Exp::tag_LIT: {
 166          int s0__;
 167          labeler(_LIT(redex)->LIT, s0__, r__);
 168          s__ = 0;} break;
 169       case a_Exp::tag_ID: {
 170          int s0__;
 171          labeler(_ID(redex)->ID, s0__, r__);
 172          s__ = 0;} break;
 173       case a_Exp::tag_TUPLE: {
 174          int s0__;
 175          labeler(_TUPLE(redex)->TUPLE, s0__, r__);
 176          s__ = 0;} break;
 177       case a_Exp::tag_FORALL: {
 178          int s0__;
 179          int s1__;
 180          int s2__;
 181          labeler(_FORALL(redex)->_1, s0__, r__);
 182          labeler(_FORALL(redex)->_2, s1__, r__);
 183          labeler(_FORALL(redex)->_3, s2__, r__);
 184          s__ = 0;} break;
 185       case a_Exp::tag_EXISTS: {
 186          int s0__;
 187          int s1__;
 188          int s2__;
 189          labeler(_EXISTS(redex)->_1, s0__, r__);
 190          labeler(_EXISTS(redex)->_2, s1__, r__);
 191          labeler(_EXISTS(redex)->_3, s2__, r__);
 192          s__ = 0;} break;
 193       case a_Exp::tag_GUARD: {
 194          int s0__;
 195          int s1__;
 196          labeler(_GUARD(redex)->_1, s0__, r__);
 197          labeler(_GUARD(redex)->_2, s1__, r__);
 198          s__ = Phase3_theta_7[Phase3_mu_7_0[s0__]][0]; } break;
 199       case a_Exp::tag_GENERATOR: {
 200          int s0__;
 201          int s1__;
 202          int s2__;
 203          s0__ = 0; // Ids
 204          labeler(_GENERATOR(redex)->_2, s1__, r__);
 205          labeler(_GENERATOR(redex)->_3, s2__, r__);
 206          s__ = Phase3_theta_8[0][0][Phase3_mu_8_2[s2__]]; } break;
 207       default: {
 208          int s0__;
 209          int s1__;
 210          int s2__;
 211          labeler(_LET(redex)->_1, s0__, r__);
 212          labeler(_LET(redex)->_2, s1__, r__);
 213          labeler(_LET(redex)->_3, s2__, r__);
 214          s__ = Phase3_theta_9[0][Phase3_mu_9_1[s1__]][0]; } break;
 215    }
 216    switch (s__) {
 217       case 5: {
 218 #line 57 "phase3.pcc"
 219          { redex = DEBUG_Phase3(LET(_LET(_LET(redex)->_2)->_1,_LET(_LET(redex)->_2)->_2,LET(_LET(redex)->_1,_LET(_LET(redex)->_2)->_3,_LET(redex)->_3)),redex,Phase3_file_name,57,"LET (x, LET (y, b, a), e): ...");
 220            r__ = 1; goto replacement__; }
 221 #line 58 "phase3.pcc"
 222 } break;
 223       case 8: {
 224 #line 40 "phase3.pcc"
 225        Ids  xs   =
 226 #line 40 "phase3.pcc"
 227 #line 40 "phase3.pcc"
 228          nil_1_
 229 #line 40 "phase3.pcc"
 230 #line 40 "phase3.pcc"
 231          ;
 232          Exps Qs   =
 233 #line 41 "phase3.pcc"
 234 #line 41 "phase3.pcc"
 235          nil_1_
 236 #line 41 "phase3.pcc"
 237 #line 41 "phase3.pcc"
 238          ;
 239          Exps exps =
 240 #line 42 "phase3.pcc"
 241 #line 42 "phase3.pcc"
 242          nil_1_
 243 #line 42 "phase3.pcc"
 244 #line 42 "phase3.pcc"
 245          ;
 246          Exps disjuncts = _OP(_GUARD(_GENERATOR(redex)->_3)->_1)->_2;
 247
 248 #line 44 "phase3.pcc"
 249 #line 51 "phase3.pcc"
 250          {
 251             for (;;) {
 252                if (disjuncts) {
 253 #line 46 "phase3.pcc"
 254                 Id Q = gensym();
 255                             xs   =
 256 #line 47 "phase3.pcc"
 257 #line 47 "phase3.pcc"
 258                   list_1_(Q,xs)
 259 #line 47 "phase3.pcc"
 260 #line 47 "phase3.pcc"
 261                   ;
 262                             Qs   =
 263 #line 48 "phase3.pcc"
 264 #line 48 "phase3.pcc"
 265                   list_1_(GENERATOR(_GENERATOR(redex)->_1,_GENERATOR(redex)->_2,GUARD(disjuncts->_1,_GUARD(_GENERATOR(redex)->_3)->_2)),Qs)
 266 #line 48 "phase3.pcc"
 267 #line 48 "phase3.pcc"
 268                   ;
 269                   exps =
 270 #line 49 "phase3.pcc"
 271 #line 49 "phase3.pcc"
 272                   list_1_(ID(Q),exps)
 273 #line 49 "phase3.pcc"
 274 #line 49 "phase3.pcc"
 275                   ;
 276                   disjuncts = disjuncts->_2;
 277
 278 #line 51 "phase3.pcc"
 279                } else { goto L1; }
 280             }
 281             L1:;
 282          }
 283 #line 52 "phase3.pcc"
 284 #line 52 "phase3.pcc"
 285
 286
 287 #line 53 "phase3.pcc"
 288 #line 53 "phase3.pcc"
 289          { redex = DEBUG_Phase3(make_let(xs,Qs,OP("union",exps)),redex,Phase3_file_name,39,"GENERATOR (x, A, GUARD (OP (\"or\", es), e)): ...");
 290            r__ = 1; goto replacement__; }
 291 #line 53 "phase3.pcc"
 292 #line 53 "phase3.pcc"
 293
 294
 295 #line 54 "phase3.pcc"
 296 } break;
 297       case 10: {
 298 #line 36 "phase3.pcc"
 299          { redex = DEBUG_Phase3(OP("or",list_1_(_OP(redex)->_2->_1,_OP(_OP(redex)->_2->_2->_1)->_2)),redex,Phase3_file_name,36,"OP (\"or\", #[a, OP (\"or\", b)]): ...");
 300            r__ = 1; goto replacement__; }
 301 #line 39 "phase3.pcc"
 302 } break;
 303    }
 304    if (boxed(redex)) {
 305       redex->set_rewrite_state(s__);
 306    }
 307
 308 }
 309
 310 void  Phase3::labeler (Literal & redex, int& s__, int r__)
 311 {
 312 replacement__:
 313    switch(redex->tag__) {
 314       case a_Literal::tag_INT: {
 315          int s0__;
 316          s0__ = 0; // int
 317          s__ = 0;} break;
 318       case a_Literal::tag_STRING: {
 319          int s0__;
 320          labeler(_STRING(redex)->STRING, s0__, r__);
 321          s__ = 0;} break;
 322       default: {
 323          int s0__;
 324          s0__ = 0; // Bool
 325          s__ = 0;} break;
 326    }
 327
 328 }
 329
 330 void  Phase3::labeler (a_List<Exp> *  & redex, int& s__, int r__)
 331 {
 332 replacement__:
 333    if ((redex)) {
 334       int s0__;
 335       int s1__;
 336       labeler(redex->_1, s0__, r__);
 337       labeler(redex->_2, s1__, r__);
 338       s__ = Phase3_theta_11[Phase3_mu_11_0[s0__]][Phase3_mu_11_1[s1__]];
 339    } else {s__ = 1;
 340    }
 341
 342 }
 343
 344 #line 58 "phase3.pcc"
 345 #line 58 "phase3.pcc"
 346
 347 #line 59 "phase3.pcc"
 348 /*
 349 ------------------------------- Statistics -------------------------------
 350 Merge matching rules         = yes
 351 Number of DFA nodes merged   = 20
 352 Number of ifs generated      = 2
 353 Number of switches generated = 2
 354 Number of labels             = 0
 355 Number of gotos              = 0
 356 Adaptive matching            = disabled
 357 Fast string matching         = disabled
 358 Inline downcasts             = disabled
 359 --------------------------------------------------------------------------
 360 */