prop-src/trs2.cc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //  This file is generated automatically using Prop (version 2.3.6),
   3 //  last updated on Nov 2, 1999.
   4 //  The original source file is "trs2.pcc".
   5 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #define PROP_STRCMP_USED
   8 #define PROP_TUPLE2_USED
   9 #include <propdefs.h>
  10 #line 1 "trs2.pcc"
  11 ///////////////////////////////////////////////////////////////////////////////
  12 //
  13 //  This is the main partial evaluation routines.
  14 //
  15 ///////////////////////////////////////////////////////////////////////////////
  16 #include <iostream>
  17 #include <string.h>
  18 #include <stdlib.h>
  19 #include "trs.h"
  20 #include "ir.h"
  21 #include "ast.h"
  22 #include "type.h"
  23 #include "list.h"
  24 #include "matchcom.h"
  25 #include "funmap.h"
  26 #include "rwgen.h"
  27
  28 ///////////////////////////////////////////////////////////////////////////////
  29 //
  30 //  Type definitions
  31 //
  32 ///////////////////////////////////////////////////////////////////////////////
  33 typedef TreeAutomaton::Functor Functor;
  34 typedef TreeAutomaton::State   State;
  35 typedef TreeAutomaton::Rule    Rule;
  36
  37 ///////////////////////////////////////////////////////////////////////////////
  38 //
  39 //  Method for partial evaluating the trs
  40 //
  41 ///////////////////////////////////////////////////////////////////////////////
  42 void TRS::mix()
  43 {  for (Rule r = 0; r < number_of_rules; r++)
  44    {  mix(r);
  45    }
  46 }
  47
  48 ///////////////////////////////////////////////////////////////////////////////
  49 //
  50 //  Method for partial evaluating one rule
  51 //
  52 ///////////////////////////////////////////////////////////////////////////////
  53 void TRS::mix(Rule r)
  54 {  mix_0(r);
  55    mix_1(r);
  56 }
  57
  58 ///////////////////////////////////////////////////////////////////////////////
  59 //
  60 //  Method for partial evaluting one rule, using 0-strategy.
  61 //
  62 ///////////////////////////////////////////////////////////////////////////////
  63 void TRS::mix_0(Rule r)
  64 {  int arity = num_var_map[r];
  65    for (int i = 0; i < arity; i++) states[i] = 0;
  66    // msg("0-Partial evaluating %r ", rule_map[r]) << rhs_map[r] << '\n';
  67    Term rhs = copy(rhs_map[r]);
  68    int reductions = 0;
  69    State new_state = normalize(rhs,reductions);
  70    if (reductions > 0)
  71    {  print_residue(r,rhs);
  72       make_rhs(r,optimized_map[r] = make_exp(rhs));
  73    }
  74 }
  75
  76 ///////////////////////////////////////////////////////////////////////////////
  77 //
  78 //  Method for partial evaluting one rule, using 1-strategy.
  79 //
  80 ///////////////////////////////////////////////////////////////////////////////
  81 void TRS::mix_1(Rule r)
  82 {  int arity            = num_var_map[r];
  83    int number_of_states = treeauto.number_of_states();
  84    // msg("1-Partial evaluating %r ", rule_map[r]) << rhs_map[r] << '\n';
  85    for (int i = 0; i < arity; i++)
  86    {  // If the variable does not have an index we can't do anything
  87       // with it.
  88       if (! compiler.has_index(var_pat_map[r][i]->ty)) continue;
  89       for (int j = 0; j < arity; j++) states[j] = 0;
  90       for (State s = 1; s < number_of_states; s++)
  91       {  // skip accept states
  92          states[i] = s;
  93          if (treeauto.is_accept_state(s)) continue;
  94          if (! is_relevant(r)) continue;
  95          int reductions = 0;
  96          Term rhs = copy(rhs_map[r]);
  97          State new_state = normalize(rhs,reductions);
  98          if (reductions > 0)
  99          {  generate_residue(r,i,s,rhs); }
 100       }
 101    }
 102 }
 103
 104 ///////////////////////////////////////////////////////////////////////////////
 105 //
 106 //  Method to check that a particular specialization is relevant
 107 //
 108 ///////////////////////////////////////////////////////////////////////////////
 109 Bool TRS::is_relevant(Rule r)
 110 {  int redex_count = 0;
 111    count_redex = true;
 112    State s = normalize(lhs_map[r],redex_count);
 113    count_redex = false;
 114    // cerr << lhs_map[r] << " has " << redex_count << " redexes\n";
 115    if (redex_count > 1) return false;
 116    if (treeauto.accept1_rule(s) != r) return false;
 117    return true;
 118 }
 119
 120 ///////////////////////////////////////////////////////////////////////////////
 121 //
 122 //  Method to normalize a rule
 123 //
 124 ///////////////////////////////////////////////////////////////////////////////
 125 TRS::State TRS::normalize(Term& term, int& reductions)
 126 {  Bool changed;
 127    State new_state;
 128    do {
 129       changed = false;
 130
 131 #line 120 "trs2.pcc"
 132 #line 138 "trs2.pcc"
 133 {
 134    switch (term->tag__) {
 135       case a_Term::tag_CONSterm: {
 136 #line 122 "trs2.pcc"
 137        int mu[MAX_VARS];
 138          for (int i = 0; i < ((Term_CONSterm *)term)->_3; i++)
 139          {  State s = normalize(((Term_CONSterm *)term)->_4[i],reductions);
 140             mu[i]   = treeauto.index_map(((Term_CONSterm *)term)->_1,i,s);
 141          }
 142          new_state = treeauto.get_delta(((Term_CONSterm *)term)->_1,mu);
 143          // Check for redex
 144          if (treeauto.is_accept_state(new_state))
 145          {  if (count_redex) {
 146                           reductions++;
 147                           return new_state;
 148             }
 149                        term = reduce(term,new_state,reductions,changed);
 150          }
 151
 152 #line 136 "trs2.pcc"
 153          } break;
 154       case a_Term::tag_VARterm: {
 155 #line 137 "trs2.pcc"
 156         return states[((Term_VARterm *)term)->_1];
 157 #line 137 "trs2.pcc"
 158          } break;
 159       default: {
 160 #line 138 "trs2.pcc"
 161         return 0;
 162 #line 138 "trs2.pcc"
 163          } break;
 164    }
 165 }
 166 #line 139 "trs2.pcc"
 167 #line 139 "trs2.pcc"
 168
 169    } while (changed);
 170    return new_state;
 171 }
 172
 173 ///////////////////////////////////////////////////////////////////////////////
 174 //
 175 //  Method to reduce a rule during accepting
 176 //
 177 ///////////////////////////////////////////////////////////////////////////////
 178 Term TRS::reduce(Term term, State state, int& reductions, Bool& changed)
 179 {
 180    // Test for conditional rules
 181    // For each rule that can accept, check the guard associated
 182    // with the rule.  Evaluate the guard if possible.
 183    // We'll not reduce if we are not guaranteed that the reduction
 184    // can be performed.
 185    const BitSet& accept = treeauto.accept_rules(state);
 186    for (Rule r = 0; r <= number_of_rules; r++)
 187    {  if (accept[r])
 188       {  Exp guard = guard_map[r];
 189          EvalResult result = SUCCESS;
 190          if (guard == NOexp) result = SUCCESS;
 191          else result = eval_guard(guard);
 192          switch (result)
 193          {  case SUCCESS:
 194             {  Term rule_rhs = rhs_map[r];
 195                Bool ok = true;
 196                Term new_rhs = subst(rule_rhs,term,ok);
 197                if (! ok) return term; // no reduction
 198                reductions++;
 199                changed = true;
 200                return new_rhs;
 201             } break;
 202             case UNKNOWN: return term; // no reduction
 203             case FAILURE:  break; // try next rule
 204          }
 205       }
 206    }
 207    return term;  // no reduction
 208 }
 209
 210 ///////////////////////////////////////////////////////////////////////////////
 211 //
 212 //  Apply a rule
 213 //
 214 ///////////////////////////////////////////////////////////////////////////////
 215 Term TRS::subst(Term rhs, Term redex, Bool& ok)
 216 {
 217 #line 187 "trs2.pcc"
 218 #line 194 "trs2.pcc"
 219 {
 220    switch (rhs->tag__) {
 221       case a_Term::tag_CONSterm: {
 222 #line 189 "trs2.pcc"
 223        return CONSterm(((Term_CONSterm *)rhs)->_1,((Term_CONSterm *)rhs)->_2,((Term_CONSterm *)rhs)->_3,subst(((Term_CONSterm *)rhs)->_3,((Term_CONSterm *)rhs)->_4,redex,ok));
 224 #line 189 "trs2.pcc"
 225          } break;
 226       case a_Term::tag_VARterm: {
 227 #line 191 "trs2.pcc"
 228        return proj(((Term_VARterm *)rhs)->_3,redex,ok);
 229 #line 191 "trs2.pcc"
 230          } break;
 231       case a_Term::tag_CODEterm: {
 232 #line 193 "trs2.pcc"
 233        return proj(((Term_CODEterm *)rhs)->CODEterm,redex,ok);
 234 #line 193 "trs2.pcc"
 235          } break;
 236       default: {
 237 #line 194 "trs2.pcc"
 238         bug("TRS::subst"); return redex;
 239 #line 194 "trs2.pcc"
 240          } break;
 241    }
 242 }
 243 #line 195 "trs2.pcc"
 244 #line 195 "trs2.pcc"
 245
 246 }
 247
 248 ///////////////////////////////////////////////////////////////////////////////
 249 //
 250 //  Apply a rule
 251 //
 252 ///////////////////////////////////////////////////////////////////////////////
 253 Term * TRS::subst(int n, Term * rhs, Term redex, Bool& ok)
 254 {  Term * args = (Term*)mem_pool.m_alloc(sizeof(Term) * n);
 255    for (int i = 0; i < n; i++)
 256       args[i] = subst(rhs[i],redex,ok);
 257    return args;
 258 }
 259
 260 ///////////////////////////////////////////////////////////////////////////////
 261 //
 262 //  Perform projection a rule
 263 //
 264 ///////////////////////////////////////////////////////////////////////////////
 265 Term TRS::proj(Exp exp, Term redex, Bool& ok)
 266 {  int nth;
 267
 268 #line 217 "trs2.pcc"
 269 #line 260 "trs2.pcc"
 270 {
 271    if (exp) {
 272       switch (exp->tag__) {
 273          case a_Exp::tag_IDexp: {
 274             if (_equal_string(((Exp_IDexp *)exp)->IDexp,"redex")) {
 275 #line 218 "trs2.pcc"
 276            return redex;
 277 #line 218 "trs2.pcc"
 278 }
 279             else {
 280             L1:;
 281 #line 256 "trs2.pcc"
 282           // msg("3 Can't project %e ", exp);
 283                  // print(msg(""),redex); msg("\n");
 284                  ok = false;
 285                      return CODEterm(NOexp);
 286
 287 #line 260 "trs2.pcc"
 288 }
 289             } break;
 290          case a_Exp::tag_DOTexp: {
 291             if (((Exp_DOTexp *)exp)->_1) {
 292                switch (((Exp_DOTexp *)exp)->_1->tag__) {
 293                   case a_Exp::tag_SELECTORexp: {
 294 #line 220 "trs2.pcc"
 295
 296 #line 220 "trs2.pcc"
 297 #line 238 "trs2.pcc"
 298                      {
 299                         Term _V1 = proj(((Exp_SELECTORexp *)((Exp_DOTexp *)exp)->_1)->_1,redex,ok);
 300                         switch (_V1->tag__) {
 301                            case a_Term::tag_CONSterm: {
 302                               if (
 303 #line 221 "trs2.pcc"
 304                               ((((Exp_SELECTORexp *)((Exp_DOTexp *)exp)->_1)->_2 == ((Term_CONSterm *)_V1)->_2) && (nth = (atol((((Exp_DOTexp *)exp)->_2 + 1)) - 1)),(nth < ((Term_CONSterm *)_V1)->_3))
 305 #line 222 "trs2.pcc"
 306 ) {
 307
 308 #line 223 "trs2.pcc"
 309                                return ((Term_CONSterm *)_V1)->_4[nth];
 310 #line 223 "trs2.pcc"
 311                               } else {
 312
 313 #line 228 "trs2.pcc"
 314                                // msg("1 Can't project %e %i %i", exp,nth,n);
 315                                                // print(msg(""),redex); msg("\n");
 316                                                ok = false;
 317                                                 return _V1;
 318
 319 #line 232 "trs2.pcc"
 320                               }
 321                               } break;
 322                            case a_Term::tag_VARterm: {
 323 #line 226 "trs2.pcc"
 324                              return CODEterm(DOTexp(SELECTORexp(((Term_VARterm *)_V1)->_3,((Exp_SELECTORexp *)((Exp_DOTexp *)exp)->_1)->_2,((Exp_SELECTORexp *)((Exp_DOTexp *)exp)->_1)->_3),((Exp_DOTexp *)exp)->_2));
 325 #line 226 "trs2.pcc"
 326                               } break;
 327                            case a_Term::tag_CODEterm: {
 328 #line 224 "trs2.pcc"
 329                              return CODEterm(DOTexp(SELECTORexp(((Term_CODEterm *)_V1)->CODEterm,((Exp_SELECTORexp *)((Exp_DOTexp *)exp)->_1)->_2,((Exp_SELECTORexp *)((Exp_DOTexp *)exp)->_1)->_3),((Exp_DOTexp *)exp)->_2));
 330 #line 224 "trs2.pcc"
 331                               } break;
 332                            default: {
 333 #line 234 "trs2.pcc"
 334                             // msg("1 Can't project %e", exp);
 335                                        // print(msg(""),redex); msg("\n");
 336                                        ok = false;
 337                                              return redex;
 338
 339 #line 238 "trs2.pcc"
 340                               } break;
 341                         }
 342                      }
 343 #line 239 "trs2.pcc"
 344 #line 239 "trs2.pcc"
 345
 346
 347 #line 240 "trs2.pcc"
 348                      } break;
 349                   default: { goto L1; } break;
 350                }
 351             } else { goto L1; }
 352             } break;
 353          case a_Exp::tag_SELECTORexp: {
 354 #line 242 "trs2.pcc"
 355
 356 #line 242 "trs2.pcc"
 357 #line 252 "trs2.pcc"
 358             {
 359                Term _V2 = proj(((Exp_SELECTORexp *)exp)->_1,redex,ok);
 360                switch (_V2->tag__) {
 361                   case a_Term::tag_CONSterm: {
 362                      if (
 363 #line 243 "trs2.pcc"
 364                      (((Exp_SELECTORexp *)exp)->_2 == ((Term_CONSterm *)_V2)->_2)
 365 #line 243 "trs2.pcc"
 366 ) {
 367
 368 #line 244 "trs2.pcc"
 369                       return ((Term_CONSterm *)_V2)->_4[0];
 370 #line 244 "trs2.pcc"
 371                      } else {
 372
 373                         L2:;
 374 #line 248 "trs2.pcc"
 375                       // msg("2 Can't project %e ", exp);
 376                                        // print(msg(""),redex); msg("\n");
 377                                        ok = false;
 378                                        return _V2;
 379
 380 #line 252 "trs2.pcc"
 381                      }
 382                      } break;
 383                   case a_Term::tag_VARterm: {
 384 #line 246 "trs2.pcc"
 385                     return CODEterm(SELECTORexp(((Term_VARterm *)_V2)->_3,((Exp_SELECTORexp *)exp)->_2,((Exp_SELECTORexp *)exp)->_3));
 386 #line 246 "trs2.pcc"
 387                      } break;
 388                   case a_Term::tag_CODEterm: {
 389 #line 245 "trs2.pcc"
 390                     return CODEterm(SELECTORexp(((Term_CODEterm *)_V2)->CODEterm,((Exp_SELECTORexp *)exp)->_2,((Exp_SELECTORexp *)exp)->_3));
 391 #line 245 "trs2.pcc"
 392                      } break;
 393                   default: { goto L2; } break;
 394                }
 395             }
 396 #line 253 "trs2.pcc"
 397 #line 253 "trs2.pcc"
 398
 399
 400 #line 254 "trs2.pcc"
 401             } break;
 402          default: { goto L1; } break;
 403       }
 404    } else { goto L1; }
 405 }
 406 #line 261 "trs2.pcc"
 407 #line 261 "trs2.pcc"
 408
 409 }
 410
 411 ///////////////////////////////////////////////////////////////////////////////
 412 //
 413 //  Compose two projection expression
 414 //
 415 ///////////////////////////////////////////////////////////////////////////////
 416 Exp TRS::proj(Exp e1, Exp e2, Bool& ok)
 417 {
 418 #line 270 "trs2.pcc"
 419 #line 274 "trs2.pcc"
 420 {
 421    if (e1) {
 422       switch (e1->tag__) {
 423          case a_Exp::tag_IDexp: {
 424             if (_equal_string(((Exp_IDexp *)e1)->IDexp,"redex")) {
 425 #line 271 "trs2.pcc"
 426            return e2;
 427 #line 271 "trs2.pcc"
 428 }
 429             else {
 430             L3:;
 431 #line 274 "trs2.pcc"
 432            msg("Can't project %e %e\n", e1, e2);  return NOexp;
 433 #line 274 "trs2.pcc"
 434 }
 435             } break;
 436          case a_Exp::tag_DOTexp: {
 437 #line 273 "trs2.pcc"
 438            return DOTexp(proj(((Exp_DOTexp *)e1)->_1,e2,ok),((Exp_DOTexp *)e1)->_2);
 439 #line 273 "trs2.pcc"
 440             } break;
 441          case a_Exp::tag_SELECTORexp: {
 442 #line 272 "trs2.pcc"
 443            return SELECTORexp(proj(((Exp_SELECTORexp *)e1)->_1,e2,ok),((Exp_SELECTORexp *)e1)->_2,((Exp_SELECTORexp *)e1)->_3);
 444 #line 272 "trs2.pcc"
 445             } break;
 446          default: { goto L3; } break;
 447       }
 448    } else { goto L3; }
 449 }
 450 #line 275 "trs2.pcc"
 451 #line 275 "trs2.pcc"
 452
 453 }
 454
 455 ///////////////////////////////////////////////////////////////////////////////
 456 //
 457 //  Copying the rhs
 458 //
 459 ///////////////////////////////////////////////////////////////////////////////
 460 Term TRS::copy(Term rhs)
 461 {
 462 #line 284 "trs2.pcc"
 463 #line 287 "trs2.pcc"
 464 {
 465    switch (rhs->tag__) {
 466       case a_Term::tag_CONSterm: {
 467 #line 286 "trs2.pcc"
 468        return CONSterm(((Term_CONSterm *)rhs)->_1,((Term_CONSterm *)rhs)->_2,((Term_CONSterm *)rhs)->_3,copy(((Term_CONSterm *)rhs)->_3,((Term_CONSterm *)rhs)->_4));
 469 #line 286 "trs2.pcc"
 470          } break;
 471       default: {
 472 #line 287 "trs2.pcc"
 473         return rhs;
 474 #line 287 "trs2.pcc"
 475          } break;
 476    }
 477 }
 478 #line 288 "trs2.pcc"
 479 #line 288 "trs2.pcc"
 480
 481 }
 482
 483 ///////////////////////////////////////////////////////////////////////////////
 484 //
 485 //  Copying the rhs
 486 //
 487 ///////////////////////////////////////////////////////////////////////////////
 488 Term * TRS::copy(int n, Term rhs [])
 489 {  Term * args = (Term*)mem_pool.m_alloc(sizeof(Term) * n);
 490    for (int i = 0; i < n; i++)
 491       args[i] = copy(rhs[i]);
 492    return args;
 493 }
 494
 495 ///////////////////////////////////////////////////////////////////////////////
 496 //
 497 //  Method to evaluate a guard expression
 498 //
 499 ///////////////////////////////////////////////////////////////////////////////
 500 TRS::EvalResult TRS::eval_guard(Exp exp)
 501 {  return UNKNOWN;
 502 }
 503
 504 ///////////////////////////////////////////////////////////////////////////////
 505 //
 506 //  Method to print out the residue.
 507 //
 508 ///////////////////////////////////////////////////////////////////////////////
 509 void TRS::print_residue(Rule r, Term rhs_residue) const
 510 {  std::ostream& log = open_logfile();
 511    MatchRule rule = rule_map[r];
 512    log << "line " << rule->begin_line << ": "
 513        << rule_map[r] << ' ';
 514    print(log, rhs_map[r]); log << '\n';
 515    for (int i = 0; i < num_var_map[r]; i++)
 516    {  if (states[i] != 0)
 517       {  log << "\twhen " << var_pat_map[r][i] << " is in state:\n";
 518          treeauto.print_state(log,states[i]);
 519       }
 520    }
 521    log << "\toptimize rhs to ";
 522    print(log,rhs_residue);
 523    log << "\n\n";
 524 }
 525 #line 333 "trs2.pcc"
 526 /*
 527 ------------------------------- Statistics -------------------------------
 528 Merge matching rules         = yes
 529 Number of DFA nodes merged   = 121
 530 Number of ifs generated      = 7
 531 Number of switches generated = 8
 532 Number of labels             = 3
 533 Number of gotos              = 7
 534 Adaptive matching            = enabled
 535 Fast string matching         = disabled
 536 Inline downcasts             = enabled
 537 --------------------------------------------------------------------------
 538 */