app/willard/rename.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 "rename.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 "rename.pcc"
  13 #include <AD/pretty/postream.h>
  14 #include "rename.h"
  15
  16 ///////////////////////////////////////////////////////////////////////////////
  17 //
  18 //  Constructor and destructor for the renaming phase
  19 //
  20 ///////////////////////////////////////////////////////////////////////////////
  21 RemoveDuplicateNames::RemoveDuplicateNames() {}
  22 RemoveDuplicateNames::~RemoveDuplicateNames() {}
  23
  24 ///////////////////////////////////////////////////////////////////////////////
  25 //
  26 //  Method to create a new variable binding.  We'll only create a
  27 //  new name if the current binding overshadows some previous name.
  28 //
  29 ///////////////////////////////////////////////////////////////////////////////
  30 void RemoveDuplicateNames::new_binding(Id& x)
  31 {  if (env.contains(x))
  32    {  Id y = gensym(x);
  33       env.insert(x,
  34 #line 21 "rename.pcc"
  35 #line 21 "rename.pcc"
  36 list_1_(y,env[x])
  37 #line 21 "rename.pcc"
  38 #line 21 "rename.pcc"
  39 );
  40    } else
  41    {  env.insert(x,
  42 #line 23 "rename.pcc"
  43 #line 23 "rename.pcc"
  44 list_1_(x)
  45 #line 23 "rename.pcc"
  46 #line 23 "rename.pcc"
  47 ); }
  48 }
  49
  50 void RemoveDuplicateNames::new_binding(Ids ids)
  51 {
  52 #line 27 "rename.pcc"
  53 #line 28 "rename.pcc"
  54 {
  55    for (;;) {
  56       if (ids) {
  57 #line 28 "rename.pcc"
  58         new_binding(ids->_1); ids = ids->_2;
  59 #line 28 "rename.pcc"
  60       } else { goto L1; }
  61    }
  62    L1:;
  63 }
  64 #line 29 "rename.pcc"
  65 #line 29 "rename.pcc"
  66
  67 }
  68
  69 ///////////////////////////////////////////////////////////////////////////////
  70 //
  71 //  Method to remove a variable binding.
  72 //
  73 ///////////////////////////////////////////////////////////////////////////////
  74 void RemoveDuplicateNames::old_binding(Id& x)
  75 {  Ids names = env[x];
  76
  77 #line 39 "rename.pcc"
  78 #line 43 "rename.pcc"
  79 {
  80    if (names) {
  81       if (names->_2) {
  82 #line 41 "rename.pcc"
  83         env.insert(x,names->_2); x = names->_1;
  84 #line 41 "rename.pcc"
  85       } else {
  86 #line 40 "rename.pcc"
  87         env.remove(x); x = names->_1;
  88 #line 40 "rename.pcc"
  89       }
  90    } else {}
  91 }
  92 #line 43 "rename.pcc"
  93 #line 43 "rename.pcc"
  94
  95 }
  96
  97 void RemoveDuplicateNames::old_binding(Ids ids)
  98 {
  99 #line 47 "rename.pcc"
 100 #line 48 "rename.pcc"
 101 {
 102    for (;;) {
 103       if (ids) {
 104 #line 48 "rename.pcc"
 105         old_binding(ids->_1); ids = ids->_2;
 106 #line 48 "rename.pcc"
 107       } else { goto L2; }
 108    }
 109    L2:;
 110 }
 111 #line 49 "rename.pcc"
 112 #line 49 "rename.pcc"
 113
 114 }
 115
 116 ///////////////////////////////////////////////////////////////////////////////
 117 //
 118 //  Method to rename a variable
 119 //
 120 ///////////////////////////////////////////////////////////////////////////////
 121 void RemoveDuplicateNames::rename(Id& x)
 122 {  if (env.contains(x))
 123    {  Ids names = env[x];
 124
 125 #line 60 "rename.pcc"
 126 #line 63 "rename.pcc"
 127 {
 128    if (names) {
 129 #line 61 "rename.pcc"
 130      x = names->_1;
 131 #line 61 "rename.pcc"
 132    } else {}
 133 }
 134 #line 63 "rename.pcc"
 135 #line 63 "rename.pcc"
 136
 137    }
 138 }
 139
 140 ///////////////////////////////////////////////////////////////////////////////
 141 //
 142 //  Method to invoke the renaming phase.
 143 //
 144 ///////////////////////////////////////////////////////////////////////////////
 145 Exp RemoveDuplicateNames::remove_duplicate_names(Exp e)
 146 {  message("Renaming phase", e); env.clear(); (*this)(e); return e; }
 147
 148 ///////////////////////////////////////////////////////////////////////////////
 149 //
 150 //  Transformation rules
 151 //
 152 ///////////////////////////////////////////////////////////////////////////////
 153 #line 80 "rename.pcc"
 154 #line 100 "rename.pcc"
 155 ///////////////////////////////////////////////////////////////////////////////
 156 //
 157 // This macro can be redefined by the user for debugging
 158 //
 159 ///////////////////////////////////////////////////////////////////////////////
 160 #ifndef DEBUG_RemoveDuplicateNames
 161 #define DEBUG_RemoveDuplicateNames(repl,redex,file,line,rule) repl
 162 #else
 163 static const char * RemoveDuplicateNames_file_name = "rename.pcc";
 164 #endif
 165
 166 inline void  RemoveDuplicateNames::labeler(char const * redex,int& s__,int)
 167 {
 168    {
 169 s__ = 0;
 170    }
 171 }
 172
 173 inline void  RemoveDuplicateNames::labeler(Quark redex,int& s__,int)
 174 {
 175    {
 176 s__ = 0;
 177    }
 178 }
 179
 180 void  RemoveDuplicateNames::labeler (Exp & redex, int& s__, int r__)
 181 {
 182 replacement__:
 183    {
 184       switch (redex->tag__) {
 185          case a_Exp::tag_ID: {
 186 #line 94 "rename.pcc"
 187            rename(_ID(redex)->ID);
 188 #line 94 "rename.pcc"
 189             } break;
 190          case a_Exp::tag_FORALL: {
 191 #line 89 "rename.pcc"
 192            new_binding(_FORALL(redex)->_1);
 193 #line 89 "rename.pcc"
 194             } break;
 195          case a_Exp::tag_EXISTS: {
 196 #line 88 "rename.pcc"
 197            new_binding(_EXISTS(redex)->_1);
 198 #line 88 "rename.pcc"
 199             } break;
 200          case a_Exp::tag_GENERATOR: {
 201 #line 90 "rename.pcc"
 202            new_binding(_GENERATOR(redex)->_1);
 203 #line 90 "rename.pcc"
 204             } break;
 205          case a_Exp::tag_LET: {
 206 #line 91 "rename.pcc"
 207            new_binding(_LET(redex)->_1);
 208 #line 91 "rename.pcc"
 209             } break;
 210          default: {} break;
 211       }
 212    }
 213    switch(redex->tag__) {
 214       case a_Exp::tag_OP: {
 215          int s0__;
 216          int s1__;
 217          labeler(_OP(redex)->_1, s0__, r__);
 218          labeler(_OP(redex)->_2, s1__, r__);
 219          s__ = 0;} break;
 220       case a_Exp::tag_APP: {
 221          int s0__;
 222          int s1__;
 223          labeler(_APP(redex)->_1, s0__, r__);
 224          labeler(_APP(redex)->_2, s1__, r__);
 225          s__ = 0;} break;
 226       case a_Exp::tag_LIT: {
 227          int s0__;
 228          labeler(_LIT(redex)->LIT, s0__, r__);
 229          s__ = 0;} break;
 230       case a_Exp::tag_ID: {
 231          int s0__;
 232          labeler(_ID(redex)->ID, s0__, r__);
 233          s__ = 0;} break;
 234       case a_Exp::tag_TUPLE: {
 235          int s0__;
 236          labeler(_TUPLE(redex)->TUPLE, s0__, r__);
 237          s__ = 0;} break;
 238       case a_Exp::tag_FORALL: {
 239          int s0__;
 240          int s1__;
 241          int s2__;
 242          labeler(_FORALL(redex)->_1, s0__, r__);
 243          labeler(_FORALL(redex)->_2, s1__, r__);
 244          labeler(_FORALL(redex)->_3, s2__, r__);
 245          s__ = 0;} break;
 246       case a_Exp::tag_EXISTS: {
 247          int s0__;
 248          int s1__;
 249          int s2__;
 250          labeler(_EXISTS(redex)->_1, s0__, r__);
 251          labeler(_EXISTS(redex)->_2, s1__, r__);
 252          labeler(_EXISTS(redex)->_3, s2__, r__);
 253          s__ = 0;} break;
 254       case a_Exp::tag_GUARD: {
 255          int s0__;
 256          int s1__;
 257          labeler(_GUARD(redex)->_1, s0__, r__);
 258          labeler(_GUARD(redex)->_2, s1__, r__);
 259          s__ = 0;} break;
 260       case a_Exp::tag_GENERATOR: {
 261          int s0__;
 262          int s1__;
 263          int s2__;
 264          s0__ = 0; // Ids
 265          labeler(_GENERATOR(redex)->_2, s1__, r__);
 266          labeler(_GENERATOR(redex)->_3, s2__, r__);
 267          s__ = 0;} break;
 268       default: {
 269          int s0__;
 270          int s1__;
 271          int s2__;
 272          labeler(_LET(redex)->_1, s0__, r__);
 273          labeler(_LET(redex)->_2, s1__, r__);
 274          labeler(_LET(redex)->_3, s2__, r__);
 275          s__ = 0;} break;
 276    }
 277    {
 278       switch (redex->tag__) {
 279          case a_Exp::tag_FORALL: {
 280 #line 98 "rename.pcc"
 281            old_binding(_FORALL(redex)->_1);  define_range(_FORALL(redex)->_1,_FORALL(redex)->_2);
 282 #line 98 "rename.pcc"
 283             } break;
 284          case a_Exp::tag_EXISTS: {
 285 #line 97 "rename.pcc"
 286            old_binding(_EXISTS(redex)->_1);  define_range(_EXISTS(redex)->_1,_EXISTS(redex)->_2);
 287 #line 97 "rename.pcc"
 288             } break;
 289          case a_Exp::tag_GENERATOR: {
 290 #line 99 "rename.pcc"
 291            old_binding(_GENERATOR(redex)->_1); define_range(_GENERATOR(redex)->_1,_GENERATOR(redex)->_2);
 292 #line 99 "rename.pcc"
 293             } break;
 294          case a_Exp::tag_LET: {
 295 #line 100 "rename.pcc"
 296            old_binding(_LET(redex)->_1);
 297 #line 100 "rename.pcc"
 298             } break;
 299          default: {} break;
 300       }
 301    }
 302
 303 }
 304
 305 void  RemoveDuplicateNames::labeler (Literal & redex, int& s__, int r__)
 306 {
 307 replacement__:
 308    switch(redex->tag__) {
 309       case a_Literal::tag_INT: {
 310          int s0__;
 311          s0__ = 0; // int
 312          s__ = 0;} break;
 313       case a_Literal::tag_STRING: {
 314          int s0__;
 315          labeler(_STRING(redex)->STRING, s0__, r__);
 316          s__ = 0;} break;
 317       default: {
 318          int s0__;
 319          s0__ = 0; // Bool
 320          s__ = 0;} break;
 321    }
 322
 323 }
 324
 325 void  RemoveDuplicateNames::labeler (a_List<Exp> *  & redex, int& s__, int r__)
 326 {
 327 replacement__:
 328    if ((redex)) {
 329       int s0__;
 330       int s1__;
 331       labeler(redex->_1, s0__, r__);
 332       labeler(redex->_2, s1__, r__);
 333       s__ = 0;
 334    } else {s__ = 0;
 335    }
 336
 337 }
 338
 339 #line 101 "rename.pcc"
 340 #line 101 "rename.pcc"
 341
 342 #line 102 "rename.pcc"
 343 /*
 344 ------------------------------- Statistics -------------------------------
 345 Merge matching rules         = yes
 346 Number of DFA nodes merged   = 16
 347 Number of ifs generated      = 5
 348 Number of switches generated = 2
 349 Number of labels             = 0
 350 Number of gotos              = 0
 351 Adaptive matching            = disabled
 352 Fast string matching         = disabled
 353 Inline downcasts             = disabled
 354 --------------------------------------------------------------------------
 355 */