prop-src/trs.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 "trs.pcc".
   5 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #define PROP_STRCMP_USED
   8 #define PROP_TUPLE2_USED
   9 #include <propdefs.h>
  10 #line 1 "trs.pcc"
  11 ///////////////////////////////////////////////////////////////////////////////
  12 //
  13 //  These are the routines for building the data structure
  14 //  for partial evaluting a TRS
  15 //
  16 ///////////////////////////////////////////////////////////////////////////////
  17 #include <iostream.h>
  18 #include <string.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 "datagen.h"
  26 #include "rwgen.h"
  27 #include "funmap.h"
  28 #include "setlgen.h"
  29
  30 ///////////////////////////////////////////////////////////////////////////////
  31 //
  32 //  Constructors for represents a term
  33 //
  34 ///////////////////////////////////////////////////////////////////////////////
  35 #line 25 "trs.pcc"
  36 #line 25 "trs.pcc"
  37 ///////////////////////////////////////////////////////////////////////////////
  38 //
  39 // Interface specification of datatype Term
  40 //
  41 ///////////////////////////////////////////////////////////////////////////////
  42 #line 25 "trs.pcc"
  43
  44
  45 ///////////////////////////////////////////////////////////////////////////////
  46 //
  47 // Instantiation of datatype Term
  48 //
  49 ///////////////////////////////////////////////////////////////////////////////
  50 #line 25 "trs.pcc"
  51 Term_CONSterm::Term_CONSterm (TreeAutomaton::Functor x_1, Cons x_2, int x_3, Term * x_4)
  52  : a_Term(tag_CONSterm), _1(x_1), _2(x_2), _3(x_3), _4(x_4)
  53 {
  54 }
  55 a_Term * CONSterm (TreeAutomaton::Functor x_1, Cons x_2, int x_3, Term * x_4)
  56 {
  57    return new Term_CONSterm (x_1, x_2, x_3, x_4);
  58 }
  59 Term_VARterm::Term_VARterm (int x_1, Pat x_2, Exp x_3)
  60  : a_Term(tag_VARterm), _1(x_1), _2(x_2), _3(x_3)
  61 {
  62 }
  63 a_Term * VARterm (int x_1, Pat x_2, Exp x_3)
  64 {
  65    return new Term_VARterm (x_1, x_2, x_3);
  66 }
  67 Term_CODEterm::Term_CODEterm (Exp x_CODEterm)
  68  : a_Term(tag_CODEterm), CODEterm(x_CODEterm)
  69 {
  70 }
  71 a_Term * CODEterm (Exp x_CODEterm)
  72 {
  73    return new Term_CODEterm (x_CODEterm);
  74 }
  75 Term_OPAQUEterm::Term_OPAQUEterm (Decls x_OPAQUEterm)
  76  : a_Term(tag_OPAQUEterm), OPAQUEterm(x_OPAQUEterm)
  77 {
  78 }
  79 a_Term * OPAQUEterm (Decls x_OPAQUEterm)
  80 {
  81    return new Term_OPAQUEterm (x_OPAQUEterm);
  82 }
  83 Term_PATterm::Term_PATterm (Pat x_PATterm)
  84  : a_Term(tag_PATterm), PATterm(x_PATterm)
  85 {
  86 }
  87 a_Term * PATterm (Pat x_PATterm)
  88 {
  89    return new Term_PATterm (x_PATterm);
  90 }
  91
  92
  93 #line 25 "trs.pcc"
  94 #line 25 "trs.pcc"
  95
  96
  97 ///////////////////////////////////////////////////////////////////////////////
  98 //
  99 //  Constructor for TRS
 100 //
 101 ///////////////////////////////////////////////////////////////////////////////
 102 TRS::TRS(RewritingCompiler& C)
 103    : compiler(C), Fmap(*C.Fmap), treeauto(*C.Fmap->tree_gen),
 104      count_redex(false)
 105 {
 106    MatchRules rules = Fmap.bottomup_rules;
 107    number_of_rules  = length(rules);
 108    rule_map    = new MatchRule [number_of_rules];
 109    guard_map   = new Exp       [number_of_rules];
 110    lhs_map     = new Term      [number_of_rules];
 111    rhs_map     = new Term      [number_of_rules];
 112    num_var_map = new int       [number_of_rules];
 113    var_map     = new Exp *     [number_of_rules];
 114    var_pat_map = new Pat *     [number_of_rules];
 115    residue_map = new Residues *[number_of_rules];
 116    literal_map = new Literal   [Fmap.G.functors()];
 117    optimized_map = new Exp     [number_of_rules];
 118
 119    clear_statistics();
 120
 121    int i = 0;
 122    for_each(MatchRule, r, rules)
 123    {
 124 #line 53 "trs.pcc"
 125 #line 63 "trs.pcc"
 126 {
 127 #line 55 "trs.pcc"
 128  if (r->rule_number != i) bug("%LTRS::TRS()");
 129    rule_map[i]  = r;
 130    guard_map[i] = r->_3;
 131             make_lhs(i,r->_2);
 132
 133 #line 59 "trs.pcc"
 134 #line 61 "trs.pcc"
 135    {
 136       a_List<Decl> *  _V1 = r->_5;
 137       if (_V1) {
 138          if (_V1->_1) {
 139             switch (_V1->_1->tag__) {
 140                case a_Decl::tag_MARKEDdecl: {
 141                   if (((Decl_MARKEDdecl *)_V1->_1)->_2) {
 142                      switch (((Decl_MARKEDdecl *)_V1->_1)->_2->tag__) {
 143                         case a_Decl::tag_REPLACEMENTdecl: {
 144                            if (_V1->_2) {
 145                               L1:;
 146 #line 61 "trs.pcc"
 147                              rhs_map[i] = OPAQUEterm(r->_5);
 148 #line 61 "trs.pcc"
 149                            } else {
 150 #line 60 "trs.pcc"
 151                              make_rhs(i,((Decl_REPLACEMENTdecl *)((Decl_MARKEDdecl *)_V1->_1)->_2)->_1);
 152 #line 60 "trs.pcc"
 153                            }
 154                            } break;
 155                         default: { goto L1; } break;
 156                      }
 157                   } else { goto L1; }
 158                   } break;
 159                default: { goto L1; } break;
 160             }
 161          } else { goto L1; }
 162       } else { goto L1; }
 163    }
 164 #line 62 "trs.pcc"
 165 #line 62 "trs.pcc"
 166
 167
 168 #line 63 "trs.pcc"
 169 }
 170 #line 64 "trs.pcc"
 171 #line 64 "trs.pcc"
 172
 173       i++;
 174    }
 175 }
 176
 177 ///////////////////////////////////////////////////////////////////////////////
 178 //
 179 //  Destructor for TRS
 180 //
 181 ///////////////////////////////////////////////////////////////////////////////
 182 TRS::~TRS()
 183 {  delete [] rule_map;
 184    delete [] guard_map;
 185    delete [] lhs_map;
 186    delete [] rhs_map;
 187    delete [] num_var_map;
 188    delete [] var_map;
 189    delete [] var_pat_map;
 190    delete [] residue_map;
 191    delete [] literal_map;
 192    delete [] optimized_map;
 193 }
 194
 195 ///////////////////////////////////////////////////////////////////////////////
 196 //
 197 //  Method to determine if any expression is a pattern variable.
 198 //
 199 ///////////////////////////////////////////////////////////////////////////////
 200 Bool is_pattern_var(Exp exp)
 201 {
 202 #line 93 "trs.pcc"
 203 #line 98 "trs.pcc"
 204 {
 205    for (;;) {
 206       if (exp) {
 207          switch (exp->tag__) {
 208             case a_Exp::tag_DOTexp: {
 209                if (((Exp_DOTexp *)exp)->_1) {
 210                   switch (((Exp_DOTexp *)exp)->_1->tag__) {
 211                      case a_Exp::tag_SELECTORexp: {
 212                         if (((Exp_SELECTORexp *)((Exp_DOTexp *)exp)->_1)->_1) {
 213                            switch (((Exp_SELECTORexp *)((Exp_DOTexp *)exp)->_1)->_1->tag__) {
 214                               case a_Exp::tag_IDexp: {
 215                                  if (_equal_string(((Exp_IDexp *)((Exp_SELECTORexp *)((Exp_DOTexp *)exp)->_1)->_1)->IDexp,"redex")) {
 216 #line 95 "trs.pcc"
 217                                 return true;
 218 #line 95 "trs.pcc"
 219 }
 220                                  else {
 221                                  L3:;
 222 #line 96 "trs.pcc"
 223                                 exp = ((Exp_SELECTORexp *)((Exp_DOTexp *)exp)->_1)->_1;
 224 #line 96 "trs.pcc"
 225 }
 226                                  } break;
 227                               default: { goto L3; } break;
 228                            }
 229                         } else { goto L3; }
 230                         } break;
 231                      default: {
 232                         L4:;
 233 #line 98 "trs.pcc"
 234                        return false;
 235 #line 98 "trs.pcc"
 236                         } break;
 237                   }
 238                } else { goto L4; }
 239                } break;
 240             case a_Exp::tag_SELECTORexp: {
 241                if (((Exp_SELECTORexp *)exp)->_1) {
 242                   switch (((Exp_SELECTORexp *)exp)->_1->tag__) {
 243                      case a_Exp::tag_IDexp: {
 244                         if (_equal_string(((Exp_IDexp *)((Exp_SELECTORexp *)exp)->_1)->IDexp,"redex")) {
 245 #line 94 "trs.pcc"
 246                        return true;
 247 #line 94 "trs.pcc"
 248 }
 249                         else {
 250                         L5:;
 251 #line 97 "trs.pcc"
 252                        exp = ((Exp_SELECTORexp *)exp)->_1;
 253 #line 97 "trs.pcc"
 254 }
 255                         } break;
 256                      default: { goto L5; } break;
 257                   }
 258                } else { goto L5; }
 259                } break;
 260             default: { goto L4; } break;
 261          }
 262       } else { goto L4; }
 263    }
 264 }
 265 #line 99 "trs.pcc"
 266 #line 99 "trs.pcc"
 267
 268 }
 269
 270 ///////////////////////////////////////////////////////////////////////////////
 271 //
 272 //  Method to create the lhs
 273 //
 274 ///////////////////////////////////////////////////////////////////////////////
 275 void TRS::make_lhs(Rule r, Pat pat)
 276 {  num_vars = 0;
 277    lhs_map[r] = make_term(pat);
 278
 279    num_var_map[r] = num_vars;
 280    var_map[r]     = (Exp*)mem_pool.m_alloc(sizeof(Exp)*num_vars);
 281    var_pat_map[r] = (Pat*)mem_pool.m_alloc(sizeof(Pat)*num_vars);
 282    residue_map[r] = (Residues*)mem_pool.c_alloc(sizeof(Residues)*num_vars);
 283    optimized_map[r] = NOexp;
 284
 285    memcpy(var_map[r],    vars,    sizeof(Exp)*num_vars);
 286    memcpy(var_pat_map[r],var_pats,sizeof(Pat)*num_vars);
 287 }
 288
 289 ///////////////////////////////////////////////////////////////////////////////
 290 //
 291 //  Method to create the lhs for rule r
 292 //
 293 ///////////////////////////////////////////////////////////////////////////////
 294 Term TRS::make_term(Pat pat)
 295 {
 296 #line 127 "trs.pcc"
 297 #line 148 "trs.pcc"
 298 {
 299    for (;;) {
 300       if (pat) {
 301          switch (pat->tag__) {
 302             case a_Pat::tag_IDpat: {
 303 #line 130 "trs.pcc"
 304               return make_term_var(pat,pat->selector);
 305 #line 130 "trs.pcc"
 306                } break;
 307             case a_Pat::tag_CONSpat: {
 308 #line 133 "trs.pcc"
 309               return make_term(pat,((Pat_CONSpat *)pat)->CONSpat,
 310 #line 133 "trs.pcc"
 311 #line 133 "trs.pcc"
 312                nil_1_
 313 #line 133 "trs.pcc"
 314 #line 133 "trs.pcc"
 315                );
 316 #line 133 "trs.pcc"
 317                } break;
 318             case a_Pat::tag_APPpat: {
 319                if (((Pat_APPpat *)pat)->_1) {
 320                   switch (((Pat_APPpat *)pat)->_1->tag__) {
 321                      case a_Pat::tag_CONSpat: {
 322                         if (((Pat_APPpat *)pat)->_2) {
 323                            switch (((Pat_APPpat *)pat)->_2->tag__) {
 324                               case a_Pat::tag_TUPLEpat: {
 325 #line 131 "trs.pcc"
 326                                 return make_term(pat,((Pat_CONSpat *)((Pat_APPpat *)pat)->_1)->CONSpat,((Pat_TUPLEpat *)((Pat_APPpat *)pat)->_2)->TUPLEpat);
 327 #line 131 "trs.pcc"
 328                                  } break;
 329                               default: {
 330                                  L7:;
 331 #line 132 "trs.pcc"
 332                                 return make_term(pat,((Pat_CONSpat *)((Pat_APPpat *)pat)->_1)->CONSpat,
 333 #line 132 "trs.pcc"
 334 #line 132 "trs.pcc"
 335                                  list_1_(((Pat_APPpat *)pat)->_2)
 336 #line 132 "trs.pcc"
 337 #line 132 "trs.pcc"
 338                                  );
 339 #line 132 "trs.pcc"
 340                                  } break;
 341                            }
 342                         } else { goto L7; }
 343                         } break;
 344                      default: {
 345                         L8:;
 346 #line 148 "trs.pcc"
 347                        return PATterm(pat);
 348 #line 148 "trs.pcc"
 349                         } break;
 350                   }
 351                } else { goto L8; }
 352                } break;
 353             case a_Pat::tag_ASpat: {
 354 #line 129 "trs.pcc"
 355               pat = ((Pat_ASpat *)pat)->_2;
 356 #line 129 "trs.pcc"
 357                } break;
 358             case a_Pat::tag_LITERALpat: {
 359                if (
 360 #line 143 "trs.pcc"
 361                Fmap.literal_map.contains(((Pat_LITERALpat *)pat)->LITERALpat)
 362 #line 143 "trs.pcc"
 363 ) {
 364
 365 #line 144 "trs.pcc"
 366                 Functor f = Fmap.literal_map[((Pat_LITERALpat *)pat)->LITERALpat];
 367                          literal_map[f] = ((Pat_LITERALpat *)pat)->LITERALpat;
 368                          return CONSterm(f,NOcons,0,0);
 369
 370 #line 147 "trs.pcc"
 371                } else {
 372                    goto L8; }
 373                } break;
 374             case a_Pat::tag_LISTpat: {
 375                if (((Pat_LISTpat *)pat)->head) {
 376 #line 139 "trs.pcc"
 377                 Pat tl_pat =
 378 #line 139 "trs.pcc"
 379 #line 139 "trs.pcc"
 380                   LISTpat(((Pat_LISTpat *)pat)->cons, ((Pat_LISTpat *)pat)->nil, ((Pat_LISTpat *)pat)->head->_2, ((Pat_LISTpat *)pat)->tail)
 381 #line 139 "trs.pcc"
 382 #line 139 "trs.pcc"
 383                   ;
 384                          tl_pat->ty = pat->ty;
 385                          return make_term(pat,((Pat_LISTpat *)pat)->cons,
 386 #line 141 "trs.pcc"
 387 #line 141 "trs.pcc"
 388                   list_1_(((Pat_LISTpat *)pat)->head->_1,list_1_(tl_pat))
 389 #line 141 "trs.pcc"
 390 #line 141 "trs.pcc"
 391                   );
 392
 393 #line 142 "trs.pcc"
 394                } else {
 395                   if (((Pat_LISTpat *)pat)->tail) {
 396 #line 137 "trs.pcc"
 397                    pat = ((Pat_LISTpat *)pat)->tail;
 398 #line 137 "trs.pcc"
 399                   } else {
 400 #line 135 "trs.pcc"
 401                    return make_term(pat,((Pat_LISTpat *)pat)->nil,
 402 #line 135 "trs.pcc"
 403 #line 135 "trs.pcc"
 404                      nil_1_
 405 #line 135 "trs.pcc"
 406 #line 135 "trs.pcc"
 407                      );
 408 #line 135 "trs.pcc"
 409                   }
 410                }
 411                } break;
 412             case a_Pat::tag_MARKEDpat: {
 413 #line 128 "trs.pcc"
 414               pat = ((Pat_MARKEDpat *)pat)->_2;
 415 #line 128 "trs.pcc"
 416                } break;
 417             default: { goto L8; } break;
 418          }
 419       } else { goto L8; }
 420    }
 421 }
 422 #line 149 "trs.pcc"
 423 #line 149 "trs.pcc"
 424
 425 }
 426
 427 ///////////////////////////////////////////////////////////////////////////////
 428 //
 429 //  Method to create the lhs for rule r
 430 //
 431 ///////////////////////////////////////////////////////////////////////////////
 432 Term TRS::make_term(Pat pat, Cons cons, Pats pats)
 433 {  int n       = length(pats);
 434    FunctorTable::Entry * E = Fmap.type_map.lookup(pat->ty);
 435    if (E == 0) { return PATterm(pat); }
 436
 437 #line 161 "trs.pcc"
 438 #line 167 "trs.pcc"
 439 {
 440    Ty _V2 = cons->alg_ty;
 441    if (_V2) {
 442       switch (_V2->tag__) {
 443          case a_Ty::tag_TYCONty: {
 444             if (boxed(((Ty_TYCONty *)_V2)->_1)) {
 445                switch (((Ty_TYCONty *)_V2)->_1->tag__) {
 446                   case a_TyCon::tag_DATATYPEtycon: {
 447 #line 163 "trs.pcc"
 448                    Functor f = Fmap.type_map.value(E) + cons->tag +
 449                                        (cons->ty == NOty ? 0 : ((TyCon_DATATYPEtycon *)((Ty_TYCONty *)_V2)->_1)->unit);
 450                          return CONSterm(f,cons,n,make_term(pats));
 451
 452 #line 166 "trs.pcc"
 453                      } break;
 454                   default: {
 455                      L9:;
 456 #line 167 "trs.pcc"
 457                     bug("TRS::make_term"); return PATterm(pat);
 458 #line 167 "trs.pcc"
 459                      } break;
 460                }
 461             } else { goto L9; }
 462             } break;
 463          default: { goto L9; } break;
 464       }
 465    } else { goto L9; }
 466 }
 467 #line 168 "trs.pcc"
 468 #line 168 "trs.pcc"
 469
 470 }
 471
 472 ///////////////////////////////////////////////////////////////////////////////
 473 //
 474 //  Method to create the lhs for rule r
 475 //
 476 ///////////////////////////////////////////////////////////////////////////////
 477 Term * TRS::make_term(Pats pats)
 478 {  int n = length(pats);
 479    Term * args = (Term *)mem_pool.m_alloc(sizeof(Term) * n);
 480    int i = 0;
 481    for_each(Pat, p, pats) args[i++] = make_term(p);
 482    return args;
 483 }
 484
 485 ///////////////////////////////////////////////////////////////////////////////
 486 //
 487 //  Return the type of an expression
 488 //
 489 ///////////////////////////////////////////////////////////////////////////////
 490 Ty type_of(Exp e) { return type_of(e,Env()); }
 491
 492 ///////////////////////////////////////////////////////////////////////////////
 493 //
 494 //  Method to create the rhs for rule r
 495 //
 496 ///////////////////////////////////////////////////////////////////////////////
 497 void TRS::make_rhs(Rule r, Exp exp)
 498 {  type_of(exp);
 499    rhs_map[r] = make_term(exp);
 500 }
 501
 502 ///////////////////////////////////////////////////////////////////////////////
 503 //
 504 //  Method to create the rhs
 505 //
 506 ///////////////////////////////////////////////////////////////////////////////
 507 Term TRS::make_term(Exp exp)
 508 {  Exp law_exp;
 509
 510 #line 208 "trs.pcc"
 511 #line 242 "trs.pcc"
 512 {
 513    for (;;) {
 514       if (exp) {
 515          switch (exp->tag__) {
 516             case a_Exp::tag_LITERALexp: {
 517                if (
 518 #line 239 "trs.pcc"
 519                Fmap.literal_map.contains(((Exp_LITERALexp *)exp)->LITERALexp)
 520 #line 239 "trs.pcc"
 521 ) {
 522
 523 #line 240 "trs.pcc"
 524                  return CONSterm(Fmap.literal_map[((Exp_LITERALexp *)exp)->LITERALexp],0,0,0);
 525 #line 240 "trs.pcc"
 526                } else {
 527
 528                   L11:;
 529                   if (
 530 #line 241 "trs.pcc"
 531                   is_pattern_var(exp)
 532 #line 241 "trs.pcc"
 533 ) {
 534
 535                      L12:;
 536 #line 241 "trs.pcc"
 537                     return make_term_var(NOpat,exp);
 538 #line 241 "trs.pcc"
 539                   } else {
 540
 541                      L13:;
 542 #line 242 "trs.pcc"
 543                     return CODEterm(exp);
 544 #line 242 "trs.pcc"
 545                   }
 546                }
 547                } break;
 548             case a_Exp::tag_IDexp: {
 549 #line 210 "trs.pcc"
 550               return make_term(exp,((Exp_IDexp *)exp)->IDexp,
 551 #line 210 "trs.pcc"
 552 #line 210 "trs.pcc"
 553                nil_1_
 554 #line 210 "trs.pcc"
 555 #line 210 "trs.pcc"
 556                );
 557 #line 210 "trs.pcc"
 558                } break;
 559             case a_Exp::tag_APPexp: {
 560                if (
 561 #line 241 "trs.pcc"
 562                is_pattern_var(exp)
 563 #line 241 "trs.pcc"
 564 ) {
 565
 566                   if (((Exp_APPexp *)exp)->_1) {
 567                      switch (((Exp_APPexp *)exp)->_1->tag__) {
 568                         case a_Exp::tag_IDexp: {
 569                            L14:;
 570                            if (((Exp_APPexp *)exp)->_2) {
 571                               switch (((Exp_APPexp *)exp)->_2->tag__) {
 572                                  case a_Exp::tag_TUPLEexp: {
 573                                     L15:;
 574 #line 228 "trs.pcc"
 575                                    law_exp = DatatypeCompiler::lookup_law(((Exp_IDexp *)((Exp_APPexp *)exp)->_1)->IDexp,((Exp_TUPLEexp *)((Exp_APPexp *)exp)->_2)->TUPLEexp);
 576                                         if (law_exp == NOexp) return make_term(exp,((Exp_IDexp *)((Exp_APPexp *)exp)->_1)->IDexp,((Exp_TUPLEexp *)((Exp_APPexp *)exp)->_2)->TUPLEexp);
 577                                         type_of(law_exp);
 578                                         exp = law_exp;
 579
 580 #line 232 "trs.pcc"
 581                                     } break;
 582                                  default: {
 583                                     L16:;
 584 #line 234 "trs.pcc"
 585                                    law_exp = DatatypeCompiler::lookup_law(((Exp_IDexp *)((Exp_APPexp *)exp)->_1)->IDexp,
 586 #line 234 "trs.pcc"
 587 #line 234 "trs.pcc"
 588                                     list_1_(((Exp_APPexp *)exp)->_2)
 589 #line 234 "trs.pcc"
 590 #line 234 "trs.pcc"
 591                                     );
 592                                         if (law_exp == NOexp) return make_term(exp,((Exp_IDexp *)((Exp_APPexp *)exp)->_1)->IDexp,
 593 #line 235 "trs.pcc"
 594 #line 235 "trs.pcc"
 595                                     list_1_(((Exp_APPexp *)exp)->_2)
 596 #line 235 "trs.pcc"
 597 #line 235 "trs.pcc"
 598                                     );
 599                                         type_of(law_exp);
 600                                         exp = law_exp;
 601
 602 #line 238 "trs.pcc"
 603                                     } break;
 604                               }
 605                            } else { goto L16; }
 606                            } break;
 607                         default: { goto L12; } break;
 608                      }
 609                   } else { goto L12; }
 610                } else {
 611
 612                   if (((Exp_APPexp *)exp)->_1) {
 613                      switch (((Exp_APPexp *)exp)->_1->tag__) {
 614                         case a_Exp::tag_IDexp: { goto L14; } break;
 615                         default: { goto L13; } break;
 616                      }
 617                   } else { goto L13; }
 618                }
 619                } break;
 620             case a_Exp::tag_LISTexp: {
 621                if (
 622 #line 241 "trs.pcc"
 623                is_pattern_var(exp)
 624 #line 241 "trs.pcc"
 625 ) {
 626
 627                   if (((Exp_LISTexp *)exp)->_3) {
 628                      L17:;
 629                      if (((Exp_LISTexp *)exp)->_3->_2) {
 630                         L18:;
 631 #line 223 "trs.pcc"
 632                        Exp e2 = LISTexp(((Exp_LISTexp *)exp)->_1, ((Exp_LISTexp *)exp)->_2, ((Exp_LISTexp *)exp)->_3->_2, ((Exp_LISTexp *)exp)->_4);
 633                                 e2->ty = exp->ty;
 634                                 return make_term(exp,((Exp_LISTexp *)exp)->_1->name,
 635 #line 225 "trs.pcc"
 636 #line 225 "trs.pcc"
 637                         list_1_(((Exp_LISTexp *)exp)->_3->_1,list_1_(e2))
 638 #line 225 "trs.pcc"
 639 #line 225 "trs.pcc"
 640                         );
 641
 642 #line 226 "trs.pcc"
 643                      } else {
 644                         L19:;
 645 #line 218 "trs.pcc"
 646                        Exp nil_exp = ((Exp_LISTexp *)exp)->_4 == NOexp ? CONSexp(((Exp_LISTexp *)exp)->_2,
 647 #line 218 "trs.pcc"
 648 #line 218 "trs.pcc"
 649                         nil_1_
 650 #line 218 "trs.pcc"
 651 #line 218 "trs.pcc"
 652                         ,NOexp) : ((Exp_LISTexp *)exp)->_4;
 653                                 nil_exp->ty = exp->ty;
 654                                 return make_term(exp,((Exp_LISTexp *)exp)->_1->name,
 655 #line 220 "trs.pcc"
 656 #line 220 "trs.pcc"
 657                         list_1_(((Exp_LISTexp *)exp)->_3->_1,list_1_(nil_exp))
 658 #line 220 "trs.pcc"
 659 #line 220 "trs.pcc"
 660                         );
 661
 662 #line 221 "trs.pcc"
 663                      }
 664                   } else { goto L12; }
 665                } else {
 666
 667                   if (((Exp_LISTexp *)exp)->_3) { goto L17; } else { goto L13; }
 668                }
 669                } break;
 670             case a_Exp::tag_CONSexp: {
 671                if (
 672 #line 241 "trs.pcc"
 673                is_pattern_var(exp)
 674 #line 241 "trs.pcc"
 675 ) {
 676
 677                   if (((Exp_CONSexp *)exp)->_3) {
 678                      switch (((Exp_CONSexp *)exp)->_3->tag__) {
 679                         case a_Exp::tag_TUPLEexp: {
 680                            if (((Exp_CONSexp *)exp)->_2) { goto L12; } else {
 681                               L20:;
 682 #line 214 "trs.pcc"
 683                              return make_term(exp,((Exp_CONSexp *)exp)->_1->name,((Exp_TUPLEexp *)((Exp_CONSexp *)exp)->_3)->TUPLEexp);
 684 #line 214 "trs.pcc"
 685                            }
 686                            } break;
 687                         default: {
 688                            if (((Exp_CONSexp *)exp)->_2) { goto L12; } else {
 689                               L21:;
 690 #line 216 "trs.pcc"
 691                              return make_term(exp,((Exp_CONSexp *)exp)->_1->name,
 692 #line 216 "trs.pcc"
 693 #line 216 "trs.pcc"
 694                               list_1_(((Exp_CONSexp *)exp)->_3)
 695 #line 216 "trs.pcc"
 696 #line 216 "trs.pcc"
 697                               );
 698 #line 216 "trs.pcc"
 699                            }
 700                            } break;
 701                      }
 702                   } else {
 703                      if (((Exp_CONSexp *)exp)->_2) { goto L12; } else {
 704                         L22:;
 705 #line 212 "trs.pcc"
 706                        return make_term(exp,((Exp_CONSexp *)exp)->_1->name,
 707 #line 212 "trs.pcc"
 708 #line 212 "trs.pcc"
 709                         nil_1_
 710 #line 212 "trs.pcc"
 711 #line 212 "trs.pcc"
 712                         );
 713 #line 212 "trs.pcc"
 714                      }
 715                   }
 716                } else {
 717
 718                   if (((Exp_CONSexp *)exp)->_3) {
 719                      switch (((Exp_CONSexp *)exp)->_3->tag__) {
 720                         case a_Exp::tag_TUPLEexp: {
 721                            if (((Exp_CONSexp *)exp)->_2) { goto L13; } else { goto L20; }
 722                            } break;
 723                         default: {
 724                            if (((Exp_CONSexp *)exp)->_2) { goto L13; } else { goto L21; }
 725                            } break;
 726                      }
 727                   } else {
 728                      if (((Exp_CONSexp *)exp)->_2) { goto L13; } else { goto L22; }
 729                   }
 730                }
 731                } break;
 732             case a_Exp::tag_MARKEDexp: {
 733 #line 209 "trs.pcc"
 734               exp = ((Exp_MARKEDexp *)exp)->_2;
 735 #line 209 "trs.pcc"
 736                } break;
 737             default: { goto L11; } break;
 738          }
 739       } else { goto L11; }
 740    }
 741 }
 742 #line 243 "trs.pcc"
 743 #line 243 "trs.pcc"
 744
 745 }
 746
 747 ///////////////////////////////////////////////////////////////////////////////
 748 //
 749 //  Method to create the rhs
 750 //
 751 ///////////////////////////////////////////////////////////////////////////////
 752 Term TRS::make_term(Exp exp, Id id, Exps exps)
 753 {  int n = length(exps);
 754    Cons cons = find_cons(id);
 755    if (cons == NOcons) { return CODEterm(exp); }
 756    FunctorTable::Entry * E = Fmap.type_map.lookup(exp->ty);
 757    if (E == 0) { return CODEterm(exp); }
 758
 759 #line 257 "trs.pcc"
 760 #line 263 "trs.pcc"
 761 {
 762    Ty _V3 = cons->alg_ty;
 763    if (_V3) {
 764       switch (_V3->tag__) {
 765          case a_Ty::tag_TYCONty: {
 766             if (boxed(((Ty_TYCONty *)_V3)->_1)) {
 767                switch (((Ty_TYCONty *)_V3)->_1->tag__) {
 768                   case a_TyCon::tag_DATATYPEtycon: {
 769 #line 259 "trs.pcc"
 770                    Functor f = Fmap.type_map.value(E) + cons->tag +
 771                                          (cons->ty == NOty ? 0 : ((TyCon_DATATYPEtycon *)((Ty_TYCONty *)_V3)->_1)->unit);
 772                          return CONSterm(f,cons,n,make_term(exps));
 773
 774 #line 262 "trs.pcc"
 775                      } break;
 776                   default: {
 777                      L23:;
 778 #line 263 "trs.pcc"
 779                     bug("TRS::make_term"); return CODEterm(exp);
 780 #line 263 "trs.pcc"
 781                      } break;
 782                }
 783             } else { goto L23; }
 784             } break;
 785          default: { goto L23; } break;
 786       }
 787    } else { goto L23; }
 788 }
 789 #line 264 "trs.pcc"
 790 #line 264 "trs.pcc"
 791
 792 }
 793
 794 ///////////////////////////////////////////////////////////////////////////////
 795 //
 796 //  Method to create the term variable
 797 //
 798 ///////////////////////////////////////////////////////////////////////////////
 799 Term TRS::make_term_var(Pat pat, Exp exp)
 800 {  for (int i = 0; i < num_vars; i++)
 801    {  if (equal(exp,vars[i])) return VARterm(i,var_pats[i],vars[i]); }
 802    if (pat == NOpat) { return CODEterm(exp); }
 803    if (num_vars == MAX_VARS)
 804       bug("%LTRS::make_term_var() too many variables");
 805    vars[num_vars] = exp;
 806    var_pats[num_vars] = pat;
 807    return VARterm(num_vars++,pat,exp);
 808 }
 809
 810 ///////////////////////////////////////////////////////////////////////////////
 811 //
 812 //  Method to create the term from a list of expressions
 813 //
 814 ///////////////////////////////////////////////////////////////////////////////
 815 Term * TRS::make_term(Exps exps)
 816 {  int n = length(exps);
 817    Term * args = (Term *)mem_pool.m_alloc(sizeof(Term) * n);
 818    int i = 0;
 819    for_each(Exp, e, exps) args[i++] = make_term(e);
 820    return args;
 821 }
 822
 823 /////////////////////////////////////////////////////////////////////////////// //
 824 //
 825 //  Method to print a term
 826 //
 827 ///////////////////////////////////////////////////////////////////////////////
 828 void TRS::print (ostream& s, Term term) const
 829 {
 830 #line 302 "trs.pcc"
 831 #line 336 "trs.pcc"
 832 {
 833    switch (term->tag__) {
 834       case a_Term::tag_CONSterm: {
 835          switch (((Term_CONSterm *)term)->_3) {
 836             case 2: {
 837                if (
 838 #line 303 "trs.pcc"
 839                is_list_constructor(((Term_CONSterm *)term)->_2)
 840 #line 303 "trs.pcc"
 841 ) {
 842
 843 #line 304 "trs.pcc"
 844                 s << '#' << ((Term_CONSterm *)term)->_2->name[1];
 845                          Term t = term;
 846                          Id comma = "";
 847
 848 #line 307 "trs.pcc"
 849 #line 309 "trs.pcc"
 850                   {
 851                      for (;;) {
 852                         switch (t->tag__) {
 853                            case a_Term::tag_CONSterm: {
 854                               switch (((Term_CONSterm *)t)->_3) {
 855                                  case 2: {
 856                                     if (
 857 #line 308 "trs.pcc"
 858                                     (((Term_CONSterm *)t)->_1 == ((Term_CONSterm *)term)->_1)
 859 #line 308 "trs.pcc"
 860 ) {
 861
 862 #line 309 "trs.pcc"
 863                                      s << comma; print(s,((Term_CONSterm *)t)->_4[0]); t = ((Term_CONSterm *)t)->_4[1]; comma = ", ";
 864 #line 309 "trs.pcc"
 865                                     } else {
 866                                         goto L24; }
 867                                  } break;
 868                                  default: { goto L24; }
 869                               }
 870                               } break;
 871                            default: { goto L24; } break;
 872                         }
 873                      }
 874                      L24:;
 875                   }
 876 #line 310 "trs.pcc"
 877 #line 310 "trs.pcc"
 878
 879
 880 #line 311 "trs.pcc"
 881 #line 314 "trs.pcc"
 882                   {
 883                      switch (t->tag__) {
 884                         case a_Term::tag_CONSterm: {
 885                            switch (((Term_CONSterm *)t)->_3) {
 886                               case 0: {
 887                                  if (
 888 #line 313 "trs.pcc"
 889                                  (((Term_CONSterm *)term)->_2 && is_list_constructor(((Term_CONSterm *)t)->_2))
 890 #line 313 "trs.pcc"
 891 ) {
 892                                     } else {
 893
 894                                     L25:;
 895 #line 314 "trs.pcc"
 896                                    s << comma; print(s,t);
 897 #line 314 "trs.pcc"
 898                                  }
 899                               } break;
 900                               default: { goto L25; }
 901                            }
 902                            } break;
 903                         default: { goto L25; } break;
 904                      }
 905                   }
 906 #line 315 "trs.pcc"
 907 #line 315 "trs.pcc"
 908
 909                          s << ((Term_CONSterm *)term)->_2->name[5];
 910
 911 #line 317 "trs.pcc"
 912                } else {
 913
 914                   L26:;
 915 #line 319 "trs.pcc"
 916                 s << (((Term_CONSterm *)term)->_2 != NOcons ? ((Term_CONSterm *)term)->_2->name : Fmap.G.functor_name(((Term_CONSterm *)term)->_1));
 917                   if (((Term_CONSterm *)term)->_3 > 0)
 918                   {  s << '(';
 919                      for (int i = 0; i < ((Term_CONSterm *)term)->_3; i++)
 920                      {  print(s,((Term_CONSterm *)term)->_4[i]);
 921                         if (i < ((Term_CONSterm *)term)->_3 - 1) s << ", ";
 922                      }
 923                      s << ')';
 924                   }
 925
 926 #line 328 "trs.pcc"
 927                }
 928             } break;
 929             default: { goto L26; }
 930          }
 931          } break;
 932       case a_Term::tag_VARterm: {
 933 #line 329 "trs.pcc"
 934         s << ((Term_VARterm *)term)->_2;
 935 #line 329 "trs.pcc"
 936          } break;
 937       case a_Term::tag_CODEterm: {
 938 #line 330 "trs.pcc"
 939         Bool save = pretty_print_exp;
 940                                   pretty_print_exp = true;
 941                                   s << "[[" << ((Term_CODEterm *)term)->CODEterm << "]]";
 942                                   pretty_print_exp = save;
 943
 944 #line 334 "trs.pcc"
 945          } break;
 946       case a_Term::tag_OPAQUEterm: {
 947 #line 335 "trs.pcc"
 948         s << "...";
 949 #line 335 "trs.pcc"
 950          } break;
 951       default: {
 952 #line 336 "trs.pcc"
 953         s << "[[" << ((Term_PATterm *)term)->PATterm << "]]";
 954 #line 336 "trs.pcc"
 955          } break;
 956    }
 957 }
 958 #line 337 "trs.pcc"
 959 #line 337 "trs.pcc"
 960
 961 }
 962
 963 ///////////////////////////////////////////////////////////////////////////////
 964 //
 965 //  Method to print a TRS
 966 //
 967 ///////////////////////////////////////////////////////////////////////////////
 968 void TRS::print (ostream& s) const
 969 {  s << "\n\nBottom-up term rewriting system:\n";
 970    Bool save = pretty_print_exp;
 971    pretty_print_exp = true;
 972    for (Rule r = 0; r < number_of_rules; r++)
 973    {  MatchRule rule = rule_map[r];
 974       s << "line " << rule->begin_line << ": ";
 975       print(s,lhs_map[r]);
 976       if (guard_map[r] != NOexp) s << " | " << guard_map[r];
 977       s << ":\n\t"; print(s,rhs_map[r]); s << '\n';
 978       for (int i = 0; i < num_var_map[r]; i++)
 979       {  Pat pat_var = var_pat_map[r][i];
 980          Ty pat_ty   = pat_var->ty;
 981          s << "\tvariable " << pat_var << " : " << pat_ty;
 982          if (! compiler.has_index(pat_ty)) s << " has no index";
 983          s << '\n';
 984       }
 985       s << '\n';
 986    }
 987    s << '\n';
 988    pretty_print_exp = save;
 989 }
 990 #line 367 "trs.pcc"
 991 /*
 992 ------------------------------- Statistics -------------------------------
 993 Merge matching rules         = yes
 994 Number of DFA nodes merged   = 903
 995 Number of ifs generated      = 43
 996 Number of switches generated = 25
 997 Number of labels             = 22
 998 Number of gotos              = 46
 999 Adaptive matching            = enabled
1000 Fast string matching         = disabled
1001 Inline downcasts             = enabled
1002 --------------------------------------------------------------------------
1003 */